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

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

@[implicit_reducible]

noncomputable instance HodgeMathlib.instAddCommGroupDiffForm (n k : ℕ) : AddCommGroup (DiffForm n k)

Pointwise addition makes the space of differential $k$-forms an additive group.

@[implicit_reducible]

noncomputable instance HodgeMathlib.instModuleRealDiffForm (n k : ℕ) : Module ℝ (DiffForm n k)

Pointwise scalar multiplication makes the space of differential $k$-forms an $\mathbb{R}$-module.

@[implicit_reducible]

noncomputable instance HodgeMathlib.instTopologicalSpaceDiffForm (n k : ℕ) : TopologicalSpace (DiffForm n k)

The product topology on the space of differential $k$-forms.

noncomputable def HodgeMathlib.dForm {n k : ℕ} (ω : DiffForm n k) : DiffForm n (k + 1)

The exterior derivative $d : \Omega^k \to \Omega^{k+1}$ on differential forms on Euclidean space.

structure HodgeMathlib.Codifferential (n : ℕ) : Type

A codifferential operator $d^* : \Omega^{k+1} \to \Omega^k$ that is linear and satisfies $d^* \circ d^* = 0$.

• dstar {k : ℕ} : DiffForm n (k + 1) → DiffForm n k
• dstar_add {k : ℕ} (α β : DiffForm n (k + 1)) : self.dstar (α + β) = self.dstar α + self.dstar β
• dstar_smul {k : ℕ} (r : ℝ) (α : DiffForm n (k + 1)) : self.dstar (r • α) = r • self.dstar α
• dstar_squared {k : ℕ} (ω : DiffForm n (k + 2)) : self.dstar (self.dstar ω) = 0

noncomputable def HodgeMathlib.laplacian {n : ℕ} (cod : Codifferential n) {k : ℕ} (α : DiffForm n (k + 1)) : DiffForm n (k + 1)

The Hodge Laplacian $\Delta = dd^* + d^*d$ on differential forms.

def HodgeMathlib.IsHarmonic {n : ℕ} (cod : Codifferential n) {k : ℕ} (α : DiffForm n (k + 1)) : Prop

A form $\alpha$ is harmonic if $\Delta \alpha = 0$, i.e. it lies in the kernel of the Hodge Laplacian.

structure HodgeMathlib.L2InnerProduct {n : ℕ} (cod : Codifferential n) : Type

An $L^2$ inner product on differential forms making $d^*$ the formal adjoint of $d$.

• inner {k : ℕ} : DiffForm n k → DiffForm n k → ℝ
• inner_self_eq_zero {k : ℕ} (α : DiffForm n k) : self.inner α α = 0 → α = 0
• inner_self_nonneg {k : ℕ} (α : DiffForm n k) : 0 ≤ self.inner α α
• inner_symm {k : ℕ} (α β : DiffForm n k) : self.inner α β = self.inner β α
• adjoint_d {k : ℕ} (α : DiffForm n k) (β : DiffForm n (k + 1)) : self.inner (dForm α) β = self.inner α (cod.dstar β)
• inner_add_left {k : ℕ} (α β γ : DiffForm n k) : self.inner (α + β) γ = self.inner α γ + self.inner β γ
• inner_smul_left {k : ℕ} (r : ℝ) (α β : DiffForm n k) : self.inner (r • α) β = r * self.inner α β

@[reducible, inline]

abbrev HodgeMathlib.MultiIndex (n : ℕ) : Type

A multi-index $\alpha = (\alpha_1, \dots, \alpha_n) \in \mathbb{N}^n$, indexing partial derivatives.

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

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

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

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

noncomputable def HodgeMathlib.constMultiIndex (n k : ℕ) : MultiIndex n

The constant multi-index whose every entry equals $k$.

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

The finite set of multi-indices componentwise bounded by $(k, \dots, k)$.

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

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

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

The finite set of multi-indices with total degree at most $k$.

noncomputable def HodgeMathlib.principalSymbolDiffForm {n : ℕ} (ord : ℕ) (coeff : {k : ℕ} → MultiIndex n → DiffForm n (k + 1) → DiffForm n (k + 1)) (ξ : Fin n → ℝ) {k : ℕ} (s : DiffForm n (k + 1)) : DiffForm n (k + 1)

