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

Differential $k$-form on $\mathbb{R}^n$: a pointwise alternating $\mathbb{R}$-multilinear $k$-form on $\mathbb{R}^n$.

@[implicit_reducible]

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

Pointwise additive group structure on differential $k$-forms.

@[implicit_reducible]

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

Pointwise $\mathbb{R}$-module structure on differential $k$-forms.

@[implicit_reducible]

noncomputable instance EllipticRegularityBridge.instMeasurableSpace (n : ℕ) : MeasurableSpace (EuclideanSpace ℝ (Fin n))

Borel measurable space structure on $\mathbb{R}^n$, needed for integration of forms.

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

A differential form $\xi$ is smooth iff it is $C^\infty$ as a map between normed spaces.

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

Abstract data of Sobolev norms $\|\xi\|_{H^s}$ on $(k+1)$-forms, indexed by regularity $s$, required to be nonnegative.

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

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

$\xi$ has Sobolev regularity $H^s$ iff $\|\xi\|_{H^s} < \infty$.

theorem EllipticRegularityBridge.isSmoothForm_iff_contMDiff {n k : ℕ} (ξ : DiffForm n k) : IsSmoothForm ξ ↔ ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n) [⋀^Fin k]→L[ℝ] ℝ)) ⊤ ξ

A differential form on $\mathbb{R}^n$ is smooth iff it is $C^\infty$ as a manifold map between the trivially-charted vector spaces.

theorem EllipticRegularityBridge.IsSmoothForm.toContMDiff {n k : ℕ} {ξ : DiffForm n k} (h : IsSmoothForm ξ) : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n) [⋀^Fin k]→L[ℝ] ℝ)) ⊤ ξ

Forward direction: a smooth form is $C^\infty$ in the manifold sense.

theorem EllipticRegularityBridge.IsSmoothForm.ofContMDiff {n k : ℕ} {ξ : DiffForm n k} (h : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n) [⋀^Fin k]→L[ℝ] ℝ)) ⊤ ξ) : IsSmoothForm ξ

Reverse direction: a manifold-$C^\infty$ form is smooth in the analytic sense.

theorem EllipticRegularityBridge.sobolev_zero_iff_memLp {n k : ℕ} (snorms : SobolevNorms n k) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) [MeasureTheory.IsFiniteMeasure μ] (ξ : DiffForm n (k + 1)) : HasSobolevRegularity snorms 0 ξ ↔ MeasureTheory.MemLp ξ 2 μ

Bridge: $H^0$-Sobolev regularity coincides with membership in $L^2$ under a finite measure.

theorem EllipticRegularityBridge.HasSobolevRegularity.toMemLp {n k : ℕ} {snorms : SobolevNorms n k} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} [MeasureTheory.IsFiniteMeasure μ] {ξ : DiffForm n (k + 1)} (h : HasSobolevRegularity snorms 0 ξ) : MeasureTheory.MemLp ξ 2 μ

Forward implication of the $H^0$–$L^2$ bridge.

theorem EllipticRegularityBridge.HasSobolevRegularity.ofMemLp {n k : ℕ} {snorms : SobolevNorms n k} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} [MeasureTheory.IsFiniteMeasure μ] {ξ : DiffForm n (k + 1)} (h : MeasureTheory.MemLp ξ 2 μ) : HasSobolevRegularity snorms 0 ξ

Reverse implication of the $H^0$–$L^2$ bridge.