def EllipticRegularityConcrete.DiffForm (n k : ℕ) : Type

A differential $k$-form on $\mathbb{R}^n$: a map from $\mathbb{R}^n$ to the space of continuous alternating $k$-multilinear forms on $\mathbb{R}^n$.

@[implicit_reducible]

noncomputable instance EllipticRegularityConcrete.instAddCommGroup (n k : ℕ) : AddCommGroup (DiffForm n k)

Pointwise addition gives DiffForm n k the structure of an additive abelian group.

@[implicit_reducible]

noncomputable instance EllipticRegularityConcrete.instModule (n k : ℕ) : Module ℝ (DiffForm n k)

Pointwise scalar multiplication gives DiffForm n k the structure of an $\mathbb{R}$-module.

def EllipticRegularityConcrete.IsSmoothForm {n k : ℕ} (ξ : DiffForm n k) : Prop

A differential form is smooth ($C^\infty$) when its coefficient map is infinitely differentiable as a function $\mathbb{R}^n \to (\mathbb{R}^n)^{[\Lambda^k]\to \mathbb{R}}$.

theorem EllipticRegularityConcrete.isSmoothForm_sub {n k : ℕ} (a b : DiffForm n k) (ha : IsSmoothForm a) (hb : IsSmoothForm b) : IsSmoothForm (a - b)

Smoothness is preserved under subtraction: $a, b \in C^\infty \Rightarrow a - b \in C^\infty$.

structure EllipticRegularityConcrete.SobolevNorms (n k : ℕ) : Type

A family of nonnegative Sobolev seminorms indexed by regularity index $s \in \mathbb{N}$, acting on differential $(k+1)$-forms.

• norm : ℕ → DiffForm n (k + 1) → ℝ
• norm_nonneg (s : ℕ) (ξ : DiffForm n (k + 1)) : 0 ≤ self.norm s ξ

def EllipticRegularityConcrete.HasSobolevRegularity {n k : ℕ} (snorms : SobolevNorms n k) (s : ℕ) (ξ : DiffForm n (k + 1)) : Prop

The form $\xi$ has Sobolev regularity of order $s$ when $\|\xi\|_s$ is bounded by some constant. (Trivially holds in this framework but records the membership in $H^s$ qualitatively.)

structure EllipticRegularityConcrete.IsSmoothingOperator {n k : ℕ} (snorms : SobolevNorms n k) (S : DiffForm n (k + 1) → DiffForm n (k + 1)) : Prop

A smoothing (regularity-improving) operator: it gains one derivative in the Sobolev scale and maps anything with finite Sobolev regularity into the smooth class $C^\infty$.

• regularity_gain (s : ℕ) : ∃ C > 0, ∀ (ξ : DiffForm n (k + 1)), snorms.norm (s + 1) (S ξ) ≤ C * snorms.norm s ξ
• maps_to_smooth (s : ℕ) (ξ : DiffForm n (k + 1)) : HasSobolevRegularity snorms s ξ → IsSmoothForm (S ξ)

structure EllipticRegularityConcrete.ConcreteParametrix {n : ℕ} (k : ℕ) (L : DiffForm n (k + 1) → DiffForm n (k + 1)) : Type

A concrete parametrix for an elliptic operator $L$: an approximate inverse $P$ with $P \circ L = \mathrm{Id} + S$ for a smoothing remainder $S$. This is the key analytic input for the elliptic regularity theorem $L\xi \in C^\infty \Rightarrow \xi \in C^\infty$.

• P : DiffForm n (k + 1) → DiffForm n (k + 1)
• S_left : DiffForm n (k + 1) → DiffForm n (k + 1)
• sobolevNorms : SobolevNorms n k
• PL_eq (ξ : DiffForm n (k + 1)) : self.P (L ξ) = ξ + self.S_left ξ
• S_left_smoothing : IsSmoothingOperator self.sobolevNorms self.S_left