The principal symbol of a differential operator: $\sigma(L)(\xi) = \sum_{|\alpha| = \mathrm{ord}} a_\alpha \, \xi^\alpha$.

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

Data witnessing that $L$ is a linear differential operator of given order with coefficients $a_\alpha$ and local expression $L = \sum_{|\alpha| \le \mathrm{ord}} a_\alpha \partial^\alpha$.

• order : ℕ
• coeff {k : ℕ} : MultiIndex n → DiffForm n (k + 1) → DiffForm n (k + 1)
• coeff_support (α : MultiIndex n) : multiIndexDegree α > self.order → ∀ {k : ℕ} (ω : DiffForm n (k + 1)), self.coeff α ω = 0
• partialDeriv {k : ℕ} : MultiIndex n → DiffForm n (k + 1) → DiffForm n (k + 1)
• local_expression {k : ℕ} (s : DiffForm n (k + 1)) : L s = ∑ α ∈ multiIndicesOfDegreeLE n self.order, self.coeff α (self.partialDeriv α s)
• L_add {k : ℕ} (α β : DiffForm n (k + 1)) : L (α + β) = L α + L β
• L_smul {k : ℕ} (r : ℝ) (α : DiffForm n (k + 1)) : L (r • α) = r • L α

noncomputable def HodgeMathlib.IsDifferentialOperator.symbol {n : ℕ} {L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)} (hL : IsDifferentialOperator fun {k : ℕ} => L) (ξ : Fin n → ℝ) {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)

The principal symbol $\sigma(L)(\xi)$ of a differential operator $L$, extracted from its top-order coefficients.

structure HodgeMathlib.IsElliptic {n : ℕ} (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) extends HodgeMathlib.IsDifferentialOperator fun {k : ℕ} => L : Type

A differential operator $L$ is elliptic if its principal symbol $\sigma(L)(\xi)$ is bijective for every nonzero covector $\xi$.

• order : ℕ
• coeff {k : ℕ} : MultiIndex n → DiffForm n (k + 1) → DiffForm n (k + 1)
• coeff_support (α : MultiIndex n) : multiIndexDegree α > self.order → ∀ {k : ℕ} (ω : DiffForm n (k + 1)), self.coeff α ω = 0
• partialDeriv {k : ℕ} : MultiIndex n → DiffForm n (k + 1) → DiffForm n (k + 1)
• local_expression {k : ℕ} (s : DiffForm n (k + 1)) : L s = ∑ α ∈ multiIndicesOfDegreeLE n self.order, self.coeff α (self.partialDeriv α s)
• L_add {k : ℕ} (α β : DiffForm n (k + 1)) : L (α + β) = L α + L β
• L_smul {k : ℕ} (r : ℝ) (α : DiffForm n (k + 1)) : L (r • α) = r • L α
• elliptic (ξ : Fin n → ℝ) : ξ ≠ 0 → ∀ {k : ℕ}, Function.Bijective (principalSymbolDiffForm self.order (fun {k : ℕ} => self.coeff) ξ)

theorem HodgeMathlib.IsElliptic.symbol_injective {n : ℕ} {L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)} (hL : IsElliptic fun {k : ℕ} => L) (ξ : Fin n → ℝ) (hξ : ξ ≠ 0) {k : ℕ} : Function.Injective (principalSymbolDiffForm hL.order (fun {k : ℕ} => hL.coeff) ξ)

The principal symbol of an elliptic operator is injective at every nonzero covector.

structure HodgeMathlib.IsSmoothingOp {n k : ℕ} (sobolevNorm : ℕ → DiffForm n (k + 1) → ℝ) (S : DiffForm n (k + 1) →ₗ[ℝ] DiffForm n (k + 1)) : Prop

A smoothing operator: gains one Sobolev derivative, $\|S\,x\|_{s+1} \le C\,\|x\|_s$.

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

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

A parametrix for $L$: an operator $P$ with $PL = I + S_{\mathrm{left}}$ and $LP = I + S_{\mathrm{right}}$ modulo smoothing operators.

