def HodgeStarMathlib.SmoothForm (n : ℕ) (M : Type u_1) [TopologicalSpace M] (k : ℕ) : Type u_1

A smooth complex-valued $k$-form on $M$ modelled on $\mathbb{C}^n$: a pointwise alternating $\mathbb{C}$-multilinear $k$-form on $\mathbb{C}^n$.

@[implicit_reducible]

noncomputable instance HodgeStarMathlib.instAddCommGroupSmoothForm {n : ℕ} {M : Type u_1} [TopologicalSpace M] {k : ℕ} : AddCommGroup (SmoothForm n M k)

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

@[implicit_reducible]

noncomputable instance HodgeStarMathlib.instModuleSmoothForm {n : ℕ} {M : Type u_1} [TopologicalSpace M] {k : ℕ} : Module ℂ (SmoothForm n M k)

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

noncomputable def HodgeStarMathlib.integrateScalar {M : Type u_1} [MeasurableSpace M] (μ : MeasureTheory.Measure M) (f : M → ℂ) : ℂ

Bochner integral $\int_M f \, d\mu$ of a complex-valued function against a measure $\mu$.

noncomputable def HodgeStarMathlib.wedgeProduct {n : ℕ} {M : Type u_1} [TopologicalSpace M] {k l : ℕ} : SmoothForm n M k → SmoothForm n M l → SmoothForm n M (k + l)

Wedge product of smooth forms: $\alpha \wedge \beta$ takes a $k$-form and an $l$-form to a $(k+l)$-form.

noncomputable def HodgeStarMathlib.hodgeStar {n : ℕ} {M : Type u_1} [TopologicalSpace M] {k : ℕ} : SmoothForm n M k → SmoothForm n M (2 * n - k)

Hodge star operator $\ast : \Omega^k \to \Omega^{2n-k}$ on smooth forms on an $n$-complex- dimensional (real $2n$) manifold. On Kähler manifolds it restricts to $\bigwedge^{p,q} \to \bigwedge^{n-q, n-p}$.

noncomputable def HodgeStarMathlib.conjForm {n : ℕ} {M : Type u_1} [TopologicalSpace M] {k : ℕ} : SmoothForm n M k → SmoothForm n M k

Pointwise complex conjugation $\bar{\alpha}$ of a smooth $k$-form.

noncomputable def HodgeStarMathlib.L2InnerProduct {n : ℕ} {M : Type u_1} [TopologicalSpace M] [MeasurableSpace M] {k : ℕ} (μ : MeasureTheory.Measure M) (α β : SmoothForm n M k) : ℂ

$L^2$ inner product of smooth $k$-forms: $\langle \alpha, \beta \rangle = \int_M \alpha \wedge \ast \bar{\beta}$.

noncomputable def HodgeStarMathlib.extD {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] {k : ℕ} : SmoothForm n M k → SmoothForm n M (k + 1)

Exterior derivative $d : \Omega^k \to \Omega^{k+1}$ on smooth complex forms.

noncomputable def HodgeStarMathlib.codifferential {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] {k : ℕ} : SmoothForm n M (k + 1) → SmoothForm n M k

Codifferential $d^\ast : \Omega^{k+1} \to \Omega^k$, the formal $L^2$-adjoint of $d$.

noncomputable def HodgeStarMathlib.laplacianForm {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] {k : ℕ} : SmoothForm n M k → SmoothForm n M k

Hodge–de Rham Laplacian $\Delta = d d^\ast + d^\ast d$ acting on $k$-forms.

theorem HodgeStarMathlib.laplacianForm_zero {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] {k : ℕ} : laplacianForm 0 = 0

The Laplacian annihilates the zero form: $\Delta 0 = 0$.

def HodgeStarMathlib.IsHarmonicForm {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] {k : ℕ} (α : SmoothForm n M k) : Prop

A $k$-form $\alpha$ is harmonic iff $\Delta \alpha = 0$.

theorem HodgeStarMathlib.hodge_decomposition {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] [CompactSpace M] [MeasurableSpace M] {k : ℕ} (α : SmoothForm n M (k + 1)) : ∃ (h : SmoothForm n M (k + 1)) (β : SmoothForm n M k) (γ : SmoothForm n M (k + 1 + 1)), IsHarmonicForm h ∧ α = h + extD β + codifferential γ

Hodge decomposition: on a compact complex manifold, every smooth $(k+1)$-form decomposes uniquely as $\alpha = h + d\beta + d^\ast \gamma$ with $h$ harmonic.