structure HasComplexStructure {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

A complex-linear structure on the spaces of differential forms.

Equips each $\Omega^p$ with a scalar multiplication by $\mathbb{C}$ compatible with the existing $\mathbb{R}$-module structure.

• complexSmul {p : ℕ} : ℂ → Ω p → Ω p
• complexSmul_add {p : ℕ} (z : ℂ) (ω₁ ω₂ : Ω p) : self.complexSmul z (ω₁ + ω₂) = self.complexSmul z ω₁ + self.complexSmul z ω₂
• complexSmul_zero {p : ℕ} (ω : Ω p) : self.complexSmul 0 ω = 0
• complexSmul_mul {p : ℕ} (z w : ℂ) (ω : Ω p) : self.complexSmul z (self.complexSmul w ω) = self.complexSmul (z * w) ω
• complexSmul_one {p : ℕ} (ω : Ω p) : self.complexSmul 1 ω = ω
• complexSmul_real {p : ℕ} (r : ℝ) (ω : Ω p) : self.complexSmul (↑r) ω = r • ω

structure HodgeStar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

The Hodge star operator $*: \Omega^p \to \Omega^p$ (a simplified involution version); on an oriented Riemannian $n$-manifold it normally maps $\Omega^k \to \Omega^{n-k}$.

• star {p : ℕ} : Ω p → Ω p
• star_star {p : ℕ} (α : Ω p) : self.star (self.star α) = α

structure Codifferential {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

The codifferential $d^*: \Omega^k \to \Omega^{k-1}$, the formal $L^2$-adjoint of $d$.

On an oriented Riemannian $n$-manifold, $d^* = (-1)^{n(k-1)+1} * d *$ where $*$ is the Hodge star and the sign factor satisfies $(\text{sign})^2 = 1$.

• dstar {p : ℕ} : Ω (p + 1) → Ω p
• dstar_add {p : ℕ} (α β : Ω (p + 1)) : self.dstar (α + β) = self.dstar α + self.dstar β
• dstar_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : self.dstar (r • α) = r • self.dstar α
• hodge : HodgeStar
• sign_factor : ℕ → ℝ
• sign_factor_sq (k : ℕ) : self.sign_factor k ^ 2 = 1
• manifold_dim : ℕ
• sign_factor_formula (k : ℕ) : self.sign_factor k = (-1) ^ (self.manifold_dim * (k - 1) + 1)
• star_deg {k : ℕ} : k ≤ self.manifold_dim → Ω k → Ω (self.manifold_dim - k)
• star_deg_star_deg {k : ℕ} (hk : k ≤ self.manifold_dim) (hk' : self.manifold_dim - k ≤ self.manifold_dim := by omega) (α : Ω k) : cast ⋯ (self.star_deg hk' (self.star_deg hk α)) = α
• dstar_formula {p : ℕ} (h : p + 1 ≤ self.manifold_dim) (ω : Ω (p + 1)) : self.dstar ω = self.sign_factor (p + 1) • cast ⋯ (self.star_deg ⋯ (DifferentialFormSpace.d VF (self.star_deg h ω)))
• dstar_squared {p : ℕ} (ω : Ω (p + 2)) : self.dstar (self.dstar ω) = 0

theorem Codifferential.formula {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (h : p + 1 ≤ cod.manifold_dim) (ω : Ω (p + 1)) : cod.dstar ω = cod.sign_factor (p + 1) • cast ⋯ (cod.star_deg ⋯ (DifferentialFormSpace.d VF (cod.star_deg h ω)))

Restates the explicit formula $d^*\omega = (-1)^{n(k-1)+1} * d * \omega$ for the codifferential in terms of the Hodge star, packaged from the structure data.

def star_d_star {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (h : p + 1 ≤ cod.manifold_dim) (ω : Ω (p + 1)) : Ω p

The composite $* \circ d \circ *: \Omega^{p+1} \to \Omega^p$ (without the sign factor), the geometric content of the codifferential.

def laplacian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Ω (p + 1)

The Hodge–de Rham Laplacian $\Delta = dd^* + d^*d: \Omega^k \to \Omega^k$.

def IsHarmonic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Prop

A form $\alpha$ is harmonic if $\Delta \alpha = 0$.

@[reducible, inline]

abbrev IsHarmonicForm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Prop

Synonym for IsHarmonic: the form $\alpha$ is harmonic.

def HarmonicForms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (p : ℕ) : Set (Ω (p + 1))

The space $\mathcal{H}^{p+1} = \{\alpha \in \Omega^{p+1} : \Delta \alpha = 0\}$ of harmonic forms of degree $p+1$.

structure L2InnerProduct {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) : Type u_1

The $L^2$ inner product on differential forms: a symmetric, positive-definite, $\mathbb{R}$-bilinear form $\langle \cdot, \cdot \rangle$ on each $\Omega^p$ for which $d$ and $d^*$ are mutually adjoint, i.e. $\langle d\alpha, \beta\rangle = \langle \alpha, d^*\beta\rangle$.

• inner {p : ℕ} : Ω p → Ω p → ℝ
• inner_self_eq_zero {p : ℕ} (α : Ω p) : self.inner α α = 0 → α = 0
• inner_self_nonneg {p : ℕ} (α : Ω p) : 0 ≤ self.inner α α
• inner_symm {p : ℕ} (α β : Ω p) : self.inner α β = self.inner β α
• adjoint_d {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : self.inner (DifferentialFormSpace.d VF α) β = self.inner α (cod.dstar β)
• inner_add_left {p : ℕ} (α β γ : Ω p) : self.inner (α + β) γ = self.inner α γ + self.inner β γ
• inner_smul_left {p : ℕ} (r : ℝ) (α β : Ω p) : self.inner (r • α) β = r * self.inner α β

noncomputable def L2InnerProduct.toInner {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {cod : Codifferential} (ip : L2InnerProduct cod) (p : ℕ) : Inner ℝ (Ω p)

Packages the $L^2$ inner product as a Mathlib Inner ℝ instance on $\Omega^p$.

theorem L2InnerProduct.inner_product_axioms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {cod : Codifferential} (ip : L2InnerProduct cod) {p : ℕ} : (∀ (α β : Ω p), ip.inner α β = ip.inner β α) ∧ (∀ (α β γ : Ω p), ip.inner (α + β) γ = ip.inner α γ + ip.inner β γ) ∧ (∀ (r : ℝ) (α β : Ω p), ip.inner (r • α) β = r * ip.inner α β) ∧ (∀ (α : Ω p), 0 ≤ ip.inner α α) ∧ ∀ (α : Ω p), ip.inner α α = 0 → α = 0

The $L^2$ inner product satisfies the standard inner-product axioms: symmetry, additivity in the first slot, scalar homogeneity, non-negativity and positive-definiteness.

theorem Codifferential.dstar_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} : cod.dstar 0 = 0

The codifferential vanishes on zero: $d^*(0) = 0$.

theorem L2InnerProduct.inner_zero_left {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {cod : Codifferential} (ip : L2InnerProduct cod) {p : ℕ} (α : Ω p) : ip.inner 0 α = 0

The $L^2$ inner product vanishes when its first argument is zero: $\langle 0, \alpha\rangle = 0$.

theorem harmonic_iff_closed_coclosed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (α : Ω (p + 1)) : IsHarmonic cod α ↔ DifferentialFormSpace.d VF α = 0 ∧ cod.dstar α = 0

On a compact oriented Riemannian manifold, a form $\alpha$ is harmonic iff it is both closed and coclosed: $\Delta\alpha = 0 \iff d\alpha = 0 \text{ and } d^*\alpha = 0$.

structure DolbeaultLaplacian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) (cod : Codifferential) : Type u_1

Auxiliary data packaging the formal adjoints $\partial^*$ and $\bar\partial^*$ together with the decomposition $d^* = \partial^* + \bar\partial^*$.

• del_star {p : ℕ} : Ω (p + 1) → Ω p
• delbar_star {p : ℕ} : Ω (p + 1) → Ω p
• dstar_decomp {p : ℕ} (ω : Ω (p + 1)) : cod.dstar ω = self.del_star ω + self.delbar_star ω
• delbar_star_add {p : ℕ} (α β : Ω (p + 1)) : self.delbar_star (α + β) = self.delbar_star α + self.delbar_star β
• delbar_star_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : self.delbar_star (r • α) = r • self.delbar_star α

def DolbeaultLaplacian.box_bar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) {p : ℕ} (α : Ω (p + 1)) : Ω (p + 1)

The $\bar\partial$-Laplacian $\bar\square = \bar\partial\bar\partial^* + \bar\partial^*\bar\partial$ on $(p,q)$-forms.

def DolbeaultLaplacian.box {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) {p : ℕ} (α : Ω (p + 1)) : Ω (p + 1)

The $\partial$-Laplacian $\square = \partial\partial^* + \partial^*\partial$.

structure KahlerWellsIdentities {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) : Prop

Wells' anticommutation identities for the Dolbeault adjoint operators on a Kähler manifold: $\partial\bar\partial^* + \bar\partial^*\partial = 0$ and $\bar\partial\partial^* + \partial^*\bar\partial = 0$, plus an expansion identity.

• del_delbar_star_anticommute {p : ℕ} (α : Ω (p + 1)) : dol.del (dol_lap.delbar_star α) + dol_lap.delbar_star (dol.del α) = 0
• delbar_del_star_anticommute {p : ℕ} (α : Ω (p + 1)) : dol.delbar (dol_lap.del_star α) + dol_lap.del_star (dol.delbar α) = 0
• wells_expansion {p : ℕ} (α : Ω (p + 1)) : dol.del (dol_lap.del_star α) + dol_lap.del_star (dol.del α) + (dol.del (dol_lap.delbar_star α) + dol_lap.delbar_star (dol.del α)) - (dol.delbar (dol_lap.del_star α) + dol_lap.del_star (dol.delbar α)) - (dol.delbar (dol_lap.delbar_star α) + dol_lap.delbar_star (dol.delbar α)) = 0

theorem kahler_box_eq_box_bar_blocker {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (del_star delbar_star : {p : ℕ} → Ω (p + 1) → Ω p) (box box_bar : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hbox_def : ∀ {p : ℕ} (α : Ω (p + 1)), box α = dol.del (del_star α) + del_star (dol.del α)) (hbox_bar_def : ∀ {p : ℕ} (α : Ω (p + 1)), box_bar α = dol.delbar (delbar_star α) + delbar_star (dol.delbar α)) (wells : KahlerWellsIdentities S J _hK dol_lap) (h_del_star : ∀ {p : ℕ} (α : Ω (p + 1)), del_star α = dol_lap.del_star α) (h_delbar_star : ∀ {p : ℕ} (α : Ω (p + 1)), delbar_star α = dol_lap.delbar_star α) {p : ℕ} (α : Ω (p + 1)) : box α = box_bar α

On a Kähler manifold, the two Dolbeault Laplacians agree: $\square = \bar\square$.

Auxiliary version using abstract box, box_bar, del_star, delbar_star parameters together with Wells' identities.

theorem kahler_del_delbar_star_anticommute_blocker {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (wells : KahlerWellsIdentities S J _hK dol_lap) {p : ℕ} (α : Ω (p + 1)) : dol.del (dol_lap.delbar_star α) + dol_lap.delbar_star (dol.del α) = 0

Extracts the Wells anticommutation $\partial \bar\partial^* + \bar\partial^* \partial = 0$ from the structure of Kähler identities.

theorem kahler_delbar_del_star_anticommute_blocker {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (wells : KahlerWellsIdentities S J _hK dol_lap) {p : ℕ} (α : Ω (p + 1)) : dol.delbar (dol_lap.del_star α) + dol_lap.del_star (dol.delbar α) = 0

Extracts the Wells anticommutation $\bar\partial \partial^* + \partial^* \bar\partial = 0$ from the structure of Kähler identities.

theorem kahler_two_box_bar_blocker {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (wells : KahlerWellsIdentities S J _hK dol_lap) {p : ℕ} (α : Ω (p + 1)) : dol_lap.box_bar α + dol_lap.box_bar α = laplacian cod α

On a Kähler manifold, $\Delta = 2\bar\square$ acting on $(p,q)$-forms; concretely $\bar\square \alpha + \bar\square \alpha = \Delta \alpha$.

theorem box_bar_eq_half_laplacian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (_S : SymplecticManifold Ω VF) (_J : AlmostComplexStr) (_hK : IsKahler _S _J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (h_two_box_bar : ∀ {p : ℕ} (α : Ω (p + 1)), dol_lap.box_bar α + dol_lap.box_bar α = laplacian cod α) {p : ℕ} (α : Ω (p + 1)) : dol_lap.box_bar α + dol_lap.box_bar α = laplacian cod α

Restatement of $2\bar\square = \Delta$ on Kähler manifolds (given as a hypothesis here) in the form $\bar\square \alpha + \bar\square \alpha = \Delta \alpha$.

theorem kahler_laplacian_eq_box_plus_box_bar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (_S : SymplecticManifold Ω VF) (_J : AlmostComplexStr) (_hK : IsKahler _S _J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (h_del_delbar_star : ∀ {p : ℕ} (α : Ω (p + 1)), dol.del (dol_lap.delbar_star α) + dol_lap.delbar_star (dol.del α) = 0) (h_delbar_del_star : ∀ {p : ℕ} (α : Ω (p + 1)), dol.delbar (dol_lap.del_star α) + dol_lap.del_star (dol.delbar α) = 0) {p : ℕ} (α : Ω (p + 1)) : laplacian cod α = dol_lap.box α + dol_lap.box_bar α

On a Kähler manifold, $\Delta = \square + \bar\square$ as a consequence of the anticommutation identities for the Dolbeault adjoints.

theorem box_eq_box_bar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) {dol : DolbeaultOps} {cod : Codifferential} (dol_lap : DolbeaultLaplacian dol cod) (h_del_delbar_star : ∀ {p : ℕ} (α : Ω (p + 1)), dol.del (dol_lap.delbar_star α) + dol_lap.delbar_star (dol.del α) = 0) (h_delbar_del_star : ∀ {p : ℕ} (α : Ω (p + 1)), dol.delbar (dol_lap.del_star α) + dol_lap.del_star (dol.delbar α) = 0) (h_two_box_bar : ∀ {p : ℕ} (α : Ω (p + 1)), dol_lap.box_bar α + dol_lap.box_bar α = laplacian cod α) {p : ℕ} (α : Ω (p + 1)) : dol_lap.box α = dol_lap.box_bar α

On a Kähler manifold the two Dolbeault Laplacians are equal: $\square = \bar\square$, deduced from $\Delta = \square + \bar\square$ and $\Delta = 2\bar\square$.

theorem kahler_laplacian_identity {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (wells : KahlerWellsIdentities S J _hK dol_lap) {p : ℕ} (α : Ω (p + 1)) : laplacian cod α = dol_lap.box α + dol_lap.box α ∧ laplacian cod α = dol_lap.box_bar α + dol_lap.box_bar α ∧ dol_lap.box α = dol_lap.box_bar α

The Kähler Laplacian identity: $\Delta = 2\square = 2\bar\square$ and $\square = \bar\square$ on a Kähler manifold, packaged together.

structure HasBigrading {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (J : AlmostComplexStr) (n : ℕ) : Type (max u_1 (u_3 + 1))

The Hodge bigrading on an almost-complex manifold of complex dimension $n$: a decomposition $\Omega^k = \bigoplus_{p+q=k} \Omega^{p,q}$ with the Hodge star acting as $* : \Omega^{p,q} \to \Omega^{n-q, n-p}$.

• Ω_pq : ℕ → ℕ → Type u_3
• incl (p q : ℕ) : self.Ω_pq p q → Ω (p + q)
• incl_injective (p q : ℕ) : Function.Injective (self.incl p q)
• pq_add (p q : ℕ) : self.Ω_pq p q → self.Ω_pq p q → self.Ω_pq p q
• incl_add (p q : ℕ) (α β : self.Ω_pq p q) : self.incl p q (self.pq_add p q α β) = self.incl p q α + self.incl p q β
• pq_zero (p q : ℕ) : self.Ω_pq p q
• incl_zero (p q : ℕ) : self.incl p q (self.pq_zero p q) = 0
• incl_cast {p₁ q₁ p₂ q₂ : ℕ} (hp : p₁ = p₂) (hq : q₁ = q₂) (α : self.Ω_pq p₁ q₁) : self.incl p₂ q₂ (cast ⋯ α) = cast ⋯ (self.incl p₁ q₁ α)
• star_total {k : ℕ} : k ≤ 2 * n → Ω k → Ω (2 * n - k)
• star_abc_decomp {p' q' : ℕ} (hp' : p' ≤ n) (hq' : q' ≤ n) (β : self.Ω_pq p' q') : ∃ (a : ℕ) (b : ℕ) (c : ℕ) (ha : a + c = p') (hb : b + c = q') (habc : a + b + c ≤ n) (γ : self.Ω_pq (a + (n - a - b - c)) (b + (n - a - b - c))), self.incl (a + (n - a - b - c)) (b + (n - a - b - c)) γ = cast ⋯ (self.star_total ⋯ (self.incl p' q' β))

structure KahlerBigradedData {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) : Prop

Data witnessing that on a Kähler manifold, $\bar\square$ and $\Delta$ preserve the $(p,q)$ bigrading, and that every harmonic form decomposes into harmonic $(p,q)$-components.

• box_bar_preserves_bidegree (k p' q' : ℕ) (h : p' + q' = k + 1) (ω : bg.Ω_pq p' q') : ∃ (ω' : bg.Ω_pq p' q'), cast ⋯ (bg.incl p' q' ω') = dol_lap.box_bar (cast ⋯ (bg.incl p' q' ω))
• laplacian_preserves_bidegree (k p' q' : ℕ) (h : p' + q' = k + 1) (ω : bg.Ω_pq p' q') : ∃ (ω' : bg.Ω_pq p' q'), cast ⋯ (bg.incl p' q' ω') = laplacian cod (cast ⋯ (bg.incl p' q' ω))
• harmonic_bigrading_decomposition {k : ℕ} (h_form : Ω (k + 1)) (_h_harmonic : laplacian cod h_form = 0) : ∃ (component : Fin (k + 2) → Ω (k + 1)), (∀ (j : Fin (k + 2)), ∃ (ω : bg.Ω_pq (↑j) (k + 1 - ↑j)), cast ⋯ (bg.incl (↑j) (k + 1 - ↑j) ω) = component j) ∧ (∀ (j : Fin (k + 2)), dol.del (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol.delbar (component j) = 0) ∧ (∀ (j : Fin (k + 2)), laplacian cod (component j) = 0) ∧ h_form = Finset.univ.sum component

theorem laplacian_preserves_bidegree {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J' : AlmostComplexStr) (hK : IsKahler S J') (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) (h_box_bar_pres : ∀ (k p' q' : ℕ) (h : p' + q' = k + 1) (ω : bg.Ω_pq p' q'), ∃ (ω' : bg.Ω_pq p' q'), cast ⋯ (bg.incl p' q' ω') = dol_lap.box_bar (cast ⋯ (bg.incl p' q' ω))) (h_two_box_bar : ∀ {p : ℕ} (α : Ω (p + 1)), dol_lap.box_bar α + dol_lap.box_bar α = laplacian cod α) (k p' q' : ℕ) (h : p' + q' = k + 1) (ω : bg.Ω_pq p' q') : ∃ (ω' : bg.Ω_pq p' q'), cast ⋯ (bg.incl p' q' ω') = laplacian cod (cast ⋯ (bg.incl p' q' ω))

On a Kähler manifold, the Laplacian $\Delta$ preserves the Hodge $(p,q)$ bigrading, deduced from the fact that $\bar\square$ preserves it and $\Delta = 2\bar\square$.

theorem dolbeault_identification {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (h_two_box_bar : ∀ {p : ℕ} (α : Ω (p + 1)), dol_lap.box_bar α + dol_lap.box_bar α = laplacian cod α) {k : ℕ} (α : Ω (k + 1)) : laplacian cod α = 0 ↔ dol_lap.box_bar α = 0

On a Kähler manifold a form is $\Delta$-harmonic iff it is $\bar\square$-harmonic: $\Delta \alpha = 0 \iff \bar\square \alpha = 0$. This gives the identification $\mathcal{H}^k = \bigoplus_{p+q=k} \mathcal{H}^{p,q}_{\bar\square}$.

structure LefschetzOp {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type u_1

The Lefschetz operator $L: \Omega^p \to \Omega^{p+2}$, $\alpha \mapsto \omega \wedge \alpha$ on a symplectic manifold; it commutes with $d$.

• L_op {p : ℕ} : Ω p → Ω (p + 2)
• d_commutes {p : ℕ} (α : Ω p) : self.L_op (DifferentialFormSpace.d VF α) = DifferentialFormSpace.d VF (self.L_op α)

structure DualLefschetz {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

The dual Lefschetz operator $\Lambda = L^*: \Omega^{p+2} \to \Omega^p$, the formal $L^2$-adjoint of $L$.

• Λ_op {p : ℕ} : Ω (p + 2) → Ω p

structure JActsOnForms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (J : AlmostComplexStr) : Type u_1

An action of the almost-complex structure $J$ on differential forms: an $\mathbb{R}$-linear involution-up-to-sign $J: \Omega^p \to \Omega^p$ with $J^2 = -\mathrm{id}$.

• J_form {p : ℕ} : Ω p → Ω p
• J_form_sq {p : ℕ} (α : Ω p) : self.J_form (self.J_form α) = -α
• J_form_add {p : ℕ} (α β : Ω p) : self.J_form (α + β) = self.J_form α + self.J_form β
• J_form_smul {p : ℕ} (r : ℝ) (α : Ω p) : self.J_form (r • α) = r • self.J_form α

theorem JActsOnForms.J_form_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) {p : ℕ} (α : Ω p) : Jf.J_form (-α) = -Jf.J_form α

The action of $J$ on forms commutes with negation: $J(-\alpha) = -J(\alpha)$.

theorem JActsOnForms.J_form_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) {p : ℕ} : Jf.J_form 0 = 0

The action of $J$ on forms preserves zero: $J(0) = 0$.

noncomputable def d_C_form {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) {p : ℕ} (α : Ω p) : Ω (p + 1)

The twisted differential $d_C = -J d J: \Omega^p \to \Omega^{p+1}$ associated to an action of $J$ on forms.

noncomputable def d_C_star_form {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Ω p

The codifferential twisted by $J$: $d_C^* = -J d^* J: \Omega^{p+1} \to \Omega^p$.

theorem JActsOnForms.laplacian_commutes_J {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) (cod : Codifferential) (d_commutes_J : ∀ {p : ℕ} (α : Ω p), DifferentialFormSpace.d VF (Jf.J_form α) = Jf.J_form (DifferentialFormSpace.d VF α)) (dstar_commutes_J : ∀ {p : ℕ} (α : Ω (p + 1)), cod.dstar (Jf.J_form α) = Jf.J_form (cod.dstar α)) {p : ℕ} (α : Ω (p + 1)) : laplacian cod (Jf.J_form α) = Jf.J_form (laplacian cod α)

If $d$ and $d^*$ both commute with $J$ on forms, then so does the Laplacian: $\Delta(J\alpha) = J(\Delta \alpha)$.

theorem kahler_identity_Lstar_dstar_commute {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (lef : LefschetzOp S) (cod : Codifferential) (ip : L2InnerProduct cod) (dl : DualLefschetz) (adjoint_L : ∀ {q : ℕ} (γ : Ω q) (δ : Ω (q + 2)), ip.inner (lef.L_op γ) δ = ip.inner γ (dl.Λ_op δ)) {p : ℕ} (α : Ω (p + 3)) : dl.Λ_op (cod.dstar α) = cod.dstar (dl.Λ_op α)

The Kähler identity $[\Lambda, d^*] = 0$: the dual Lefschetz operator commutes with the codifferential, $\Lambda \circ d^* = d^* \circ \Lambda$. Proved from $[L, d] = 0$ by taking $L^2$-adjoints.

theorem kahler_identities_all_four {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (Jf : JActsOnForms J) (lef : LefschetzOp S) (cod : Codifferential) (ip : L2InnerProduct cod) (dl : DualLefschetz) (adjoint_L : ∀ {q : ℕ} (γ : Ω q) (δ : Ω (q + 2)), ip.inner (lef.L_op γ) δ = ip.inner γ (dl.Λ_op δ)) (identity3_L_dstar : ∀ {p : ℕ} (α : Ω (p + 1)), lef.L_op (cod.dstar α) + -cod.dstar (lef.L_op α) = d_C_form Jf α) (identity4_Λ_d : ∀ {p : ℕ} (α : Ω (p + 2)), dl.Λ_op (DifferentialFormSpace.d VF α) + -DifferentialFormSpace.d VF (dl.Λ_op α) = -d_C_star_form Jf cod α) : (∀ {p : ℕ} (α : Ω p), lef.L_op (DifferentialFormSpace.d VF α) = DifferentialFormSpace.d VF (lef.L_op α)) ∧ (∀ {p : ℕ} (α : Ω (p + 3)), dl.Λ_op (cod.dstar α) = cod.dstar (dl.Λ_op α)) ∧ (∀ {p : ℕ} (α : Ω (p + 1)), lef.L_op (cod.dstar α) + -cod.dstar (lef.L_op α) = d_C_form Jf α) ∧ ∀ {p : ℕ} (α : Ω (p + 2)), dl.Λ_op (DifferentialFormSpace.d VF α) + -DifferentialFormSpace.d VF (dl.Λ_op α) = -d_C_star_form Jf cod α

The four Kähler identities on a Kähler manifold: $[L, d] = 0$, $[\Lambda, d^*] = 0$, $[L, d^*] = d_C$, $[\Lambda, d] = -d_C^*$.

theorem laplacian_J_invariant {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (Jf : JActsOnForms J) (cod : Codifferential) (d_commutes_J : ∀ {p : ℕ} (α : Ω p), DifferentialFormSpace.d VF (Jf.J_form α) = Jf.J_form (DifferentialFormSpace.d VF α)) (dstar_commutes_J : ∀ {p : ℕ} (α : Ω (p + 1)), cod.dstar (Jf.J_form α) = Jf.J_form (cod.dstar α)) {p : ℕ} (α : Ω (p + 1)) : laplacian cod (Jf.J_form α) = Jf.J_form (laplacian cod α)

On a Kähler manifold the Laplacian is $J$-invariant: $\Delta(J\alpha) = J(\Delta \alpha)$.

structure IsDifferentialOperator {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) : Type u_1

A linear differential operator $L: \Omega^{p+1} \to \Omega^{p+1}$ of order order equipped with its principal symbol $\sigma_k(L)(\xi)$ that is homogeneous of degree order in $\xi$.

• order : ℕ
• symbol : Ω 1 → {p : ℕ} → Ω (p + 1) → Ω (p + 1)
• L_add {p : ℕ} (α β : Ω (p + 1)) : L (α + β) = L α + L β
• L_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : L (r • α) = r • L α
• symbol_homogeneous (r : ℝ) (ξ : Ω 1) {p : ℕ} (α : Ω (p + 1)) : self.symbol (r • ξ) α = r ^ self.order • self.symbol ξ α

structure IsElliptic {ΓE : Type u_1} {ΓF : Type u_2} {T : Type u_3} [AddCommGroup ΓE] [Module ℝ ΓE] [AddCommGroup ΓF] [Module ℝ ΓF] [AddCommGroup T] [Module ℝ T] (L : ΓE → ΓF) : Type (max (max u_1 u_2) u_3)

A general elliptic operator $L: \Gamma E \to \Gamma F$: a linear operator whose principal symbol $\sigma(L)(\xi)$ is a bijection for every nonzero $\xi$.

• order : ℕ
• symbol : T → ΓE → ΓF
• L_add (s t : ΓE) : L (s + t) = L s + L t
• L_smul (r : ℝ) (s : ΓE) : L (r • s) = r • L s
• symbol_homogeneous (r : ℝ) (ξ : T) (s : ΓE) : self.symbol (r • ξ) s = r ^ self.order • self.symbol ξ s
• elliptic (ξ : T) : ξ ≠ 0 → Function.Bijective (self.symbol ξ)

structure IsEllipticEndo {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) extends IsDifferentialOperator fun {p : ℕ} => L : Type u_1

An elliptic differential endomorphism $L: \Omega^{p+1} \to \Omega^{p+1}$: a differential operator whose principal symbol is bijective at every nonzero covector.

• order : ℕ
• symbol : Ω 1 → {p : ℕ} → Ω (p + 1) → Ω (p + 1)
• L_add {p : ℕ} (α β : Ω (p + 1)) : L (α + β) = L α + L β
• L_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : L (r • α) = r • L α
• symbol_homogeneous (r : ℝ) (ξ : Ω 1) {p : ℕ} (α : Ω (p + 1)) : self.symbol (r • ξ) α = r ^ self.order • self.symbol ξ α
• elliptic (ξ : Ω 1) : ξ ≠ 0 → ∀ {p : ℕ}, Function.Bijective (self.symbol ξ)

class IsCompactManifold (Ω : ℕ → Type u_1) (VF : Type u_2) [DifferentialFormSpace Ω VF] : Type

A compact manifold of positive dimension dim.

• dim : ℕ
• dim_pos : 0 < dim Ω VF

class IsCompactOrientedRiemannian (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] extends IsCompactManifold Ω VF : Type u_1

A compact oriented Riemannian manifold equipped with a codifferential, an $L^2$ inner product, a volume form, Stokes' theorem for exact forms, and the integral formula $\langle \alpha, \beta\rangle = \int_M \alpha \wedge *\beta$. Also assumes finite dimensionality of harmonic forms in each degree.

• dim : ℕ
• dim_pos : 0 < dim Ω VF
• cod : Codifferential
• ip : L2InnerProduct cod
• vol : Ω (IsCompactManifold.dim Ω VF)
• vol_nonzero : vol ≠ 0
• wedge_star (p : ℕ) : Ω p → Ω p → Ω (IsCompactManifold.dim Ω VF)
• integrate : Ω (IsCompactManifold.dim Ω VF) → ℝ
• integrate_linear (r : ℝ) (ω₁ ω₂ : Ω (IsCompactManifold.dim Ω VF)) : integrate (r • ω₁ + ω₂) = r * integrate ω₁ + integrate ω₂
• stokes_exact_vanishes (p : ℕ) (hp : p + 1 = IsCompactManifold.dim Ω VF) (η : Ω p) : integrate (hp ▸ DifferentialFormSpace.d VF η) = 0
• inner_eq_integrate_wedge_star {p : ℕ} (α β : Ω p) : ip.inner α β = integrate (wedge_star p α β)
• compact_finite_dim_harmonic (k : ℕ) : ∃ (S : Finset (Ω (k + 1))), (∀ s ∈ S, IsHarmonic cod s) ∧ ∀ (α : Ω (k + 1)), IsHarmonic cod α → ∃ (coeffs : Ω (k + 1) → ℝ), α = ∑ s ∈ S, coeffs s • s

@[reducible]

noncomputable def IsCompactSymplectic.toIsCompactOrientedRiemannian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [h : IsCompactSymplectic Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) (vol : Ω (2 * SymplecticManifoldDim.n Ω VF)) (vol_nonzero : vol ≠ 0) (wedge_star : (p : ℕ) → Ω p → Ω p → Ω (2 * SymplecticManifoldDim.n Ω VF)) (integrate : Ω (2 * SymplecticManifoldDim.n Ω VF) → ℝ) (integrate_linear : ∀ (r : ℝ) (ω₁ ω₂ : Ω (2 * SymplecticManifoldDim.n Ω VF)), integrate (r • ω₁ + ω₂) = r * integrate ω₁ + integrate ω₂) (stokes : ∀ (p : ℕ) (hp : p + 1 = 2 * SymplecticManifoldDim.n Ω VF) (η : Ω p), integrate (hp ▸ DifferentialFormSpace.d VF η) = 0) (inner_eq : ∀ {p : ℕ} (α β : Ω p), ip.inner α β = integrate (wedge_star p α β)) (finite_harmonic : ∀ (k : ℕ), ∃ (S : Finset (Ω (k + 1))), (∀ s ∈ S, IsHarmonic cod s) ∧ ∀ (α : Ω (k + 1)), IsHarmonic cod α → ∃ (coeffs : Ω (k + 1) → ℝ), α = ∑ s ∈ S, coeffs s • s) : IsCompactOrientedRiemannian Ω VF

Builds an IsCompactOrientedRiemannian structure on a compact symplectic manifold (of real dimension $2n$) from explicit choices of codifferential, $L^2$ inner product, volume form, Stokes data, and finite-dimensional harmonic spaces.

@[implicit_reducible, instance 100]

instance IsCompactSymplectic.toIsCompactManifold {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] [h : IsCompactSymplectic Ω VF] : IsCompactManifold Ω VF

Every compact symplectic manifold (of complex dimension $n$) is a compact manifold of real dimension $2n$.

class HasHodgeData (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type u_1

Minimal data required for Hodge theory: a codifferential and a compatible $L^2$ inner product on differential forms.

• codiff : Codifferential
• l2ip : L2InnerProduct codiff

@[implicit_reducible, instance 100]

noncomputable instance IsCompactOrientedRiemannian.toHasHodgeData {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hR : IsCompactOrientedRiemannian Ω VF] : HasHodgeData Ω VF

Every compact oriented Riemannian manifold provides Hodge data.

noncomputable def IsCompactOrientedRiemannian.hodgeStar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hR : IsCompactOrientedRiemannian Ω VF] : HodgeStar

The Hodge star operator extracted from the codifferential data on a compact oriented Riemannian manifold.

theorem IsCompactOrientedRiemannian.codifferential_from_star {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hR : IsCompactOrientedRiemannian Ω VF] {p : ℕ} (h : p + 1 ≤ cod.manifold_dim) (ω : Ω (p + 1)) : cod.dstar ω = cod.sign_factor (p + 1) • cast ⋯ (cod.star_deg ⋯ (DifferentialFormSpace.d VF (cod.star_deg h ω)))

On a compact oriented Riemannian manifold the codifferential satisfies the standard formula $d^*\omega = (-1)^{n(k-1)+1} * d * \omega$.

theorem IsCompactOrientedRiemannian.l2_inner_eq_integral {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hR : IsCompactOrientedRiemannian Ω VF] {p : ℕ} (α β : Ω p) : ip.inner α β = integrate (wedge_star p α β)

The $L^2$ inner product equals the integral of the wedge with the star: $\langle \alpha, \beta \rangle = \int_M \alpha \wedge *\beta$.

class HasSobolevSpaces (Ω : ℕ → Type u_1) (VF : Type u_2) [DifferentialFormSpace Ω VF] : Type u_1

A predicate giving the Sobolev regularity scale $H^s$ for differential forms.

• IsSobolevRegular : ℕ → {p : ℕ} → Ω (p + 1) → Prop

class IsSmoothing {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [sob : HasSobolevSpaces Ω VF] (S : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) : Prop

A smoothing operator $S$: linear and raises Sobolev regularity by at least one order (and by two when iterated).

• S_add {p : ℕ} (a b : Ω (p + 1)) : S (a + b) = S a + S b
• S_smul {p : ℕ} (r : ℝ) (a : Ω (p + 1)) : S (r • a) = r • S a
• sobolev_improvement (s : ℕ) {p : ℕ} (α : Ω (p + 1)) : HasSobolevSpaces.IsSobolevRegular VF s α → HasSobolevSpaces.IsSobolevRegular VF (s + 1) (S α)
• compact_improvement (s : ℕ) {p : ℕ} (α : Ω (p + 1)) : HasSobolevSpaces.IsSobolevRegular VF s α → HasSobolevSpaces.IsSobolevRegular VF (s + 2) (S (S α))

theorem IsSmoothing.iterate_improvement {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [sob : HasSobolevSpaces Ω VF] {S : {p : ℕ} → Ω (p + 1) → Ω (p + 1)} [hS : IsSmoothing fun {p : ℕ} => S] (n s : ℕ) {p : ℕ} (α : Ω (p + 1)) : HasSobolevSpaces.IsSobolevRegular VF s α → HasSobolevSpaces.IsSobolevRegular VF (s + n) (S^[n] α)

Iterating a smoothing operator $n$ times raises Sobolev regularity by $n$ orders: if $\alpha \in H^s$, then $S^n \alpha \in H^{s+n}$.

structure IsSmoothingOp {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousConstSMul ℝ E] (S : E →L[ℝ] E) (IsSobReg : ℕ → E → Prop) : Prop

A smoothing operator $S: E \to E$ on an abstract topological vector space, characterized by raising the Sobolev regularity by one order.

• sobolev_improvement (s : ℕ) (α : E) : IsSobReg s α → IsSobReg (s + 1) (S α)

structure HasParametrix {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousConstSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℝ F] (L : E →L[ℝ] F) : Type (max u_1 u_2)

A parametrix (pseudo-inverse) for a continuous linear operator $L: E \to F$: a continuous linear $P: F \to E$ with $PL = \mathrm{id} + S_{\text{left}}$ and $LP = \mathrm{id} + S_{\text{right}}$, where $S_{\text{left}}$ and $S_{\text{right}}$ are smoothing operators.

• P : F →L[ℝ] E
• S_left : E →L[ℝ] E
• S_right : F →L[ℝ] F
• PL_eq (α : E) : self.P (L α) = α + self.S_left α
• LP_eq (β : F) : L (self.P β) = β + self.S_right β
• IsSobRegE : ℕ → E → Prop
• IsSobRegF : ℕ → F → Prop
• isSmoothingOp_S_left : IsSmoothingOp self.S_left self.IsSobRegE
• isSmoothingOp_S_right : IsSmoothingOp self.S_right self.IsSobRegF

def HasParametrix.sLeftLinearMap {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousConstSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℝ F] {L : E →L[ℝ] F} (h : HasParametrix L) : E →ₗ[ℝ] E

The left smoothing remainder $S_{\text{left}}$ of a parametrix as an $\mathbb{R}$-linear map.

def HasParametrix.sRightLinearMap {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousConstSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℝ F] {L : E →L[ℝ] F} (h : HasParametrix L) : F →ₗ[ℝ] F

The right smoothing remainder $S_{\text{right}}$ of a parametrix as an $\mathbb{R}$-linear map.

structure HasParametrixDFS {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasSobolevSpaces Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) : Type u_1

A parametrix (pseudo-inverse) for an operator $L$ on the differential form spaces: $PL = \mathrm{id} + S_{\text{left}}$ and $LP = \mathrm{id} + S_{\text{right}}$ with smoothing remainders.

• P {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• S_left {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• S_right {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• PL_eq {p : ℕ} (α : Ω (p + 1)) : self.P (L α) = α + self.S_left α
• LP_eq {p : ℕ} (α : Ω (p + 1)) : L (self.P α) = α + self.S_right α
• S_left_isSmoothing : IsSmoothing fun {p : ℕ} => self.S_left
• S_right_isSmoothing : IsSmoothing fun {p : ℕ} => self.S_right

structure IsFredholm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) : Type u_1

A Fredholm operator on differential forms: linear, with a parametrix, having finite dimensional kernel and cokernel and complemented (closed) range.

• P {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• S_left {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• S_right {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• PL_eq {p : ℕ} (α : Ω (p + 1)) : self.P (L α) = α + self.S_left α
• LP_eq {p : ℕ} (α : Ω (p + 1)) : L (self.P α) = α + self.S_right α
• ker_contained {p : ℕ} (α : Ω (p + 1)) : L α = 0 → α + self.S_left α = self.P 0
• L_add {p : ℕ} (α β : Ω (p + 1)) : L (α + β) = L α + L β
• L_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : L (r • α) = r • L α
• kernel_finiteDim (p : ℕ) : FiniteDimensional ℝ ↥{ toFun := L, map_add' := ⋯, map_smul' := ⋯ }.ker
• cokernel_finiteDim (p : ℕ) : FiniteDimensional ℝ (Ω (p + 1) ⧸ { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range)
• range_complemented (p : ℕ) : ∃ (C : Submodule ℝ (Ω (p + 1))), { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range ⊔ C = ⊤ ∧ { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range ⊓ C = ⊥

def IsFredholm.toLinearMap {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)} (hF : IsFredholm fun {p : ℕ} => L) (p : ℕ) : Ω (p + 1) →ₗ[ℝ] Ω (p + 1)

Packages a Fredholm operator on $\Omega^{p+1}$ as an $\mathbb{R}$-linear map.

structure HasGreenOperatorDecomp {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) : Type u_1

A Green-operator decomposition $\mathrm{id} = LG + H$ where $H$ is the harmonic projection (with $LH = 0$) and $G$ is the Green operator (inverse of $L$ on $(\ker L)^\perp$). Asserts the orthogonality $\langle H\alpha, LG\alpha\rangle = 0$.

• G {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• H {p : ℕ} : Ω (p + 1) → Ω (p + 1)
• H_maps_to_ker {p : ℕ} (α : Ω (p + 1)) : L (self.H α) = 0
• LG_eq {p : ℕ} (α : Ω (p + 1)) : L (self.G α) = α + -self.H α
• GL_eq {p : ℕ} (α : Ω (p + 1)) : self.G (L α) = α + -self.H α
• H_idem {p : ℕ} (α : Ω (p + 1)) : self.H (self.H α) = self.H α
• G_add {p : ℕ} (α β : Ω (p + 1)) : self.G (α + β) = self.G α + self.G β
• H_add {p : ℕ} (α β : Ω (p + 1)) : self.H (α + β) = self.H α + self.H β
• G_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : self.G (r • α) = r • self.G α
• H_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : self.H (r • α) = r • self.H α
• G_preserves_regularity [sob : HasSobolevSpaces Ω VF] (s : ℕ) {p : ℕ} (α : Ω (p + 1)) : HasSobolevSpaces.IsSobolevRegular VF s α → HasSobolevSpaces.IsSobolevRegular VF s (self.G α)
• H_preserves_regularity [sob : HasSobolevSpaces Ω VF] (s : ℕ) {p : ℕ} (α : Ω (p + 1)) : HasSobolevSpaces.IsSobolevRegular VF s α → HasSobolevSpaces.IsSobolevRegular VF s (self.H α)
• orth_decomp (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (α : Ω (p + 1)) : ip.inner (self.H α) (L (self.G α)) = 0
• G_H_eq_zero {p : ℕ} (α : Ω (p + 1)) : self.G (self.H α) = 0
• H_G_eq_zero {p : ℕ} (α : Ω (p + 1)) : self.H (self.G α) = 0

structure DelbarStar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) : Type u_1

The formal adjoint $\bar\partial^*: \Omega^{p+1} \to \Omega^p$ of the Dolbeault operator $\bar\partial$.

• delbar_star {p : ℕ} : Ω (p + 1) → Ω p
• delbar_star_add {p : ℕ} (α β : Ω (p + 1)) : self.delbar_star (α + β) = self.delbar_star α + self.delbar_star β
• delbar_star_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : self.delbar_star (r • α) = r • self.delbar_star α

structure DelStar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) : Type u_1

The formal adjoint $\partial^*: \Omega^{p+1} \to \Omega^p$ of the Dolbeault operator $\partial$.

• del_star {p : ℕ} : Ω (p + 1) → Ω p
• del_star_add {p : ℕ} (α β : Ω (p + 1)) : self.del_star (α + β) = self.del_star α + self.del_star β
• del_star_smul {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : self.del_star (r • α) = r • self.del_star α

theorem elliptic_has_parametrix {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactManifold Ω VF] [HasSobolevSpaces Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) : Nonempty (HasParametrixDFS fun {p : ℕ} => L)

Existence of a parametrix for an elliptic operator. Every elliptic differential operator on a compact manifold admits a pseudo-inverse $P$ with $PL - \mathrm{id}$ and $LP - \mathrm{id}$ smoothing.

theorem elliptic_has_parametrix_explicit {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactManifold Ω VF] [sob : HasSobolevSpaces Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (symbol : Ω 1 → {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (h_bijective : ∀ (ξ : Ω 1), ξ ≠ 0 → ∀ {p : ℕ}, Function.Bijective (symbol ξ)) (h_add : ∀ {p : ℕ} (α β : Ω (p + 1)), L (α + β) = L α + L β) (h_smul : ∀ {p : ℕ} (r : ℝ) (α : Ω (p + 1)), L (r • α) = r • L α) (order : ℕ) (h_symbol_homogeneous : ∀ (r : ℝ) (ξ : Ω 1) {p : ℕ} (α : Ω (p + 1)), symbol (r • ξ) α = r ^ order • symbol ξ α) : ∃ (P : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (S_left : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (S_right : {p : ℕ} → Ω (p + 1) → Ω (p + 1)), (∀ {p : ℕ} (α : Ω (p + 1)), P (L α) = α + S_left α) ∧ (∀ {p : ℕ} (α : Ω (p + 1)), L (P α) = α + S_right α) ∧ (IsSmoothing fun {p : ℕ} => S_left) ∧ IsSmoothing fun {p : ℕ} => S_right

Explicit form of the parametrix existence theorem: given an elliptic symbol and the algebraic data, there exist $P$, $S_{\text{left}}$, $S_{\text{right}}$ with $PL = \mathrm{id} + S_{\text{left}}$, $LP = \mathrm{id} + S_{\text{right}}$, and both remainders are smoothing.

theorem elliptic_regularity {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasSobolevSpaces Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (param : HasParametrixDFS fun {p : ℕ} => L) (IsSmoothSection : {p : ℕ} → Ω (p + 1) → Prop) (IsSobolevRegular : ℕ → {p : ℕ} → Ω (p + 1) → Prop) (P_preserves_smooth : ∀ {p : ℕ} (β : Ω (p + 1)), IsSmoothSection β → IsSmoothSection (param.P β)) (S_left_maps_sobolev_to_smooth : ∀ (s : ℕ) {p : ℕ} (α : Ω (p + 1)), IsSobolevRegular s α → IsSmoothSection (param.S_left α)) (smooth_sub : ∀ {p : ℕ} (a b : Ω (p + 1)), IsSmoothSection a → IsSmoothSection b → IsSmoothSection (a - b)) {p : ℕ} {ξ : Ω (p + 1)} (s : ℕ) (hξ_sob : IsSobolevRegular s ξ) (hLξ_smooth : IsSmoothSection (L ξ)) : IsSmoothSection ξ

Elliptic regularity. If $L$ is an elliptic operator with parametrix $P$ and $\xi$ is a Sobolev section with $L\xi$ smooth, then $\xi$ itself is smooth: $L\xi \in C^\infty \Rightarrow \xi \in C^\infty$.

theorem elliptic_kernel_finite_dim {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) (p : ℕ) : FiniteDimensional ℝ ↥{ toFun := L, map_add' := ⋯, map_smul' := ⋯ }.ker

Finite-dimensional kernel. An elliptic operator on a compact manifold has finite-dimensional kernel: $\dim_\mathbb{R} \ker L < \infty$.

theorem elliptic_cokernel_finite_dim {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) (p : ℕ) : FiniteDimensional ℝ (Ω (p + 1) ⧸ { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range)

Finite-dimensional cokernel. An elliptic operator on a compact manifold has finite-dimensional cokernel: $\dim_\mathbb{R} \mathrm{coker}\, L < \infty$.

theorem elliptic_range_complemented {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) (p : ℕ) : ∃ (C : Submodule ℝ (Ω (p + 1))), { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range ⊔ C = ⊤ ∧ { toFun := L, map_add' := ⋯, map_smul' := ⋯ }.range ⊓ C = ⊥

Closed (complemented) range. The image of an elliptic operator on a compact manifold has an algebraic complement, i.e. $\Omega^{p+1} = \mathrm{Im}\, L \oplus C$.

noncomputable def elliptic_fredholm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasSobolevSpaces Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) : IsFredholm fun {p : ℕ} => L

Elliptic operators are Fredholm. Assembles the parametrix, kernel finiteness, cokernel finiteness, and range complement results into an IsFredholm structure for an elliptic operator on a compact manifold.

theorem green_operator_decomposition {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) (cod : Codifferential) (ip : L2InnerProduct cod) (self_adj : ∀ {p : ℕ} (α β : Ω (p + 1)), ip.inner (L α) β = ip.inner α (L β)) : Nonempty (HasGreenOperatorDecomp fun {p : ℕ} => L)

Green operator decomposition for self-adjoint elliptic operators. For a self-adjoint elliptic operator $L$ on a compact oriented Riemannian manifold, there exists a Green operator $G$ and harmonic projection $H$ with $LG + H = \mathrm{id}$.

theorem elliptic_solvability {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (hL : IsEllipticEndo fun {p : ℕ} => L) (cod : Codifferential) (ip : L2InnerProduct cod) (L_star : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (h_adjoint : ∀ {p : ℕ} (α β : Ω (p + 1)), ip.inner (L α) β = ip.inner α (L_star β)) {p : ℕ} (τ : Ω (p + 1)) (h_orth_ker_star : ∀ (η : Ω (p + 1)), L_star η = 0 → ip.inner τ η = 0) : ∃! ξ : Ω (p + 1), L ξ = τ ∧ ∀ (η : Ω (p + 1)), L η = 0 → ip.inner ξ η = 0

Solvability of elliptic equations. For elliptic $L$ with formal adjoint $L^*$, the equation $L\xi = \tau$ has a unique solution orthogonal to $\ker L$, provided $\tau$ is orthogonal to $\ker L^*$.

noncomputable def laplacian_is_elliptic_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (cod : Codifferential) : IsEllipticEndo fun {p : ℕ} (α : Ω (p + 1)) => laplacian cod α

The Hodge Laplacian $\Delta = dd^* + d^* d$ is an elliptic operator on each space of differential forms, with principal symbol $\sigma_2(\Delta)(\xi) = -|\xi|^2 \mathrm{id}$.

theorem L2InnerProduct.inner_add_right {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {cod : Codifferential} (ip : L2InnerProduct cod) {p : ℕ} (α β γ : Ω p) : ip.inner α (β + γ) = ip.inner α β + ip.inner α γ

The $L^2$ inner product is additive in its second argument: $\langle \alpha, \beta + \gamma\rangle = \langle \alpha, \beta\rangle + \langle \alpha, \gamma\rangle$.

theorem laplacian_self_adjoint {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (α β : Ω (p + 1)) : ip.inner (laplacian cod α) β = ip.inner α (laplacian cod β)

The Hodge Laplacian is self-adjoint with respect to the $L^2$ inner product: $\langle \Delta\alpha, \beta\rangle = \langle \alpha, \Delta\beta\rangle$.

theorem green_operator_image_orthogonal {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) (gd : HasGreenOperatorDecomp fun {p : ℕ} (α : Ω (p + 1)) => laplacian cod α) {p : ℕ} (α : Ω (p + 1)) : (∃ (β : Ω (p + 1)), gd.G (laplacian cod β) = α) ↔ ∀ (h : Ω (p + 1)), IsHarmonic cod h → ip.inner h α = 0

The image of the Green operator $G \circ \Delta$ is exactly the orthogonal complement of the harmonic forms: $\alpha \in \mathrm{Im}(G \circ \Delta) \iff \alpha \perp \mathcal{H}^k$.

theorem corollary2_green_operator_summary {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) : ∃ (G : {p : ℕ} → Ω (p + 1) → Ω (p + 1)) (H : {p : ℕ} → Ω (p + 1) → Ω (p + 1)), (∀ {p : ℕ} (α : Ω (p + 1)), laplacian cod (H α) = 0) ∧ (∀ {p : ℕ} (α : Ω (p + 1)), G (laplacian cod α) = α + -H α) ∧ (∀ {p : ℕ} (α : Ω (p + 1)), laplacian cod (G α) = α + -H α) ∧ ∀ {p : ℕ} (α : Ω (p + 1)), (∃ (β : Ω (p + 1)), G (laplacian cod β) = α) ↔ ∀ (h : Ω (p + 1)), IsHarmonic cod h → ip.inner h α = 0

Green operator summary. On a compact oriented Riemannian manifold there exist a Green operator $G$ and harmonic projection $H$ for the Laplacian satisfying $\Delta H = 0$, $G\Delta = \mathrm{id} - H$, $\Delta G = \mathrm{id} - H$, and $\mathrm{Im}(G \circ \Delta) = (\mathcal{H}^k)^\perp$.

theorem hodge_decomposition_three_way {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (cod : Codifferential) (h_green : Nonempty (HasGreenOperatorDecomp fun {p : ℕ} (α : Ω (p + 1)) => laplacian cod α)) {p : ℕ} (α : Ω (p + 1)) : ∃ (h : Ω (p + 1)) (β : Ω p) (γ : Ω (p + 2)), IsHarmonic cod h ∧ α = h + DifferentialFormSpace.d VF β + cod.dstar γ

Hodge decomposition (three-way version). Every form $\alpha \in \Omega^k$ on a compact oriented Riemannian manifold can be written as $\alpha = h + d\beta + d^*\gamma$ with $h$ harmonic.

theorem orthog_harmonic_exact {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (h : Ω (p + 1)) (hh : IsHarmonic cod h) (β : Ω p) : ip.inner h (DifferentialFormSpace.d VF β) = 0

Harmonic forms are $L^2$-orthogonal to exact forms: $\langle h, d\beta\rangle = 0$ when $h$ is harmonic.

theorem orthog_harmonic_coexact {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (h : Ω (p + 1)) (hh : IsHarmonic cod h) (γ : Ω (p + 2)) : ip.inner h (cod.dstar γ) = 0

Harmonic forms are $L^2$-orthogonal to coexact forms: $\langle h, d^*\gamma\rangle = 0$ when $h$ is harmonic.

theorem orthog_exact_coexact {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (β : Ω p) (γ : Ω (p + 2)) : ip.inner (DifferentialFormSpace.d VF β) (cod.dstar γ) = 0

Exact and coexact forms are $L^2$-orthogonal: $\langle d\beta, d^*\gamma\rangle = 0$, since $\langle d\beta, d^*\gamma\rangle = \langle d^2\beta, \gamma\rangle = 0$.

class HasLaplacianGreenDecomp {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) : Prop

Typeclass packaging the existence of a Green-operator decomposition for the Hodge Laplacian.

• green_decomp : Nonempty (HasGreenOperatorDecomp fun {p : ℕ} (α : Ω (p + 1)) => laplacian cod α)

theorem hodge_decomposition_orthogonal {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) [h_green : HasLaplacianGreenDecomp cod] {p : ℕ} (α : Ω (p + 1)) : (∃ (h : Ω (p + 1)) (β : Ω p) (γ : Ω (p + 2)), IsHarmonic cod h ∧ α = h + DifferentialFormSpace.d VF β + cod.dstar γ ∧ ip.inner h (DifferentialFormSpace.d VF β) = 0 ∧ ip.inner h (cod.dstar γ) = 0 ∧ ip.inner (DifferentialFormSpace.d VF β) (cod.dstar γ) = 0) ∧ ∀ (h₁ h₂ : Ω (p + 1)) (β₁ β₂ : Ω p) (γ₁ γ₂ : Ω (p + 2)), IsHarmonic cod h₁ → IsHarmonic cod h₂ → α = h₁ + DifferentialFormSpace.d VF β₁ + cod.dstar γ₁ → α = h₂ + DifferentialFormSpace.d VF β₂ + cod.dstar γ₂ → h₁ = h₂

Hodge decomposition theorem (orthogonal form). On a compact oriented Riemannian manifold, every $(k+1)$-form $\alpha$ has an orthogonal Hodge decomposition $\alpha = h + d\beta + d^*\gamma$ with the three summands pairwise $L^2$-orthogonal, and the harmonic part $h$ is unique.

theorem hodge_representative {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactOrientedRiemannian Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) (h_green : Nonempty (HasGreenOperatorDecomp fun {p : ℕ} (α : Ω (p + 1)) => laplacian cod α)) {p : ℕ} (α : Ω (p + 1)) (hclosed : DifferentialFormSpace.d VF α = 0) : ∃ (h : Ω (p + 1)) (β : Ω p), IsHarmonic cod h ∧ α = h + DifferentialFormSpace.d VF β

Hodge representative (existence). Every closed form $\alpha$ on a compact oriented Riemannian manifold can be written as $\alpha = h + d\beta$ with $h$ harmonic.

theorem harmonic_exact_is_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (h : Ω (p + 1)) (hHarm : IsHarmonic cod h) (γ : Ω p) (hExact : h = DifferentialFormSpace.d VF γ) : h = 0

An exact harmonic form is zero: if $h = d\gamma$ is harmonic, then $h = 0$. Proof: $\langle h, h\rangle = \langle d\gamma, h\rangle = \langle \gamma, d^* h\rangle = 0$.

theorem Codifferential.dstar_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : cod.dstar (-α) = -cod.dstar α

The codifferential commutes with negation: $d^*(-\alpha) = -d^*\alpha$.

theorem laplacian_sub {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) {p : ℕ} (α β : Ω (p + 1)) : laplacian cod (α - β) = laplacian cod α - laplacian cod β

The Laplacian is additive under subtraction: $\Delta(\alpha - \beta) = \Delta\alpha - \Delta\beta$.

theorem hodge_representative_unique {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (ip : L2InnerProduct cod) {p : ℕ} (h₁ h₂ : Ω (p + 1)) (hHarm₁ : IsHarmonic cod h₁) (hHarm₂ : IsHarmonic cod h₂) (γ : Ω p) (hDiff : h₁ - h₂ = DifferentialFormSpace.d VF γ) : h₁ = h₂

Hodge representative uniqueness. If $h_1, h_2$ are harmonic and differ by an exact form, $h_1 - h_2 = d\gamma$, then $h_1 = h_2$.

theorem d_sub {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α β : Ω p) : DifferentialFormSpace.d VF (α - β) = DifferentialFormSpace.d VF α - DifferentialFormSpace.d VF β

The exterior derivative is additive under subtraction: $d(\alpha - \beta) = d\alpha - d\beta$.

theorem hodge_representative_exists_unique {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hR : IsCompactOrientedRiemannian Ω VF] (h_green : Nonempty (HasGreenOperatorDecomp fun {p : ℕ} (α : Ω (p + 1)) => laplacian IsCompactOrientedRiemannian.cod α)) {p : ℕ} (α : Ω (p + 1)) (hclosed : DifferentialFormSpace.d VF α = 0) : ∃! h : Ω (p + 1), IsHarmonic IsCompactOrientedRiemannian.cod h ∧ ∃ (β : Ω p), α = h + DifferentialFormSpace.d VF β

Hodge theorem. Every de Rham cohomology class on a compact oriented Riemannian manifold has a unique harmonic representative: for any closed $\alpha$, there is a unique harmonic $h$ with $\alpha = h + d\beta$ for some $\beta$.

def IsDRCohomologous {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {k : ℕ} (α₁ α₂ : Ω (k + 1)) : Prop

Two forms $\alpha_1, \alpha_2$ are de Rham cohomologous if they differ by an exact form: $\alpha_1 - \alpha_2 = d\gamma$ for some $\gamma$.

theorem kahler_hodge_decomposition_cohomology {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (cod : Codifferential) (ip : L2InnerProduct cod) (dol : DolbeaultOps) {n : ℕ} (bg : HasBigrading J n) (dol_lap : DolbeaultLaplacian dol cod) (h_harmonic_bigrading : ∀ {k : ℕ} (h_form : Ω (k + 1)), laplacian cod h_form = 0 → ∃ (component : Fin (k + 2) → Ω (k + 1)), (∀ (j : Fin (k + 2)), ∃ (ω : bg.Ω_pq (↑j) (k + 1 - ↑j)), cast ⋯ (bg.incl (↑j) (k + 1 - ↑j) ω) = component j) ∧ (∀ (j : Fin (k + 2)), dol.del (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol.delbar (component j) = 0) ∧ (∀ (j : Fin (k + 2)), laplacian cod (component j) = 0) ∧ h_form = Finset.univ.sum component) (h_hodge_rep : ∀ {p : ℕ} (α' : Ω (p + 1)), DifferentialFormSpace.d VF α' = 0 → ∃ (h : Ω (p + 1)) (β : Ω p), laplacian cod h = 0 ∧ α' = h + DifferentialFormSpace.d VF β) (h_dolbeault_id : ∀ {k' : ℕ} (α' : Ω (k' + 1)), laplacian cod α' = 0 ↔ dol_lap.box_bar α' = 0) {k : ℕ} (α₁ α₂ : Ω (k + 1)) (hclosed₁ : DifferentialFormSpace.d VF α₁ = 0) (hclosed₂ : DifferentialFormSpace.d VF α₂ = 0) (hcohom : IsDRCohomologous α₁ α₂) : (∀ (h₁ h₂ : Ω (k + 1)) (β₁ β₂ : Ω k), IsHarmonic cod h₁ → α₁ = h₁ + DifferentialFormSpace.d VF β₁ → IsHarmonic cod h₂ → α₂ = h₂ + DifferentialFormSpace.d VF β₂ → h₁ = h₂) ∧ ∃ (component : Fin (k + 2) → Ω (k + 1)) (β : Ω k), (∀ (j : Fin (k + 2)), ∃ (ω : bg.Ω_pq (↑j) (k + 1 - ↑j)), cast ⋯ (bg.incl (↑j) (k + 1 - ↑j) ω) = component j) ∧ (∀ (j : Fin (k + 2)), dol.del (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol.delbar (component j) = 0) ∧ (∀ (j : Fin (k + 2)), laplacian cod (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol_lap.box_bar (component j) = 0) ∧ α₁ = Finset.univ.sum component + DifferentialFormSpace.d VF β ∧ ∃ (β' : Ω k), α₂ = Finset.univ.sum component + DifferentialFormSpace.d VF β'

Hodge decomposition of de Rham cohomology on Kähler manifolds. Cohomologous closed forms on a compact Kähler manifold share the same harmonic representative, which further decomposes into $(p,q)$-components, each $\bar\partial$-harmonic: this yields $H^k_{dR}(M, \mathbb{C}) = \bigoplus_{p+q=k} H^{p,q}_{\bar\partial}(M)$.

theorem corollary4_kahler_hodge {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (ip : L2InnerProduct cod) (dol : DolbeaultOps) {n : ℕ} (bg : HasBigrading J n) (dol_lap : DolbeaultLaplacian dol cod) (wells : KahlerWellsIdentities S J hK dol_lap) (h_box_bar_pres : ∀ (k p' q' : ℕ) (h : p' + q' = k + 1) (ω : bg.Ω_pq p' q'), ∃ (ω' : bg.Ω_pq p' q'), cast ⋯ (bg.incl p' q' ω') = dol_lap.box_bar (cast ⋯ (bg.incl p' q' ω))) (h_harmonic_bigrading : ∀ {k : ℕ} (h_form : Ω (k + 1)), laplacian cod h_form = 0 → ∃ (component : Fin (k + 2) → Ω (k + 1)), (∀ (j : Fin (k + 2)), ∃ (ω : bg.Ω_pq (↑j) (k + 1 - ↑j)), cast ⋯ (bg.incl (↑j) (k + 1 - ↑j) ω) = component j) ∧ (∀ (j : Fin (k + 2)), dol.del (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol.delbar (component j) = 0) ∧ (∀ (j : Fin (k + 2)), laplacian cod (component j) = 0) ∧ h_form = Finset.univ.sum component) (_hC : HasComplexStructure) (h_hodge_rep : ∀ {p : ℕ} (α' : Ω (p + 1)), DifferentialFormSpace.d VF α' = 0 → ∃ (h : Ω (p + 1)) (β : Ω p), laplacian cod h = 0 ∧ α' = h + DifferentialFormSpace.d VF β) : (∀ (k p' q' : ℕ) (h : p' + q' = k + 1) (ω : bg.Ω_pq p' q'), ∃ (ω' : bg.Ω_pq p' q'), cast ⋯ (bg.incl p' q' ω') = laplacian cod (cast ⋯ (bg.incl p' q' ω))) ∧ ∀ {k : ℕ} (α₁ α₂ : Ω (k + 1)), DifferentialFormSpace.d VF α₁ = 0 → DifferentialFormSpace.d VF α₂ = 0 → IsDRCohomologous α₁ α₂ → (∀ (h₁ h₂ : Ω (k + 1)) (β₁ β₂ : Ω k), IsHarmonic cod h₁ → α₁ = h₁ + DifferentialFormSpace.d VF β₁ → IsHarmonic cod h₂ → α₂ = h₂ + DifferentialFormSpace.d VF β₂ → h₁ = h₂) ∧ ∃ (component : Fin (k + 2) → Ω (k + 1)) (β : Ω k), (∀ (j : Fin (k + 2)), ∃ (ω : bg.Ω_pq (↑j) (k + 1 - ↑j)), cast ⋯ (bg.incl (↑j) (k + 1 - ↑j) ω) = component j) ∧ (∀ (j : Fin (k + 2)), dol.del (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol.delbar (component j) = 0) ∧ (∀ (j : Fin (k + 2)), laplacian cod (component j) = 0) ∧ (∀ (j : Fin (k + 2)), dol_lap.box_bar (component j) = 0) ∧ α₁ = Finset.univ.sum component + DifferentialFormSpace.d VF β ∧ ∃ (β' : Ω k), α₂ = Finset.univ.sum component + DifferentialFormSpace.d VF β'

Corollary 4 (Kähler Hodge corollary). Combines: (a) the Laplacian preserves the bigrading on a Kähler manifold; (b) every de Rham cohomology class has a unique harmonic representative whose $(p,q)$-components are $\bar\partial$-harmonic, providing the Hodge decomposition $H^k_{dR}(M, \mathbb{C}) = \bigoplus_{p+q=k} H^{p,q}_{\bar\partial}(M)$.

def HasBigrading.is_pq_form {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α : Ω (p + q)) : Prop

A form $\alpha \in \Omega^{p+q}$ is a pure $(p,q)$-form if it lies in the image of the inclusion $\Omega^{p,q} \hookrightarrow \Omega^{p+q}$.

theorem HasBigrading.star_bigraded {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) {p q : ℕ} (hp : p ≤ n) (hq : q ≤ n) (β : bg.Ω_pq p q) : ∃ (γ : bg.Ω_pq (n - q) (n - p)), bg.incl (n - q) (n - p) γ = cast ⋯ (bg.star_total ⋯ (bg.incl p q β))

The Hodge star respects the Hodge bigrading: $*: \Omega^{p,q} \to \Omega^{n-q, n-p}$.

noncomputable def HasBigrading.star_pq {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) {p q : ℕ} (hp : p ≤ n) (hq : q ≤ n) (β : bg.Ω_pq p q) : bg.Ω_pq (n - q) (n - p)

The Hodge star restricted to the bigraded piece $\Omega^{p,q}$, with image in $\Omega^{n-q, n-p}$.

theorem HasBigrading.star_pq_spec {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) {p q : ℕ} (hp : p ≤ n) (hq : q ≤ n) (β : bg.Ω_pq p q) : bg.incl (n - q) (n - p) (bg.star_pq hp hq β) = cast ⋯ (bg.star_total ⋯ (bg.incl p q β))

Defining identity for star_pq: its inclusion into $\Omega^{2n-(p+q)}$ matches the total Hodge star applied to the inclusion of $\beta$.

theorem hodge_star_pq_type {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} {n : ℕ} (bg : HasBigrading J n) {p q : ℕ} (hp : p ≤ n) (hq : q ≤ n) (α : Ω (p + q)) (hα : bg.is_pq_form p q α) : bg.is_pq_form (n - q) (n - p) (cast ⋯ (bg.star_total ⋯ α))

If $\alpha$ is a pure $(p,q)$-form, then $*\alpha$ is a pure $(n-q, n-p)$-form, reflecting that the Hodge star preserves the bigrading.

structure ComplexL2InnerProduct {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dbs : DelbarStar dol) extends L2InnerProduct cod : Type u_1

An $L^2$ inner product compatible with the Dolbeault $\bar\partial$ operator: the formal adjoint $\bar\partial^*$ is the $L^2$-adjoint of $\bar\partial$, witnessed via Stokes-type integration formulas.

• inner {p : ℕ} : Ω p → Ω p → ℝ
• inner_self_eq_zero {p : ℕ} (α : Ω p) : self.inner α α = 0 → α = 0
• inner_self_nonneg {p : ℕ} (α : Ω p) : 0 ≤ self.inner α α
• inner_symm {p : ℕ} (α β : Ω p) : self.inner α β = self.inner β α
• adjoint_d {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : self.inner (DifferentialFormSpace.d VF α) β = self.inner α (cod.dstar β)
• inner_add_left {p : ℕ} (α β γ : Ω p) : self.inner (α + β) γ = self.inner α γ + self.inner β γ
• inner_smul_left {p : ℕ} (r : ℝ) (α β : Ω p) : self.inner (r • α) β = r * self.inner α β
• integrate_delbar_top {p : ℕ} : Ω p → Ω (p + 1) → ℝ
• stokes_delbar_leibniz {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : self.inner (dol.delbar α) β = (-1) ^ (p + 1) • self.integrate_delbar_top α β
• h_delbar_star_sign {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : (-1) ^ (p + 1) • self.integrate_delbar_top α β = self.inner α (dbs.delbar_star β)

theorem delbar_adjoint_from_stokes {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dbs : DelbarStar dol) (cip : ComplexL2InnerProduct cod dol dbs) {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : cip.inner (dol.delbar α) β = cip.inner α (dbs.delbar_star β)

Stokes-derived adjointness: $\langle \bar\partial \alpha, \beta\rangle = \langle \alpha, \bar\partial^* \beta\rangle$, obtained by combining the Stokes-Leibniz expansion with the sign-tracking formula for $\bar\partial^*$.

theorem delbar_star_L2_adjoint {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dbs : DelbarStar dol) (cip : ComplexL2InnerProduct cod dol dbs) {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : cip.inner (dol.delbar α) β = cip.inner α (dbs.delbar_star β)

$\bar\partial^*$ is the $L^2$-adjoint of $\bar\partial$ on a compact symplectic manifold: $\langle \bar\partial \alpha, \beta\rangle = \langle \alpha, \bar\partial^* \beta\rangle$.

structure ComplexL2InnerProductDel {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (ds : DelStar dol) extends L2InnerProduct cod : Type u_1

The $\partial$-counterpart of ComplexL2InnerProduct: an $L^2$ inner product compatible with the Dolbeault $\partial$ operator and its formal adjoint $\partial^*$.

• inner {p : ℕ} : Ω p → Ω p → ℝ
• inner_self_eq_zero {p : ℕ} (α : Ω p) : self.inner α α = 0 → α = 0
• inner_self_nonneg {p : ℕ} (α : Ω p) : 0 ≤ self.inner α α
• inner_symm {p : ℕ} (α β : Ω p) : self.inner α β = self.inner β α
• adjoint_d {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : self.inner (DifferentialFormSpace.d VF α) β = self.inner α (cod.dstar β)
• inner_add_left {p : ℕ} (α β γ : Ω p) : self.inner (α + β) γ = self.inner α γ + self.inner β γ
• inner_smul_left {p : ℕ} (r : ℝ) (α β : Ω p) : self.inner (r • α) β = r * self.inner α β
• integrate_del_top {p : ℕ} : Ω p → Ω (p + 1) → ℝ
• stokes_del_leibniz {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : self.inner (dol.del α) β = (-1) ^ (p + 1) • self.integrate_del_top α β
• h_del_star_sign {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : (-1) ^ (p + 1) • self.integrate_del_top α β = self.inner α (ds.del_star β)

theorem del_adjoint_from_stokes {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (ds : DelStar dol) (cip : ComplexL2InnerProductDel cod dol ds) {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : cip.inner (dol.del α) β = cip.inner α (ds.del_star β)

Stokes-derived adjointness: $\langle \partial \alpha, \beta\rangle = \langle \alpha, \partial^* \beta\rangle$.

theorem del_star_L2_adjoint {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (ds : DelStar dol) (cip : ComplexL2InnerProductDel cod dol ds) {p : ℕ} (α : Ω p) (β : Ω (p + 1)) : cip.inner (dol.del α) β = cip.inner α (ds.del_star β)

$\partial^*$ is the $L^2$-adjoint of $\partial$ on a compact symplectic manifold: $\langle \partial \alpha, \beta\rangle = \langle \alpha, \partial^* \beta\rangle$.

theorem lemma2_L2_adjointness {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dbs : DelbarStar dol) (ds : DelStar dol) (cip_delbar : ComplexL2InnerProduct cod dol dbs) (cip_del : ComplexL2InnerProductDel cod dol ds) : (∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), cip_delbar.inner (dol.delbar α) β = cip_delbar.inner α (dbs.delbar_star β)) ∧ ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), cip_del.inner (dol.del α) β = cip_del.inner α (ds.del_star β)

$L^2$-adjointness of Dolbeault operators (Lemma 2). Both $\partial^*$ and $\bar\partial^*$ are $L^2$-adjoints of $\partial$ and $\bar\partial$ respectively.

theorem box_bar_harmonic_implies_delbar_closed_coclosed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {p : ℕ} (α : Ω (p + 1)) (hBox : dol_lap.box_bar α = 0) : dol.delbar α = 0 ∧ dol_lap.delbar_star α = 0

A $\bar\square$-harmonic form is both $\bar\partial$-closed and $\bar\partial$-coclosed: $\bar\square \alpha = 0 \iff \bar\partial \alpha = 0 \text{ and } \bar\partial^* \alpha = 0$ (direct $\Rightarrow$ implication shown).

theorem box_bar_harmonic_delbar_exact_is_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {p : ℕ} (h : Ω (p + 1)) (hBox : dol_lap.box_bar h = 0) (γ : Ω p) (hExact : h = dol.delbar γ) : h = 0

A $\bar\square$-harmonic form that is $\bar\partial$-exact is zero: if $h = \bar\partial \gamma$ is $\bar\square$-harmonic, then $h = 0$.

theorem dolbeault_existence_bigraded {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α_pq : bg.Ω_pq p (q + 1)) (hclosed : dol.delbar (bg.incl p (q + 1) α_pq) = 0) : ∃ (h_pq : bg.Ω_pq p (q + 1)) (β_pq : bg.Ω_pq p q), dol_lap.box_bar (bg.incl p (q + 1) h_pq) = 0 ∧ bg.incl p (q + 1) α_pq = bg.incl p (q + 1) h_pq + dol.delbar (bg.incl p q β_pq)

Existence of a Dolbeault harmonic representative. For every $\bar\partial$-closed $(p, q+1)$-form on a compact Kähler manifold, there exist a $\bar\square$-harmonic $(p, q+1)$-form $h_{pq}$ and a $(p, q)$-form $\beta_{pq}$ with $\alpha = h_{pq} + \bar\partial \beta_{pq}$.

theorem delbar_star_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {cod : Codifferential} {dol : DolbeaultOps} (dol_lap : DolbeaultLaplacian dol cod) {p : ℕ} (α : Ω (p + 1)) : dol_lap.delbar_star (-α) = -dol_lap.delbar_star α

$\bar\partial^*$ commutes with negation: $\bar\partial^*(-\alpha) = -\bar\partial^*\alpha$.

theorem delbar_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) {p : ℕ} (α : Ω p) : dol.delbar (-α) = -dol.delbar α

$\bar\partial$ commutes with negation: $\bar\partial(-\alpha) = -\bar\partial\alpha$.

theorem box_bar_sub {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {cod : Codifferential} {dol : DolbeaultOps} (dol_lap : DolbeaultLaplacian dol cod) {p : ℕ} (α β : Ω (p + 1)) : dol_lap.box_bar (α - β) = dol_lap.box_bar α - dol_lap.box_bar β

The $\bar\square$ Laplacian is linear under subtraction: $\bar\square(\alpha - \beta) = \bar\square \alpha - \bar\square \beta$.

theorem box_bar_harmonic_unique {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {p' : ℕ} (h₁ h₂ : Ω (p' + 1)) (hHarm₁ : dol_lap.box_bar h₁ = 0) (hHarm₂ : dol_lap.box_bar h₂ = 0) (a b : Ω p') (hcohom : h₁ + dol.delbar a = h₂ + dol.delbar b) : h₁ = h₂

Uniqueness of the $\bar\square$-harmonic representative: two $\bar\square$-harmonic forms whose $\bar\partial$-cohomology classes coincide must be equal.

theorem dolbeault_harmonic_representative {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α_pq : bg.Ω_pq p (q + 1)) (hclosed : dol.delbar (bg.incl p (q + 1) α_pq) = 0) : ∃! h_pq : bg.Ω_pq p (q + 1), dol_lap.box_bar (bg.incl p (q + 1) h_pq) = 0 ∧ ∃ (β_pq : bg.Ω_pq p q), bg.incl p (q + 1) α_pq = bg.incl p (q + 1) h_pq + dol.delbar (bg.incl p q β_pq)

Dolbeault Hodge theorem. Every $\bar\partial$-closed $(p, q+1)$-form on a compact Kähler manifold has a unique $\bar\square$-harmonic representative in its $\bar\partial$-cohomology class.

noncomputable def harmonic_projection_pq {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α_pq : bg.Ω_pq p (q + 1)) (hclosed : dol.delbar (bg.incl p (q + 1) α_pq) = 0) : bg.Ω_pq p (q + 1)

The harmonic projection sending a $\bar\partial$-closed $(p, q+1)$-form to its unique $\bar\square$-harmonic representative.

theorem harmonic_projection_pq_is_harmonic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α_pq : bg.Ω_pq p (q + 1)) (hclosed : dol.delbar (bg.incl p (q + 1) α_pq) = 0) : dol_lap.box_bar (bg.incl p (q + 1) (harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q α_pq hclosed)) = 0

The harmonic projection lands in the $\bar\square$-harmonic forms: $\bar\square(\Pi_h \alpha) = 0$.

theorem harmonic_projection_pq_decomposition {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α_pq : bg.Ω_pq p (q + 1)) (hclosed : dol.delbar (bg.incl p (q + 1) α_pq) = 0) : ∃ (β_pq : bg.Ω_pq p q), bg.incl p (q + 1) α_pq = bg.incl p (q + 1) (harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q α_pq hclosed) + dol.delbar (bg.incl p q β_pq)

The decomposition $\alpha = \Pi_h \alpha + \bar\partial \beta$ provided by the harmonic projection.

theorem harmonic_projection_pq_well_defined {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (α₁_pq α₂_pq : bg.Ω_pq p (q + 1)) (hclosed₁ : dol.delbar (bg.incl p (q + 1) α₁_pq) = 0) (hclosed₂ : dol.delbar (bg.incl p (q + 1) α₂_pq) = 0) (γ_pq : bg.Ω_pq p q) (hcohom : bg.incl p (q + 1) α₁_pq = bg.incl p (q + 1) α₂_pq + dol.delbar (bg.incl p q γ_pq)) : harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q α₁_pq hclosed₁ = harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q α₂_pq hclosed₂

The harmonic projection depends only on the $\bar\partial$-cohomology class: cohomologous closed forms have the same harmonic representative.

theorem harmonic_is_delbar_closed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {p' : ℕ} (h : Ω (p' + 1)) (hBox : dol_lap.box_bar h = 0) : dol.delbar h = 0

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

theorem harmonic_projection_pq_of_harmonic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) (h_pq : bg.Ω_pq p (q + 1)) (hBox : dol_lap.box_bar (bg.incl p (q + 1) h_pq) = 0) (hclosed : dol.delbar (bg.incl p (q + 1) h_pq) = 0) : harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q h_pq hclosed = h_pq

The harmonic projection acts as the identity on $\bar\square$-harmonic forms.

theorem dolbeault_cohomology_iso_harmonic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (cod : Codifferential) (dol : DolbeaultOps) (dol_lap : DolbeaultLaplacian dol cod) (ip : L2InnerProduct cod) (h_adj_delbar : ∀ {p : ℕ} (α : Ω p) (β : Ω (p + 1)), ip.inner (dol.delbar α) β = ip.inner α (dol_lap.delbar_star β)) {n : ℕ} (bg : HasBigrading J n) (p q : ℕ) : (∀ (α_pq : bg.Ω_pq p (q + 1)), dol.delbar (bg.incl p (q + 1) α_pq) = 0 → ∃! h_pq : bg.Ω_pq p (q + 1), dol_lap.box_bar (bg.incl p (q + 1) h_pq) = 0 ∧ ∃ (β_pq : bg.Ω_pq p q), bg.incl p (q + 1) α_pq = bg.incl p (q + 1) h_pq + dol.delbar (bg.incl p q β_pq)) ∧ (∀ {p' : ℕ} (h : Ω (p' + 1)), dol_lap.box_bar h = 0 → dol.delbar h = 0) ∧ (∀ (α₁_pq α₂_pq : bg.Ω_pq p (q + 1)) (hclosed₁ : dol.delbar (bg.incl p (q + 1) α₁_pq) = 0) (hclosed₂ : dol.delbar (bg.incl p (q + 1) α₂_pq) = 0) (γ_pq : bg.Ω_pq p q), bg.incl p (q + 1) α₁_pq = bg.incl p (q + 1) α₂_pq + dol.delbar (bg.incl p q γ_pq) → harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q α₁_pq hclosed₁ = harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q α₂_pq hclosed₂) ∧ ∀ (h_pq : bg.Ω_pq p (q + 1)), dol_lap.box_bar (bg.incl p (q + 1) h_pq) = 0 → ∀ (hclosed : dol.delbar (bg.incl p (q + 1) h_pq) = 0), harmonic_projection_pq S J hK cod dol dol_lap ip ⋯ bg p q h_pq hclosed = h_pq

Dolbeault cohomology is computed by $\bar\square$-harmonic forms. Bundles existence-uniqueness of $\bar\square$-harmonic representatives, the fact that $\bar\square$-harmonic implies $\bar\partial$-closed, and the well-definedness of the harmonic projection on $\bar\partial$-cohomology classes: $H^{p,q}_{\bar\partial}(M) = \mathcal{H}^{p,q}_{\bar\square}$.

def JActsOnForms.d_C {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) {p : ℕ} (α : Ω p) : Ω (p + 1)

The twisted differential $d_C = -J d J$ as a method on JActsOnForms.

theorem JActsOnForms.d_C_sq_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) {p : ℕ} (α : Ω p) : Jf.d_C (Jf.d_C α) = 0

The twisted differential squares to zero: $d_C \circ d_C = 0$. This follows from $d^2 = 0$ and $J^2 = -\mathrm{id}$.

def JActsOnForms.laplacian_C {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Ω (p + 1)

The twisted Laplacian $\Delta_C = -J \Delta J$ associated to the $J$-action on forms.

structure KahlerJDolbeaultComm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) {J : AlmostComplexStr} (Jf : JActsOnForms J) (cod : Codifferential) (dol_lap : DolbeaultLaplacian dol cod) : Prop

Compatibility data witnessing that $J$ commutes with each of $\partial, \bar\partial, \partial^*, \bar\partial^*$ on a Kähler manifold.

• J_commutes_del {p : ℕ} (α : Ω p) : dol.del (Jf.J_form α) = Jf.J_form (dol.del α)
• J_commutes_delbar {p : ℕ} (α : Ω p) : dol.delbar (Jf.J_form α) = Jf.J_form (dol.delbar α)
• J_commutes_del_star {p : ℕ} (α : Ω (p + 1)) : dol_lap.del_star (Jf.J_form α) = Jf.J_form (dol_lap.del_star α)
• J_commutes_delbar_star {p : ℕ} (α : Ω (p + 1)) : dol_lap.delbar_star (Jf.J_form α) = Jf.J_form (dol_lap.delbar_star α)

theorem kahler_d_commutes_J {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (Jf : JActsOnForms J) {dol : DolbeaultOps} {cod : Codifferential} {dol_lap : DolbeaultLaplacian dol cod} (hJD : KahlerJDolbeaultComm dol Jf cod dol_lap) {p : ℕ} (α : Ω p) : DifferentialFormSpace.d VF (Jf.J_form α) = Jf.J_form (DifferentialFormSpace.d VF α)

On a Kähler manifold, $d$ commutes with the action of $J$ on forms: $d(J\alpha) = J(d\alpha)$. Deduced from $d = \partial + \bar\partial$ and the commutation of each Dolbeault component with $J$.

theorem kahler_dstar_commutes_J {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (Jf : JActsOnForms J) (cod : Codifferential) {dol : DolbeaultOps} {dol_lap : DolbeaultLaplacian dol cod} (hJD : KahlerJDolbeaultComm dol Jf cod dol_lap) {p : ℕ} (α : Ω (p + 1)) : cod.dstar (Jf.J_form α) = Jf.J_form (cod.dstar α)

On a Kähler manifold, $d^*$ commutes with the action of $J$: $d^*(J\alpha) = J(d^*\alpha)$. Deduced from $d^* = \partial^* + \bar\partial^*$.

theorem JActsOnForms.laplacian_C_eq_laplacian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (Jf : JActsOnForms J) (cod : Codifferential) {dol : DolbeaultOps} {dol_lap : DolbeaultLaplacian dol cod} (hJD : KahlerJDolbeaultComm dol Jf cod dol_lap) {p : ℕ} (α : Ω (p + 1)) : Jf.laplacian_C cod α = laplacian cod α

On a Kähler manifold, the twisted Laplacian equals the ordinary one: $\Delta_C = -J \Delta J = \Delta$, since $J$ commutes with $\Delta$ and $J^2 = -\mathrm{id}$.

def JActsOnForms.d_C_star {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Ω p

The twisted codifferential $d_C^* = -J d^* J$ as a method on JActsOnForms.

theorem JActsOnForms.laplacian_C_eq_dC_decomp {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (Jf : JActsOnForms J) (cod : Codifferential) {p : ℕ} (α : Ω (p + 1)) : Jf.laplacian_C cod α = Jf.d_C (Jf.d_C_star cod α) + Jf.d_C_star cod (Jf.d_C α)

The twisted Laplacian decomposes as $\Delta_C = d_C d_C^* + d_C^* d_C$ in analogy with the standard formula for $\Delta$.

def IsSmoothViaSobolev {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [sob : HasSobolevSpaces Ω VF] {p : ℕ} (α : Ω (p + 1)) : Prop

A form is smooth via Sobolev if it lies in every Sobolev space $H^s$: $\alpha \in C^\infty \iff \alpha \in \bigcap_s H^s$.

theorem IsSmoothViaSobolev_sub {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [sob : HasSobolevSpaces Ω VF] {p : ℕ} (a b : Ω (p + 1)) : IsSmoothViaSobolev a → IsSmoothViaSobolev b → IsSmoothViaSobolev (a - b)

The difference of two smooth-via-Sobolev forms is smooth via Sobolev.

theorem smoothing_maps_sobolev_to_smooth {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [sob : HasSobolevSpaces Ω VF] {S : {p : ℕ} → Ω (p + 1) → Ω (p + 1)} [hS : IsSmoothing fun {p : ℕ} => S] (s : ℕ) {p : ℕ} (α : Ω (p + 1)) (h : HasSobolevSpaces.IsSobolevRegular VF s α) : IsSmoothViaSobolev (S α)

A smoothing operator maps any Sobolev form to a smooth form (an iterated application reaches every Sobolev order).

theorem parametrix_preserves_smooth {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [sob : HasSobolevSpaces Ω VF] {L : {p : ℕ} → Ω (p + 1) → Ω (p + 1)} (param : HasParametrixDFS fun {p : ℕ} => L) {p : ℕ} (β : Ω (p + 1)) (h : IsSmoothViaSobolev β) : IsSmoothViaSobolev (param.P β)

The parametrix $P$ preserves smoothness via the Sobolev scale: if $\beta$ is smooth, so is $P\beta$.