• P {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)
• S_left {k : ℕ} : DiffForm n (k + 1) →ₗ[ℝ] DiffForm n (k + 1)
• S_right {k : ℕ} : DiffForm n (k + 1) →ₗ[ℝ] DiffForm n (k + 1)
• sobolevNorm {k : ℕ} : ℕ → DiffForm n (k + 1) → ℝ
• PL_eq {k : ℕ} (α : DiffForm n (k + 1)) : self.P (L α) = α + self.S_left α
• LP_eq {k : ℕ} (α : DiffForm n (k + 1)) : L (self.P α) = α + self.S_right α
• isSmoothing_S_left {k : ℕ} : IsSmoothingOp self.sobolevNorm self.S_left
• isSmoothing_S_right {k : ℕ} : IsSmoothingOp self.sobolevNorm self.S_right

class HodgeMathlib.HasSobolevSpaces (n : ℕ) : Type

Typeclass providing a Sobolev regularity predicate $H^s$ on differential forms.

• IsSobolevRegular : ℕ → {k : ℕ} → DiffForm n (k + 1) → Prop

theorem HodgeMathlib.elliptic_has_parametrix {n : ℕ} (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (hL : IsElliptic fun {k : ℕ} => L) : Nonempty (HasParametrix fun {k : ℕ} => L)

Every elliptic operator on differential forms admits a parametrix.

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

A Green operator decomposition: operators $G$ and $H$ with $LG = I - H$, $GL = I - H$, where $H$ projects onto $\ker L$.

• G {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)
• H {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)
• H_maps_to_ker {k : ℕ} (α : DiffForm n (k + 1)) : L (self.H α) = 0
• LG_eq {k : ℕ} (α : DiffForm n (k + 1)) : L (self.G α) = α + -self.H α
• GL_eq {k : ℕ} (α : DiffForm n (k + 1)) : self.G (L α) = α + -self.H α
• H_idem {k : ℕ} (α : DiffForm n (k + 1)) : self.H (self.H α) = self.H α

theorem HodgeMathlib.green_operator_decomposition {n : ℕ} (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (hL : IsElliptic fun {k : ℕ} => L) (cod : Codifferential n) (ip : L2InnerProduct cod) (self_adj : ∀ {k : ℕ} (α β : DiffForm n (k + 1)), ip.inner (L α) β = ip.inner α (L β)) : Nonempty (HasGreenOperatorDecomp fun {k : ℕ} => L)

A self-adjoint elliptic operator admits a Green operator decomposition $LG = I - H$ with harmonic projector $H$.

theorem HodgeMathlib.hodge_decomposition_three_way {n : ℕ} (cod : Codifferential n) (h_green : Nonempty (HasGreenOperatorDecomp fun {k : ℕ} (α : DiffForm n (k + 1)) => laplacian cod α)) {k : ℕ} (α : DiffForm n (k + 1)) : ∃ (h : DiffForm n (k + 1)) (β : DiffForm n k) (γ : DiffForm n (k + 2)), IsHarmonic cod h ∧ α = h + dForm β + cod.dstar γ

Hodge decomposition: every form $\alpha$ splits as $\alpha = h + d\beta + d^*\gamma$ with $h$ harmonic.

theorem HodgeMathlib.hodge_representative {n : ℕ} (cod : Codifferential n) (ip : L2InnerProduct cod) (h_green : Nonempty (HasGreenOperatorDecomp fun {k : ℕ} (α : DiffForm n (k + 1)) => laplacian cod α)) {k : ℕ} (α : DiffForm n (k + 1)) (hclosed : dForm α = 0) : ∃ (h : DiffForm n (k + 1)) (β : DiffForm n k), IsHarmonic cod h ∧ α = h + dForm β

Hodge theorem: every closed form $\alpha$ is cohomologous to a unique harmonic representative $h$, i.e. $\alpha = h + d\beta$.

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

A differential form is smooth if it is $C^\infty$ as a function.

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

The difference of two smooth forms is smooth.

theorem HodgeMathlib.elliptic_regularity {n : ℕ} [sob : HasSobolevSpaces n] (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (param : HasParametrix fun {k : ℕ} => L) (P_preserves_smooth : ∀ {k : ℕ} (β : DiffForm n (k + 1)), IsSmoothForm β → IsSmoothForm (param.P β)) (S_left_maps_sobolev_to_smooth : ∀ (s : ℕ) {k : ℕ} (α : DiffForm n (k + 1)), HasSobolevSpaces.IsSobolevRegular s α → IsSmoothForm (param.S_left α)) {k : ℕ} {ξ : DiffForm n (k + 1)} (s : ℕ) (hξ_sob : HasSobolevSpaces.IsSobolevRegular s ξ) (hLξ_smooth : IsSmoothForm (L ξ)) : IsSmoothForm ξ

Elliptic regularity: if $\xi$ is Sobolev-regular and $L\xi$ is smooth, then $\xi$ is smooth.

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

$L$ is Fredholm: there is a left parametrix $P$ with $PL = I + S_{\mathrm{left}}$, and the kernel of $L$ is finite-dimensional.

• P {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)
• S_left {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)
• PL_eq {k : ℕ} (α : DiffForm n (k + 1)) : self.P (L α) = α + self.S_left α
• ker_contained {k : ℕ} (α : DiffForm n (k + 1)) : L α = 0 → α + self.S_left α = self.P 0
• L_add {k : ℕ} (α β : DiffForm n (k + 1)) : L (α + β) = L α + L β
• L_smul {k : ℕ} (r : ℝ) (α : DiffForm n (k + 1)) : L (r • α) = r • L α

theorem HodgeMathlib.elliptic_kernel_finite_dim {n : ℕ} (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (hL : IsElliptic fun {k : ℕ} => L) (k : ℕ) : FiniteDimensional ℝ ↥{ toFun := L, map_add' := ⋯, map_smul' := ⋯ }.ker

The kernel of an elliptic operator on differential forms is finite-dimensional.

theorem HodgeMathlib.elliptic_cokernel_finite_dim {n : ℕ} (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (hL : IsElliptic fun {k : ℕ} => L) (k : ℕ) : FiniteDimensional ℝ (DiffForm n (k + 1) ⧸ { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range)

The cokernel of an elliptic operator on differential forms is finite-dimensional.

theorem HodgeMathlib.elliptic_regularity_unique {n : ℕ} (L : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (hL : IsElliptic fun {k : ℕ} => L) (cod : Codifferential n) (ip : L2InnerProduct cod) (L_star : {k : ℕ} → DiffForm n (k + 1) → DiffForm n (k + 1)) (h_adjoint : ∀ {k : ℕ} (α β : DiffForm n (k + 1)), ip.inner (L α) β = ip.inner α (L_star β)) {k : ℕ} (τ : DiffForm n (k + 1)) (h_orth_ker_star : ∀ (η : DiffForm n (k + 1)), L_star η = 0 → ip.inner τ η = 0) : ∃! ξ : DiffForm n (k + 1), L ξ = τ ∧ ∀ (η : DiffForm n (k + 1)), L η = 0 → ip.inner ξ η = 0

Unique solvability for elliptic equations: if $\tau \perp \ker L^*$, then $L\xi = \tau$ has a unique solution orthogonal to $\ker L$.

theorem HodgeMathlib.dolbeault_existence_bigraded {n k : ℕ} (delbar_k : DiffForm n k → DiffForm n (k + 1)) (delbar_k1 : DiffForm n (k + 1) → DiffForm n (k + 2)) (delbar_star_k1 : DiffForm n (k + 1) → DiffForm n k) (box_bar : DiffForm n (k + 1) → DiffForm n (k + 1)) (α : DiffForm n (k + 1)) (hclosed : delbar_k1 α = 0) : ∃ (h : DiffForm n (k + 1)) (β : DiffForm n k), box_bar h = 0 ∧ α = h + delbar_k β

Dolbeault Hodge theorem: every $\bar\partial$-closed form $\alpha$ decomposes as $\alpha = h + \bar\partial\beta$ with $h$ $\bar\square$-harmonic.