@[reducible, inline]

abbrev ParametrixOnManifold.SmoothSection {E_model : Type u_1} [NormedAddCommGroup E_model] [NormedSpace ℝ E_model] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E_model H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (V : M → Type u_5) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [VectorBundle ℝ F V] : Type (max u_3 u_5)

A smooth section of a vector bundle $V \to M$ over a manifold $M$, i.e. an element of $\Gamma(V) = C^\infty(M, V)$.

structure ParametrixOnManifold.SobolevNormFamily {E_model : Type u_1} [NormedAddCommGroup E_model] [NormedSpace ℝ E_model] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E_model H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] (FE : Type u_4) [NormedAddCommGroup FE] [NormedSpace ℝ FE] (VE : M → Type u_5) [TopologicalSpace (Bundle.TotalSpace FE VE)] [(x : M) → TopologicalSpace (VE x)] [FiberBundle FE VE] [(x : M) → AddCommGroup (VE x)] [(x : M) → Module ℝ (VE x)] [VectorBundle ℝ FE VE] : Type (max u_3 u_5)

A family of Sobolev norms $\|\cdot\|_{W^s}$ on smooth sections of a vector bundle over a compact manifold $M$, indexed by the regularity index $s \in \mathbb{N}$, satisfying non-negativity, monotonicity in $s$, and the triangle inequality.

• norm : ℕ → SmoothSection I M FE VE → ℝ
• norm_nonneg (s : ℕ) (σ : SmoothSection I M FE VE) : 0 ≤ self.norm s σ
• norm_mono (s t : ℕ) (σ : SmoothSection I M FE VE) : s ≤ t → self.norm s σ ≤ self.norm t σ
• norm_add (s : ℕ) (σ τ : SmoothSection I M FE VE) : self.norm s (σ + τ) ≤ self.norm s σ + self.norm s τ

structure ParametrixOnManifold.IsSmoothingOnManifold {E_model : Type u_1} [NormedAddCommGroup E_model] [NormedSpace ℝ E_model] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E_model H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] {FE : Type u_4} [NormedAddCommGroup FE] [NormedSpace ℝ FE] {VE : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace FE VE)] [(x : M) → TopologicalSpace (VE x)] [FiberBundle FE VE] [(x : M) → AddCommGroup (VE x)] [(x : M) → Module ℝ (VE x)] [VectorBundle ℝ FE VE] (W : SobolevNormFamily I FE VE) (S : SmoothSection I M FE VE →ₗ[ℝ] SmoothSection I M FE VE) : Prop

A linear operator $S$ on $\Gamma(V)$ is a smoothing operator if it improves Sobolev regularity by one degree: for every $s$, there exists $C > 0$ with $\|S\sigma\|_{W^{s+1}} \leq C \|\sigma\|_{W^s}$.

• regularity_improvement (s : ℕ) : ∃ C > 0, ∀ (σ : SmoothSection I M FE VE), W.norm (s + 1) (S σ) ≤ C * W.norm s σ

structure ParametrixOnManifold.HasParametrixOnManifold {E_model : Type u_1} [NormedAddCommGroup E_model] [NormedSpace ℝ E_model] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E_model H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] [IsManifold I ⊤ M] {FE : Type u_4} [NormedAddCommGroup FE] [NormedSpace ℝ FE] {VE : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace FE VE)] [(x : M) → TopologicalSpace (VE x)] [FiberBundle FE VE] [(x : M) → AddCommGroup (VE x)] [(x : M) → Module ℝ (VE x)] [VectorBundle ℝ FE VE] {FF : Type u_6} [NormedAddCommGroup FF] [NormedSpace ℝ FF] {VF : M → Type u_7} [TopologicalSpace (Bundle.TotalSpace FF VF)] [(x : M) → TopologicalSpace (VF x)] [FiberBundle FF VF] [(x : M) → AddCommGroup (VF x)] [(x : M) → Module ℝ (VF x)] [VectorBundle ℝ FF VF] (L : SmoothSection I M FE VE →ₗ[ℝ] SmoothSection I M FF VF) : Type (max (max u_3 u_5) u_7)

A linear operator $L : \Gamma(V_E) \to \Gamma(V_F)$ between sections of two vector bundles on a compact manifold $M$ has a parametrix $P : \Gamma(V_F) \to \Gamma(V_E)$ if both $P \circ L - \mathrm{id}$ and $L \circ P - \mathrm{id}$ are smoothing operators (raising Sobolev regularity $W^s \to W^{s+1}$).

• P : SmoothSection I M FF VF →ₗ[ℝ] SmoothSection I M FE VE
• S_left : SmoothSection I M FE VE →ₗ[ℝ] SmoothSection I M FE VE
• S_right : SmoothSection I M FF VF →ₗ[ℝ] SmoothSection I M FF VF
• W_E : SobolevNormFamily I FE VE
• W_F : SobolevNormFamily I FF VF
• PL_eq (σ : SmoothSection I M FE VE) : self.P (L σ) = σ + self.S_left σ
• LP_eq (τ : SmoothSection I M FF VF) : L (self.P τ) = τ + self.S_right τ
• isSmoothing_left : IsSmoothingOnManifold self.W_E self.S_left
• isSmoothing_right : IsSmoothingOnManifold self.W_F self.S_right

structure ParametrixOnManifold.IsEllipticOnManifold {E_model : Type u_1} [NormedAddCommGroup E_model] [NormedSpace ℝ E_model] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E_model H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] {FE : Type u_4} [NormedAddCommGroup FE] [NormedSpace ℝ FE] {VE : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace FE VE)] [(x : M) → TopologicalSpace (VE x)] [FiberBundle FE VE] [(x : M) → AddCommGroup (VE x)] [(x : M) → Module ℝ (VE x)] [VectorBundle ℝ FE VE] {FF : Type u_6} [NormedAddCommGroup FF] [NormedSpace ℝ FF] {VF : M → Type u_7} [TopologicalSpace (Bundle.TotalSpace FF VF)] [(x : M) → TopologicalSpace (VF x)] [FiberBundle FF VF] [(x : M) → AddCommGroup (VF x)] [(x : M) → Module ℝ (VF x)] [VectorBundle ℝ FF VF] (L : SmoothSection I M FE VE →ₗ[ℝ] SmoothSection I M FF VF) : Type (max (max (max u_1 u_3) u_4) u_6)

A linear differential operator $L$ of order $m$ between sections of vector bundles on $M$ is elliptic if its principal symbol $\sigma_m(L)(x, \xi) : (V_E)_x \to (V_F)_x$ is a linear bijection for every $x \in M$ and every nonzero cotangent vector $\xi$, and is homogeneous of degree $m$ in $\xi$.

• order : ℕ
• symbol : M → E_model → FE →ₗ[ℝ] FF
• elliptic (x : M) (ξ : E_model) : ξ ≠ 0 → Function.Bijective ⇑(self.symbol x ξ)
• symbol_homogeneous (x : M) (t : ℝ) (ξ : E_model) (v : FE) : (self.symbol x (t • ξ)) v = t ^ self.order • (self.symbol x ξ) v