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

The space $\Omega^k(\mathbb{R}^n)$ of (continuous) differential $k$-forms on Euclidean $n$-space, modelled as maps from points to continuous alternating $k$-linear forms.

@[implicit_reducible]

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

Pointwise additive group structure on $k$-forms.

@[implicit_reducible]

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

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

structure DolbeaultHodgeMathlib.L2InnerProduct (n : ℕ) : Type

Axiomatic $L^2$ inner product on differential forms of each degree, satisfying positivity, symmetry, and bilinearity.

• 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 β α
• 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]

def DolbeaultHodgeMathlib.L2InnerProduct.toInner {n : ℕ} (ip : L2InnerProduct n) (k : ℕ) : Inner ℝ (DiffForm n k)

Mathlib Inner instance built from the axiomatic $L^2$ inner product.

@[reducible]

noncomputable def DolbeaultHodgeMathlib.L2InnerProduct.toPreCore {n : ℕ} (ip : L2InnerProduct n) (k : ℕ) : PreInnerProductSpace.Core ℝ (DiffForm n k)

Build a PreInnerProductSpace.Core from an L2InnerProduct, giving access to Mathlib's inner-product-space machinery.

@[reducible]

noncomputable def DolbeaultHodgeMathlib.L2InnerProduct.toSeminormedAddCommGroup {n : ℕ} (ip : L2InnerProduct n) (k : ℕ) : SeminormedAddCommGroup (DiffForm n k)

The seminormed group structure on $\Omega^k$ induced by the $L^2$ inner product.

@[reducible]

noncomputable def DolbeaultHodgeMathlib.L2InnerProduct.toInnerProductSpace {n : ℕ} (ip : L2InnerProduct n) (k : ℕ) : InnerProductSpace ℝ (DiffForm n k)

The Mathlib InnerProductSpace structure on $\Omega^k$ induced by the $L^2$ inner product.

theorem DolbeaultHodgeMathlib.L2InnerProduct.inner_eq_mathlibInner {n : ℕ} (ip : L2InnerProduct n) {k : ℕ} (α β : DiffForm n k) : ip.inner α β = Inner.inner ℝ α β

Compatibility: the explicit ip.inner equals the Mathlib-derived Inner.inner.

structure DolbeaultHodgeMathlib.DolbeaultData (n : ℕ) : Type

Axiomatic Dolbeault data: the operators $\bar\partial$, its formal adjoint $\bar\partial^*$, and the $\bar\partial$-Laplacian $\bar\square = \bar\partial \bar\partial^* + \bar\partial^* \bar\partial$, satisfying $\bar\partial^2 = 0$ and linearity.

• delbar {k : ℕ} : DiffForm n k → DiffForm n (k + 1)
• delbar_star {k : ℕ} : DiffForm n (k + 1) → DiffForm n k
• box_bar {k : ℕ} : DiffForm n (k + 1) → DiffForm n (k + 1)
• delbar_sq {k : ℕ} (α : DiffForm n k) : self.delbar (self.delbar α) = 0
• delbar_add {k : ℕ} (α β : DiffForm n k) : self.delbar (α + β) = self.delbar α + self.delbar β
• delbar_smul {k : ℕ} (r : ℝ) (α : DiffForm n k) : self.delbar (r • α) = r • self.delbar α
• box_bar_eq {k : ℕ} (α : DiffForm n (k + 1)) : self.box_bar α = self.delbar (self.delbar_star α) + self.delbar_star (self.delbar α)
• delbar_star_add {k : ℕ} (α β : DiffForm n (k + 1)) : self.delbar_star (α + β) = self.delbar_star α + self.delbar_star β
• delbar_star_smul {k : ℕ} (r : ℝ) (α : DiffForm n (k + 1)) : self.delbar_star (r • α) = r • self.delbar_star α

structure DolbeaultHodgeMathlib.HasDelbarAdjoint {n : ℕ} (ip : L2InnerProduct n) (dol : DolbeaultData n) : Prop

The adjointness relation $\langle \bar\partial \alpha, \beta \rangle = \langle \alpha, \bar\partial^* \beta \rangle$ between $\bar\partial$ and $\bar\partial^*$.

