@[reducible, inline]

abbrev MultiIndex (n : ℕ) : Type

A multi-index $\alpha = (\alpha_1, \ldots, \alpha_n) \in \mathbb{N}^n$ on $n$ variables.

def multiIndexDegree {n : ℕ} (α : MultiIndex n) : ℕ

Total degree $|\alpha| = \sum_i \alpha_i$ of a multi-index.

noncomputable def multiIndexMonomial {n : ℕ} (α : MultiIndex n) (ξ : Fin n → ℝ) : ℝ

The monomial $\xi^\alpha = \prod_i \xi_i^{\alpha_i}$ associated to multi-index $\alpha$.

noncomputable def multiIndicesBounded (n k : ℕ) : Finset (MultiIndex n)

The finite set of multi-indices $\alpha \in \mathbb{N}^n$ with each component $\alpha_i \le k$.

noncomputable def multiIndicesOfDegree (n k : ℕ) : Finset (MultiIndex n)

The finite set of multi-indices of total degree exactly $k$.

noncomputable def multiIndicesOfDegreeLE (n k : ℕ) : Finset (MultiIndex n)

The finite set of multi-indices of total degree $\le k$.

noncomputable def principalSymbol {n k : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (A : MultiIndex n → E →L[ℝ] F) (ξ : Fin n → ℝ) : E →L[ℝ] F

The principal symbol $\sigma_k(L)(\xi) = \sum_{|\alpha| = k} \xi^\alpha A_\alpha$ of a differential operator with leading-order coefficients $A_\alpha$.

structure IsEllipticOperator (n : ℕ) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) : Type (max u_1 u_2)

An elliptic linear differential operator $L: \Gamma(E) \to \Gamma(F)$ of order $k$: locally $L = \sum_{|\alpha| \le k} A_\alpha \partial^\alpha$, with bijective principal symbol $\sigma_k(L)(\xi)$ for all $\xi \ne 0$.

• order : ℕ
• coeff : MultiIndex n → E →L[ℝ] F
• coeff_support (α : MultiIndex n) : multiIndexDegree α > self.order → self.coeff α = 0
• partialDeriv : MultiIndex n → E →L[ℝ] E
• local_expression (s : E) : L s = ∑ α ∈ multiIndicesOfDegreeLE n self.order, (self.coeff α) ((self.partialDeriv α) s)
• elliptic (ξ : Fin n → ℝ) : ξ ≠ 0 → Function.Bijective ⇑(principalSymbol self.coeff ξ)

noncomputable def IsEllipticOperator.symbol {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {L : E →L[ℝ] F} (hL : IsEllipticOperator n L) (ξ : Fin n → ℝ) : E →L[ℝ] F

The principal symbol $\sigma(L)(\xi)$ of an elliptic operator $L$, evaluated at cotangent direction $\xi$.

structure IsSmoothingOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (sobolevNorm : ℕ → E → ℝ) (S : E →L[ℝ] E) : Prop

A smoothing operator $S$: bounded for each Sobolev norm with a one-step gain in regularity, $\|S x\|_{s+1} \le C_s \|x\|_s$.

• regularity_improvement (s : ℕ) : ∃ C > 0, ∀ (x : E), sobolevNorm (s + 1) (S x) ≤ C * sobolevNorm s x

noncomputable def principalSymbolAt {n k : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_3} (A : M → MultiIndex n → E →L[ℝ] F) (x : M) (ξ : Fin n → ℝ) : E →L[ℝ] F

Pointwise principal symbol $\sigma_k(L)(x, \xi) = \sum_{|\alpha| = k} \xi^\alpha A_\alpha(x)$ of an operator on a manifold $M$ at point $x$ and cotangent vector $\xi$.

structure IsEllipticOperatorOnManifold (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [CompactSpace M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : (M → E) → M → F) : Type (max (max u_1 u_2) u_3)

An elliptic linear differential operator $L: \Gamma(E) \to \Gamma(F)$ on a compact manifold $M$: pointwise of order $k$ with bijective principal symbol at every $(x, \xi)$, $\xi \ne 0$.

• order : ℕ
• coeff : M → MultiIndex n → E →L[ℝ] F
• coeff_support (x : M) (α : MultiIndex n) : multiIndexDegree α > self.order → self.coeff x α = 0
• partialDeriv : MultiIndex n → (M → E) → M → E
• local_expression (s : M → E) (x : M) : L s x = ∑ α ∈ multiIndicesOfDegreeLE n self.order, (self.coeff x α) (self.partialDeriv α s x)
• elliptic (x : M) (ξ : Fin n → ℝ) : ξ ≠ 0 → Function.Bijective ⇑(principalSymbolAt self.coeff x ξ)

noncomputable def IsEllipticOperatorOnManifold.symbol {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [CompactSpace M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {L : (M → E) → M → F} (hL : IsEllipticOperatorOnManifold n M L) (x : M) (ξ : Fin n → ℝ) : E →L[ℝ] F

The principal symbol of an elliptic operator on a manifold, evaluated at $(x, \xi)$.