• adj {k : ℕ} (α : DiffForm n k) (β : DiffForm n (k + 1)) : ip.inner (dol.delbar α) β = ip.inner α (dol.delbar_star β)

theorem DolbeaultHodgeMathlib.harmonic_is_delbar_closed {n : ℕ} (ip : L2InnerProduct n) (dol : DolbeaultData n) (hadj : HasDelbarAdjoint ip dol) {k : ℕ} (h : DiffForm n (k + 1)) (hBox : dol.box_bar h = 0) : dol.delbar h = 0

A $\bar\square$-harmonic form is $\bar\partial$-closed: $\bar\square h = 0 \Rightarrow \bar\partial h = 0$.

theorem DolbeaultHodgeMathlib.harmonic_is_delbar_star_zero {n : ℕ} (ip : L2InnerProduct n) (dol : DolbeaultData n) (hadj : HasDelbarAdjoint ip dol) {k : ℕ} (h : DiffForm n (k + 1)) (hBox : dol.box_bar h = 0) : dol.delbar_star h = 0

A $\bar\square$-harmonic form is annihilated by $\bar\partial^*$: $\bar\square h = 0 \Rightarrow \bar\partial^* h = 0$.

theorem DolbeaultHodgeMathlib.box_bar_harmonic_unique {n : ℕ} (ip : L2InnerProduct n) (dol : DolbeaultData n) (hadj : HasDelbarAdjoint ip dol) {k : ℕ} (h₁ h₂ : DiffForm n (k + 1)) (hHarm₁ : dol.box_bar h₁ = 0) (hHarm₂ : dol.box_bar h₂ = 0) (a b : DiffForm n k) (hcohom : h₁ + dol.delbar a = h₂ + dol.delbar b) : h₁ = h₂

Uniqueness of the harmonic representative: if $h_1 + \bar\partial a = h_2 + \bar\partial b$ with $h_1, h_2$ both $\bar\square$-harmonic, then $h_1 = h_2$.

theorem DolbeaultHodgeMathlib.dolbeault_existence {n k : ℕ} (ip : L2InnerProduct n) (dol : DolbeaultData n) (hadj : HasDelbarAdjoint ip dol) (α : DiffForm n (k + 1)) (hclosed : dol.delbar α = 0) : ∃ (h : DiffForm n (k + 1)) (β : DiffForm n k), dol.box_bar h = 0 ∧ α = h + dol.delbar β

Existence in Hodge–Dolbeault decomposition: every $\bar\partial$-closed form $\alpha$ has a decomposition $\alpha = h + \bar\partial \beta$ with $h$ harmonic ($\bar\square h = 0$).

theorem DolbeaultHodgeMathlib.dolbeault_cohomology_iso_harmonic {n : ℕ} (ip : L2InnerProduct n) (dol : DolbeaultData n) (hadj : HasDelbarAdjoint ip dol) (k : ℕ) : (∀ (α : DiffForm n (k + 1)), dol.delbar α = 0 → ∃! h : DiffForm n (k + 1), dol.box_bar h = 0 ∧ ∃ (β : DiffForm n k), α = h + dol.delbar β) ∧ (∀ (h : DiffForm n (k + 1)), dol.box_bar h = 0 → dol.delbar h = 0) ∧ (∀ (h₁ h₂ : DiffForm n (k + 1)), dol.box_bar h₁ = 0 → dol.box_bar h₂ = 0 → ∀ (a b : DiffForm n k), h₁ + dol.delbar a = h₂ + dol.delbar b → h₁ = h₂) ∧ ∀ (h : DiffForm n (k + 1)), dol.box_bar h = 0 → ∃ (β : DiffForm n k), h = h + dol.delbar β

Dolbeault cohomology is isomorphic to harmonic forms: $H^{p,q}_{\bar\partial}(M) \cong \mathcal{H}^{p,q}_{\bar\square}$ — existence and uniqueness of harmonic representative, harmonic implies $\bar\partial$-closed, and trivial-coboundary witness.