class HasHodgeNumbers {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type

A typeclass packaging the Hodge numbers $h^{p,q}(M)$ and Betti numbers $b_k(M)$ of a compact Kähler manifold, together with the basic symmetries they satisfy: conjugation symmetry $h^{p,q} = h^{q,p}$, Hodge-star symmetry $h^{p,q} = h^{n-q,\,n-p}$, and the link $b_k = \sum_{p+q=k} h^{p,q}$ from the Hodge decomposition $H^k_{dR}(M,\mathbb{C}) = \bigoplus_{p+q=k} H^{p,q}_{\bar\partial}(M)$.

• complexDim : ℕ
• hodge : ℕ → ℕ → ℕ
• conjugation_symmetry (p q : ℕ) : hodge Ω VF p q = hodge Ω VF q p
• star_symmetry (p q : ℕ) : hodge Ω VF p q = hodge Ω VF (complexDim Ω VF - q) (complexDim Ω VF - p)
• betti : ℕ → ℕ
• betti_hodge_link (k : ℕ) : betti Ω VF k = ∑ p ∈ Finset.range (k + 1), hodge Ω VF p (k - p)

theorem hodge_conjugation_symmetry {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) [hH : HasHodgeNumbers] (p q : ℕ) : HasHodgeNumbers.hodge Ω VF p q = HasHodgeNumbers.hodge Ω VF q p

Conjugation symmetry of Hodge numbers on a compact Kähler manifold: $h^{p,q}(M) = h^{q,p}(M)$.

theorem betti_eq_sum_hodge {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) [hH : HasHodgeNumbers] (k : ℕ) : HasHodgeNumbers.betti Ω VF k = ∑ p ∈ Finset.range (k + 1), HasHodgeNumbers.hodge Ω VF p (k - p)

Hodge decomposition consequence: on a compact Kähler manifold the $k$-th Betti number decomposes as a sum of Hodge numbers, $b_k(M) = \sum_{p+q=k} h^{p,q}(M)$.

theorem compact_kahler_odd_betti_even {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (k : ℕ) (hk : k % 2 = 1) [hH : HasHodgeNumbers] : ∃ (m : ℕ), HasHodgeNumbers.betti Ω VF k = 2 * m

On a compact Kähler manifold, all odd Betti numbers are even: for odd $k$, $b_k(M) = 2m$ for some $m \in \mathbb{N}$. This follows from the Hodge decomposition together with the conjugation symmetry $h^{p,q} = h^{q,p}$.

class HasCohomologyWithLefschetz {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] extends HasCohomology : Type (u_3 + 1)

A cohomology structure equipped with iterated Lefschetz operators $L^m : H^k(M) \to H^{k+2m}(M)$. On a compact Kähler manifold these are the linear maps appearing in the Hard Lefschetz theorem.

• H : ℕ → Type u_3
• H_addCommGroup (k : ℕ) : AddCommGroup (H Ω VF k)
• H_module (k : ℕ) : Module ℝ (H Ω VF k)
• H_finiteDimensional (k : ℕ) : FiniteDimensional ℝ (H Ω VF k)
• L_map (k m : ℕ) : HasCohomology.H Ω VF k →ₗ[ℝ] HasCohomology.H Ω VF (k + 2 * m)

class HasProjectiveEmbedding {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type (max (max u_1 (u_3 + 1)) (u_4 + 1))

A projective embedding datum for a symplectic manifold $(M, \omega)$: an embedding $\iota : M \hookrightarrow N$ into a target carrying a closed form $\omega_N$ such that $\iota^* \omega_N = \omega + d\alpha$ for some $\alpha \in \Omega^1(M)$. This is the existence half of the Kodaira embedding theorem.

• embeddingDim : ℕ
• Ω_target : ℕ → Type u_3
• VF_target : Type u_4
• inst_target : DifferentialFormSpace (Ω_target S) (VF_target S)
• embedding : DFSMorphism Ω VF (Ω_target S) (VF_target S)
• targetForm : Ω_target S 2
• targetForm_closed : DifferentialFormSpace.d (VF_target S) targetForm = 0
• pullback_cohomologous : ∃ (α : Ω 1), embedding.pullback targetForm = S.ω + DifferentialFormSpace.d VF α

def HasProjectiveEmbeddingProp {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Prop

Propositional version of HasProjectiveEmbedding: there exists a target differential form space, an embedding, and a closed form whose pullback represents $[\omega]$ in de Rham cohomology.

class IsIntegralClass {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Prop

The symplectic class $[\omega] \in H^2(M, \mathbb{R})$ is integral and nontrivial: no integer multiple $k\omega$ ($k \neq 0$) is exact. This is the hypothesis of the Kodaira embedding theorem.

• not_exact (α : Ω 1) : DifferentialFormSpace.d VF α ≠ S.ω
• smul_not_exact (k : ℤ) : k ≠ 0 → ∀ (α : Ω 1), DifferentialFormSpace.d VF α ≠ k • S.ω

structure HolomorphicBundleStr {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (Sections : Type u_3) [AddCommGroup Sections] (FormsWithValues : ℕ → Type u_4) [(q : ℕ) → AddCommGroup (FormsWithValues q)] : Type u_4

Holomorphic bundle structure: a $(0,1)$-connection operator $\bar\partial_E : \Omega^{0,q}(E) \to \Omega^{0,q+1}(E)$ on $E$-valued forms satisfying the integrability condition $\bar\partial_E^2 = 0$.

• delbar_E {q : ℕ} : FormsWithValues q → FormsWithValues (q + 1)
• delbar_sq {q : ℕ} (σ : FormsWithValues q) : self.delbar_E (self.delbar_E σ) = 0
• delbar_add {q : ℕ} (σ τ : FormsWithValues q) : self.delbar_E (σ + τ) = self.delbar_E σ + self.delbar_E τ

structure HolomorphicSection {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {Sections : Type u_3} [AddCommGroup Sections] {FormsWithValues : ℕ → Type u_4} [(q : ℕ) → AddCommGroup (FormsWithValues q)] (hol : HolomorphicBundleStr Sections FormsWithValues) (toSections : Sections → FormsWithValues 0) : Type u_3

A holomorphic section of a holomorphic bundle: a section $\sigma$ such that $\bar\partial_E \sigma = 0$.

• section_ : Sections
• is_holomorphic : hol.delbar_E (toSections self.section_) = 0

structure HermitianBundleMetric (R : Type u_1) [Ring R] : Type u_1

A Hermitian metric datum on a line bundle, represented abstractly by an invertible element $h \in R$ in a ring of bundle endomorphisms.

• h : R
• h_inv : R
• h_inv_left : self.h_inv * self.h = 1
• h_right_inv : self.h * self.h_inv = 1

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

Data attached to a Hermitian line bundle: a closed curvature $2$-form $R^\nabla \in \Omega^2(M)$ representing $2\pi \cdot c_1(L) \in H^2(M, \mathbb{R})$.

• curvature : Ω 2
• curvature_closed : DifferentialFormSpace.d VF self.curvature = 0

class IsAmple {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (L : LineBundleData) : Prop

A line bundle $L$ is ample if its curvature form is nondegenerate, i.e. $X \mapsto \iota_X R^\nabla$ is injective. Geometrically this expresses positivity of $c_1(L)$.

• positive_curvature : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X L.curvature

class IsVeryAmple {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (L : LineBundleData) : Prop

A line bundle is very ample if its global sections separate points, giving an embedding into projective space; the curvature is still positive and there exist nontrivial sections distinguishing points.

• sections_give_embedding : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X L.curvature
• has_sections : ∃ (s₁ : Ω 0) (s₂ : Ω 0), s₁ ≠ s₂ ∧ DifferentialFormSpace.d VF s₁ ≠ DifferentialFormSpace.d VF s₂

class IsKahlerForm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (ω : Ω 2) : Prop

A $2$-form $\omega$ is a Kähler form if it is closed ($d\omega = 0$) and nondegenerate ($X \mapsto \iota_X \omega$ is injective).

• closed : DifferentialFormSpace.d VF ω = 0
• nondegenerate : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω

structure ApproxHolomorphicSectionFamily {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type (max u_1 u_2)

An approximately-holomorphic family of sections of a line bundle $L$: for each $k$ and each point $p$, a section $s_{k,p} \in \Omega^0(L^k)$. Used in Donaldson's construction of approximately holomorphic sections.

• L : LineBundleData
• section_ : ℕ → VF → Ω 0

class L2NormSpace (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

An $L^2$-norm structure on differential forms: a seminorm $\|\cdot\|_{L^2}$ on each $\Omega^p$ satisfying the triangle inequality and the scaling law $\|r\cdot\alpha\|_{L^2} = |r|\cdot\|\alpha\|_{L^2}$.

• l2norm {p : ℕ} : Ω p → ℝ
• l2norm_nonneg {p : ℕ} (α : Ω p) : 0 ≤ l2norm VF α
• l2norm_add {p : ℕ} (α β : Ω p) : l2norm VF (α + β) ≤ l2norm VF α + l2norm VF β
• l2norm_smul {p : ℕ} (r : ℝ) (α : Ω p) : l2norm VF (r • α) = |r| * l2norm VF α

class WeightedDerivSupNorm (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

A scale-weighted $C^r$ sup-norm on sections: for each scale $k$ and order $r$, a seminorm $\|s\|_{k,r}$ controlling derivatives up to order $r$ with weights appropriate to the scale-$k$ geometry (used in Donaldson estimates).

• weighted_supnorm (k r : ℕ) : Ω 0 → ℝ
• weighted_supnorm_nonneg (k r : ℕ) (s : Ω 0) : 0 ≤ weighted_supnorm VF k r s
• weighted_supnorm_add (k r : ℕ) (s t : Ω 0) : weighted_supnorm VF k r (s + t) ≤ weighted_supnorm VF k r s + weighted_supnorm VF k r t
• weighted_supnorm_neg (k r : ℕ) (s : Ω 0) : weighted_supnorm VF k r (-s) ≤ weighted_supnorm VF k r s

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

Pointwise evaluation of $0$-forms (i.e. functions/sections): a map $(x, s) \mapsto |s(x)|$ taking nonnegative values and bounded by the weighted $C^0$ sup-norm.

• peval : VF → Ω 0 → ℝ
• peval_nonneg (x : VF) (s : Ω 0) : 0 ≤ peval x s
• peval_le_supnorm (wdn : WeightedDerivSupNorm Ω) (x : VF) (k : ℕ) (s : Ω 0) : peval x s ≤ WeightedDerivSupNorm.weighted_supnorm VF k 0 s

class ManifoldDist (VF : Type u_1) : Type u_1

A distance function on the manifold (representing the Riemannian/Kähler metric distance), satisfying the standard axioms of a pseudo-metric: nonnegativity, symmetry, $d(p,p) = 0$, and the triangle inequality.

• mdist : VF → VF → ℝ
• mdist_nonneg (p q : VF) : 0 ≤ mdist p q
• mdist_symm (p q : VF) : mdist p q = mdist q p
• mdist_self (p : VF) : mdist p p = 0
• mdist_triangle (p q r : VF) : mdist p r ≤ mdist p q + mdist q r

structure IsUniformlyBounded {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (fam : ApproxHolomorphicSectionFamily) : Prop

A section family is uniformly bounded if its derivatives in every weighted $C^r$ norm are bounded uniformly in $k$ and $p$.

• deriv_bounded : ∃ (wdn : WeightedDerivSupNorm Ω), ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p) ≤ C_r

structure IsApproxHolomorphic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (fam : ApproxHolomorphicSectionFamily) : Prop

A section family is approximately holomorphic: $\bar\partial s_{k,p}$ is exact and its $L^2$-norm decays like $1/\sqrt{k}$, which is the precise Donaldson approximate-holomorphicity condition.

• delbar_exact (dol : DolbeaultOps) (k : ℕ) (p : VF) : ∃ (β : Ω 0), dol.delbar (fam.section_ k p) = DifferentialFormSpace.d VF β
• delbar_l2_decay : ∃ (l2 : L2NormSpace Ω), ∃ C > 0, ∀ (dol : DolbeaultOps) (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C / √↑k

structure IsUniformlyConcentrated {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (fam : ApproxHolomorphicSectionFamily) : Prop

A section family is uniformly concentrated: distinct base points give distinct sections, the sections exhibit Gaussian decay $|s_{k,p}(x)| \lesssim (1 + \sqrt{k}\,d(p,x))^N e^{-\lambda k\, d(p,x)^2}$ away from $p$, and derivative norms are uniformly bounded.

• concentrated (k : ℕ) (p q : VF) : p ≠ q → fam.section_ k p ≠ fam.section_ k q
• gaussian_decay : ∃ (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (C_gd : ℝ) (lam : ℝ) (N : ℕ), C_gd > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p x : VF), PointwiseEval.peval x (fam.section_ k p) ≤ C_gd * (1 + (√↑k * ManifoldDist.mdist p x) ^ N) * Real.exp (-lam * ↑k * ManifoldDist.mdist p x ^ 2)
• deriv_norm_bounded : ∃ (wdn : WeightedDerivSupNorm Ω), ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p) ≤ C_r

structure IsHolomorphicFamily {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) : Prop

A section family is genuinely holomorphic if $\bar\partial s_{k,p} = 0$ for every $k$ and $p$.

• holomorphic (k : ℕ) (p : VF) : dol.delbar (fam.section_ k p) = 0

class HasGaussianSections (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] : Prop

Existence axiom: a compact symplectic manifold equipped with a compatible almost complex structure admits a family of approximately-holomorphic sections that are simultaneously uniformly bounded, approximately holomorphic, uniformly concentrated, and locally bounded below by Gaussian peaks.

• sections_exist (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hcompat : IsCompatibleACS S J) : ∃ (fam : ApproxHolomorphicSectionFamily), IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ ∃ (pe : PointwiseEval Ω VF) (md : ManifoldDist VF), ∃ c > 0, ∀ (k : ℕ) (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)

structure WeitzenboeckDecomposition (V : Type u_1) [AddCommGroup V] : Type u_1

Abstract data for a Weitzenböck decomposition $\bar\square = D + R$, where $D$ is a positive second-order operator and $R$ is a $0$-th order curvature term acting on a vector space of $k$-forms; both are additive.

• D : V → V
• R_term : V → V
• k : ℕ
• D_add (a b : V) : self.D (a + b) = self.D a + self.D b
• R_add (a b : V) : self.R_term (a + b) = self.R_term a + self.R_term b

class HasGreenOperator (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) : Type u_1

A Green operator for the $\bar\partial$-Laplacian: produces a correction $\xi = G(s)$ such that $s + \xi$ is holomorphic and the $L^2$-norm of $\xi$ is controlled by $1/\sqrt{k}$ times the $L^2$-norm of $\bar\partial s$, encoding the spectral gap of $\bar\square$ on $L^k$.

• greenCorrection : ℕ → Ω 0 → Ω 0
• green_holomorphic (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : dol.delbar (s + greenCorrection l2 dol k s) = 0
• green_l2_sq_bound (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : ∃ c > 0, L2NormSpace.l2norm VF (greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (greenCorrection l2 dol k s) ≤ c / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))

theorem l2_bound_from_squared_bound {a b C : ℝ} {k : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hCk : 0 ≤ C / ↑k) (hsq : a * a ≤ C / ↑k * (b * b)) : a ≤ √(C / ↑k) * b

Helper: from a squared bound $a^2 \le (C/k) b^2$ with $a, b \ge 0$ and $C/k \ge 0$, conclude the linear bound $a \le \sqrt{C/k}\, b$.

theorem sqrt_div_eq_div_sqrt {C : ℝ} {k : ℕ} (hC : 0 < C) (_hk : k ≠ 0) : √(C / ↑k) = √C / √↑k

Helper algebraic identity: $\sqrt{C/k} = \sqrt{C}/\sqrt{k}$ for $C > 0$ and $k \ne 0$.

structure HasGaussianDecayOfDelbar {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) : Prop

The hypothesis that $\bar\partial s_{k,p}$ decays exponentially in $k^{1/3}$: $\|\bar\partial s_{k,p}\|_{L^2} \le C e^{-\lambda k^{1/3}}$. This is the form of cutoff-error bound used in Donaldson's argument.

• gaussian_decay : ∃ (lam : ℝ) (C : ℝ), lam > 0 ∧ C > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C * Real.exp (-lam * ↑k ^ (1 / 3))

structure HasCauchyEstimates {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) : Prop

Cauchy-type estimates for holomorphic sections: weighted $C^r$ norms of a holomorphic section $\xi$ (with $\bar\partial \xi = 0$) are controlled by its $L^2$-norm.

• cauchy_bound (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (ξ : Ω 0), dol.delbar ξ = 0 → WeightedDerivSupNorm.weighted_supnorm VF k r ξ ≤ C_r * L2NormSpace.l2norm VF ξ

structure IsQuantUniformlyBounded {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (fam : ApproxHolomorphicSectionFamily) : Prop

Quantitative form of uniform boundedness for a section family with respect to an explicit weighted derivative sup-norm.

• deriv_bound (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p) ≤ C_r

structure IsQuantApproxHolomorphic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (fam : ApproxHolomorphicSectionFamily) : Prop

Quantitative form of approximate holomorphicity: $\bar\partial$ of each section is exact and its $L^2$-norm satisfies the explicit $C/\sqrt{k}$ decay bound.

• delbar_exact (dol : DolbeaultOps) (k : ℕ) (p : VF) : ∃ (β : Ω 0), dol.delbar (fam.section_ k p) = DifferentialFormSpace.d VF β
• delbar_l2_bound : ∃ C > 0, ∀ (dol : DolbeaultOps) (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C / √↑k

structure IsQuantUniformlyConcentrated {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (fam : ApproxHolomorphicSectionFamily) : Prop

Quantitative form of uniform concentration: distinct base points yield distinct sections, derivative norms are uniformly bounded, and the sections exhibit explicit Gaussian decay away from their peak.

• concentrated (k : ℕ) (p q : VF) : p ≠ q → fam.section_ k p ≠ fam.section_ k q
• norm_bounded (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p) ≤ C_r
• gaussian_decay : ∃ (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (C_gd : ℝ) (lam : ℝ) (N : ℕ), C_gd > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p x : VF), PointwiseEval.peval x (fam.section_ k p) ≤ C_gd * (1 + (√↑k * ManifoldDist.mdist p x) ^ N) * Real.exp (-lam * ↑k * ManifoldDist.mdist p x ^ 2)

structure IsExponentiallyClose {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (fam fam' : ApproxHolomorphicSectionFamily) : Prop

Two families on the same line bundle are exponentially close if all weighted derivative differences decay like $e^{-\lambda k / 3}$.

• same_bundle : fam.L = fam'.L
• exp_close_all_derivs : ∃ lam > 0, ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p - fam'.section_ k p) ≤ C_r * Real.exp (-lam * ↑k / 3)

structure IsExponentiallyCloseCubeRoot {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (fam fam' : ApproxHolomorphicSectionFamily) : Prop

Cube-root version of exponential closeness: the decay rate is $e^{-\lambda k^{1/3}}$ instead of $e^{-\lambda k}$, which is the natural rate provided by Donaldson's argument.

• same_bundle : fam.L = fam'.L
• exp_close_all_derivs : ∃ lam > 0, ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p - fam'.section_ k p) ≤ C_r * Real.exp (-lam * ↑k ^ (1 / 3))

theorem nat_rpow_one_third_le (k : ℕ) (hk : 1 ≤ k) : ↑k ^ (1 / 3) ≤ ↑k

For $k \ge 1$, the cube root $k^{1/3}$ is bounded above by $k$.

theorem exp_neg_linear_le_exp_neg_cuberoot (lam : ℝ) (hlam : 0 < lam) (k : ℕ) : Real.exp (-lam * ↑k / 3) ≤ Real.exp (-(lam / 3) * ↑k ^ (1 / 3))

Convexity-style comparison: $e^{-\lambda k / 3} \le e^{-(\lambda/3) k^{1/3}}$ for $\lambda > 0$ and all $k \in \mathbb{N}$, used to convert linear decay into cube-root decay.

theorem IsExponentiallyClose.to_cube_root {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {wdn : WeightedDerivSupNorm Ω} {fam fam' : ApproxHolomorphicSectionFamily} (h : IsExponentiallyClose wdn fam fam') : IsExponentiallyCloseCubeRoot wdn fam fam'

Linear exponential closeness implies cube-root exponential closeness: the rate $e^{-\lambda k}$ dominates $e^{-(\lambda/3) k^{1/3}}$.

structure HasLocalLowerBound {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (fam : ApproxHolomorphicSectionFamily) : Prop

A section family has a uniform local lower bound: each section is nonzero, its weighted $C^0$ norm is uniformly bounded below, and there is a uniform lower bound on $|s_{k,p}(q)|$ when $d(p,q) \le 1/\sqrt{k}$ (the natural scale-$k$ ball).

• section_nonzero (k : ℕ) (p : VF) : fam.section_ k p ≠ 0
• lower_bound_exists : ∃ c > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k 0 (fam.section_ k p) ≥ c
• ball_lower_bound : ∃ (pe : PointwiseEval Ω VF) (md : ManifoldDist VF), ∃ c > 0, ∀ (k : ℕ) (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)

noncomputable def kahler_curvature_lower_bound {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (l2 : L2NormSpace Ω) (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (dol : DolbeaultOps) : (greenCorrection : ℕ → Ω 0 → Ω 0) ×' (C_geom : ℝ) ×' C_geom > 0 ∧ (∀ (k : ℕ) (s : Ω 0), ↑k > C_geom → L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ 1 / (↑k - C_geom) * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) ∧ ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), ∃ B > 0, L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ B * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))

Existence of a Green operator with spectral-gap bounds coming from the Kähler curvature estimate. Returns a Green correction $G$ along with a positive geometric constant $C_{geom}$ controlling the $L^2 \to L^2$ norm $\|G\|^2 \le 1/(k - C_{geom}) \cdot \|\bar\partial\|^2$ for $k$ large, and a weaker bound for small $k$.

theorem spectral_gap_from_curvature_bound {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (greenCorrection : ℕ → Ω 0 → Ω 0) (C_geom : ℝ) (hC_pos : C_geom > 0) (hcurv_bound : ∀ (k : ℕ) (s : Ω 0), ↑k > C_geom → L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ 1 / (↑k - C_geom) * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) (hgeneral_bound : ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), ∃ B > 0, L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ B * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : ∃ c > 0, L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ c / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))

Combines a "large $k$" curvature bound (of the form $1/(k - C_{geom})$) with a "small $k$" general bound to produce a single spectral-gap estimate $\|G(s)\|^2 \le (c/k) \|\bar\partial s\|^2$ valid for all $k \ge 1$.

theorem hodge_orthogonality {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (l2 : L2NormSpace Ω) (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (dol : DolbeaultOps) (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : dol.delbar (s + (kahler_curvature_lower_bound l2 S J hK dol).fst k s) = 0

Hodge orthogonality / harmonic projection: on a compact Kähler manifold, the Green correction $G(s)$ produced by kahler_curvature_lower_bound makes $s + G(s)$ holomorphic for every $s \in \Omega^0$ and every $k \ne 0$.

noncomputable def green_function_existence {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (l2 : L2NormSpace Ω) (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (dol : DolbeaultOps) : HasGreenOperator Ω l2 dol

Existence of a Green operator on a compact Kähler manifold, packaged from the curvature lower bound, the spectral gap, and Hodge orthogonality.

structure GreenCorrectionInput {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) : Type u_1

Bundled input data for applying Green-operator corrections to a family of approximately-holomorphic sections: a Green operator, a Gaussian decay bound for $\bar\partial$, Cauchy estimates on the correction, an $L^2$-bound on the correction, holomorphicity at $k=0$, and bundle-equality data.

• greenOp : HasGreenOperator Ω l2 dol
• gaussian_decay : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))
• cauchy_estimates (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (HasGreenOperator.greenCorrection l2 dol k s) ≤ C_r * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s)
• correction_l2_exp_bound : ∃ (C_l2 : ℝ) (lam_l2 : ℝ), C_l2 > 0 ∧ lam_l2 > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k (fam.section_ k p)) ≤ C_l2 * Real.exp (-lam_l2 * ↑k ^ (1 / 3))
• hol_at_zero (p : VF) : dol.delbar (fam.section_ 0 p + HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) = 0
• same_bundle_data : LineBundleData
• corrected_bundle_eq : fam.L = self.same_bundle_data

noncomputable def correctedFamily {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (gci : GreenCorrectionInput wdn l2 dol fam) : ApproxHolomorphicSectionFamily

The Green-corrected section family: replaces each $s_{k,p}$ by $s_{k,p} + G(s_{k,p})$, producing a (genuinely) holomorphic family on the same line bundle.

theorem green_corrected_family_is_holomorphic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (gci : GreenCorrectionInput wdn l2 dol fam) : IsHolomorphicFamily dol (correctedFamily wdn l2 dol fam gci)

The Green-corrected family is genuinely holomorphic: $\bar\partial$ of every corrected section vanishes (using the Green operator's defining property for $k \ne 0$ and the hol_at_zero hypothesis for $k = 0$).

theorem green_correction_exp_close {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (gci : GreenCorrectionInput wdn l2 dol fam) : IsExponentiallyCloseCubeRoot wdn fam (correctedFamily wdn l2 dol fam gci)

The Green-corrected family is exponentially close (at the $k^{1/3}$ rate) to the original family: combining the Cauchy estimates with the exponential $L^2$-bound on the correction gives the required uniform $\|s_{k,p} - s'_{k,p}\|_{k,r} \le C_r e^{-\lambda k^{1/3}}$ bound.

structure HasHolomorphicCorrection {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (wdn : WeightedDerivSupNorm Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) : Type (max u_1 u_2)

A "Donaldson correction" witness for a section family: a corrected holomorphic family together with the proof that it is exponentially close (cube-root rate) to the original.

• corrected_family : ApproxHolomorphicSectionFamily
• is_holomorphic : IsHolomorphicFamily dol self.corrected_family
• is_exp_close : IsExponentiallyCloseCubeRoot wdn fam self.corrected_family

class HasPDEInfrastructure (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] : Type (max u_1 u_2)

The PDE infrastructure required to run the Green-correction construction: a weighted derivative sup-norm, an $L^2$-norm, the Dolbeault operator, and a recipe for producing GreenCorrectionInput for any section family.

• wdn : WeightedDerivSupNorm Ω
• l2 : L2NormSpace Ω
• dol : DolbeaultOps
• greenCorrection (fam : ApproxHolomorphicSectionFamily) : GreenCorrectionInput wdn l2 dol fam

structure UniformGreenL2Bound {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (greenOp : (l2 : L2NormSpace Ω) → (dol : DolbeaultOps) → HasGreenOperator Ω l2 dol) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) : Type

A uniform-in-norm constant $c_G > 0$ such that for every $k \ne 0$ and $s \in \Omega^0$, $\|G(s)\|_{L^2}^2 \le (c_G/k)\, \|\bar\partial s\|_{L^2}^2$. This expresses the spectral gap of $\bar\square$ uniformly across $L^k$.

• c_G : ℝ
• c_G_pos : self.c_G > 0
• uniform_bound (k : ℕ) (hk : k ≠ 0) (s : Ω 0) : L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) ≤ self.c_G / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))

theorem derive_correction_l2_exp_bound {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] {l2 : L2NormSpace Ω} {dol : DolbeaultOps} {greenOp : HasGreenOperator Ω l2 dol} {fam : ApproxHolomorphicSectionFamily} (c_G : ℝ) (hcG_pos : c_G > 0) (h_green_sq : ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) ≤ c_G / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) (C_g lam : ℝ) (hCg_pos : C_g > 0) (hlam_pos : lam > 0) (h_gauss : ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) (h_zero : ∀ (p : VF), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) ≤ √c_G * C_g * Real.exp (-lam * 0 ^ (1 / 3))) : ∃ (C_l2 : ℝ) (lam_l2 : ℝ), C_l2 > 0 ∧ lam_l2 > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k (fam.section_ k p)) ≤ C_l2 * Real.exp (-lam_l2 * ↑k ^ (1 / 3))

Derives an exponential $L^2$-bound on the Green correction from a uniform spectral-gap bound and a Gaussian decay bound on $\bar\partial s_{k,p}$: the output bound is $\|G(s_{k,p})\|_{L^2} \le C_{L^2} e^{-\lambda k^{1/3}}$.

noncomputable def buildGreenCorrectionInput {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (greenOp : HasGreenOperator Ω l2 dol) (c_G : ℝ) (hcG_pos : c_G > 0) (h_green_sq : ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) ≤ c_G / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) (h_gauss : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) (h_cauchy : ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (HasGreenOperator.greenCorrection l2 dol k s) ≤ C_r * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s)) (h_hol_zero : ∀ (p : VF), dol.delbar (fam.section_ 0 p + HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) = 0) (bundle_data : LineBundleData) (h_bundle_eq : fam.L = bundle_data) (h_l2_zero : ∀ (C_g lam : ℝ), C_g > 0 → lam > 0 → (∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) → ∀ (p : VF), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) ≤ √c_G * C_g * Real.exp (-lam * 0 ^ (1 / 3))) : GreenCorrectionInput wdn l2 dol fam

Assembles a GreenCorrectionInput from its constituent estimates: a Green operator, uniform spectral-gap constant, Gaussian decay of $\bar\partial$, Cauchy estimates, $k=0$ holomorphicity, and bundle data.

structure GaussianPeakData {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hcompat : IsCompatibleACS S J) : Type (max u_1 u_2)

Bundled "Gaussian peak section" data on a compatibly-almost-complex symplectic manifold: a line bundle, a section family, and all the analytic infrastructure (norms, pointwise evaluation, distance) together with the uniform bound, Gaussian decay, concentration, and local lower-bound estimates that comprise Donaldson's peak sections.

• L : LineBundleData
• section_ : ℕ → VF → Ω 0
• pe : PointwiseEval Ω VF
• md : ManifoldDist VF
• wdn : WeightedDerivSupNorm Ω
• l2 : L2NormSpace Ω
• uniform_bound (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (self.section_ k p) ≤ C_r
• delbar_exact (dol : DolbeaultOps) (k : ℕ) (p : VF) : ∃ (β : Ω 0), dol.delbar (self.section_ k p) = DifferentialFormSpace.d VF β
• delbar_l2_decay : ∃ C > 0, ∀ (dol : DolbeaultOps) (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (self.section_ k p)) ≤ C / √↑k
• concentrated (k : ℕ) (p q : VF) : p ≠ q → self.section_ k p ≠ self.section_ k q
• gaussian_decay : ∃ (C_gd : ℝ) (lam : ℝ) (N : ℕ), C_gd > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p x : VF), PointwiseEval.peval x (self.section_ k p) ≤ C_gd * (1 + (√↑k * ManifoldDist.mdist p x) ^ N) * Real.exp (-lam * ↑k * ManifoldDist.mdist p x ^ 2)
• local_lower_bound : ∃ c > 0, ∀ (k : ℕ) (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (self.section_ k p)

class HasGaussianPeakData (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hcompat : IsCompatibleACS S J) : Type (max u_1 u_2)

Typeclass assumption that GaussianPeakData is available for a given compact symplectic manifold with a compatible almost-complex structure.

• peakData : GaussianPeakData S J hcompat

theorem gaussian_peak_sections_exist_sorry {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hcompat : IsCompatibleACS S J) [HasGaussianPeakData Ω S J _hcompat] : ∃ (fam : ApproxHolomorphicSectionFamily), IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ ∃ (pe : PointwiseEval Ω VF) (md : ManifoldDist VF), ∃ c > 0, ∀ (k : ℕ) (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)

Existence of Donaldson's Gaussian peak sections, derived directly from the packaged GaussianPeakData: a uniformly-bounded, approximately-holomorphic, uniformly-concentrated section family with a local lower bound on Gaussian peaks.

class HasWeitzenbockDecomp (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) : Type u_1

Abstract Weitzenböck decomposition data on a compact symplectic manifold: a Green correction, its holomorphicity property, a spectral-gap squared bound, and a uniform spectral-gap constant $c_G$.

• greenCorrection : ℕ → Ω 0 → Ω 0
• green_holomorphic (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : dol.delbar (s + greenCorrection l2 dol k s) = 0
• green_l2_sq_bound (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : ∃ c > 0, L2NormSpace.l2norm VF (greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (greenCorrection l2 dol k s) ≤ c / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))
• c_G : ℝ
• c_G_pos : c_G l2 dol > 0
• uniform_l2_bound (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : L2NormSpace.l2norm VF (greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (greenCorrection l2 dol k s) ≤ c_G l2 dol / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))

noncomputable def HasWeitzenbockDecomp.toHasGreenOperator {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [wb : HasWeitzenbockDecomp Ω l2 dol] : HasGreenOperator Ω l2 dol

Forget the uniform Weitzenböck constant: a HasWeitzenbockDecomp instance yields a HasGreenOperator instance.

noncomputable def weitzenbock_green_operator_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [wb : HasWeitzenbockDecomp Ω l2 dol] : HasGreenOperator Ω l2 dol

Convenience alias: the Green operator obtained from HasWeitzenbockDecomp.

noncomputable def weitzenbock_uniform_constant_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [wb : HasWeitzenbockDecomp Ω l2 dol] : ℝ

The uniform Weitzenböck constant $c_G$ extracted from a HasWeitzenbockDecomp instance.

theorem weitzenbock_uniform_constant_pos {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [wb : HasWeitzenbockDecomp Ω l2 dol] : weitzenbock_uniform_constant_axiom l2 dol > 0

Positivity of the Weitzenböck constant: $c_G > 0$.

theorem weitzenbock_uniform_l2_bound_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [wb : HasWeitzenbockDecomp Ω l2 dol] (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s) ≤ weitzenbock_uniform_constant_axiom l2 dol / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))

Uniform $L^2$ bound from the Weitzenböck decomposition: for all $k \ne 0$, $\|G(s)\|_{L^2}^2 \le (c_G/k)\, \|\bar\partial s\|_{L^2}^2$.

theorem mul_exp_neg_le_exp_neg_one (y : ℝ) : y * Real.exp (-y) ≤ Real.exp (-1)

Elementary inequality: $y \cdot e^{-y} \le e^{-1}$ for all $y \in \mathbb{R}$, attained at $y = 1$.

theorem t_exp_neg_lam_t_bound (t lam : ℝ) (hlam_pos : lam > 0) : t * Real.exp (-lam * t) ≤ 1 / (lam * Real.exp 1)

Rescaled form of mul_exp_neg_le_exp_neg_one: $t \cdot e^{-\lambda t} \le 1 / (\lambda e)$ for $\lambda > 0$ and all $t \in \mathbb{R}$.

theorem absorb_poly_into_exp (A lam0 : ℝ) (hA : A > 0) (hlam0 : lam0 > 0) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (t : ℝ), 0 ≤ t → A * t * Real.exp (-lam0 * t) ≤ C_g * Real.exp (-lam * t)

Absorption lemma: $A\,t\,e^{-\lambda_0 t} \le C_g\, e^{-\lambda t}$ for some $C_g, \lambda > 0$ and all $t \ge 0$. The polynomial factor $t$ is absorbed into a slightly smaller exponential rate.

structure CutoffGaussianData {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) : Type

Cutoff-localized Gaussian decay data: the $\bar\partial$ of the cutoff peak section satisfies $\|\bar\partial s_{k,p}\|_{L^2} \le A_{\sup}\, k^{1/3} e^{-\lambda_0 k^{1/3}}$. After absorption (via absorb_poly_into_exp) this becomes the exponential bound used in the Donaldson construction.

• A_sup : ℝ
• A_sup_pos : self.A_sup > 0
• lam_0 : ℝ
• lam_0_pos : self.lam_0 > 0
• l2_delbar_bound (k : ℕ) (p : VF) : L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ self.A_sup * ↑k ^ (1 / 3) * Real.exp (-self.lam_0 * ↑k ^ (1 / 3))

theorem derive_gaussian_l2_bound' {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] {l2 : L2NormSpace Ω} {dol : DolbeaultOps} {fam : ApproxHolomorphicSectionFamily} (cgd : CutoffGaussianData l2 dol fam) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))

Convert a CutoffGaussianData polynomial-times-exponential bound into a pure exponential bound: $\|\bar\partial s_{k,p}\|_{L^2} \le C_g\, e^{-\lambda k^{1/3}}$.

class HasDonaldsonPDEData (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] : Type (max u_1 u_2)

Donaldson's PDE-axiom package: provides cutoff Gaussian data for every section family, Cauchy estimates for every Green operator, holomorphicity of the corrected $k=0$ section, and the $L^2$ zero-edge correction bound.

• cutoffGaussianData (fam : ApproxHolomorphicSectionFamily) : CutoffGaussianData l2 dol fam
• cauchyEstimates (greenOp : HasGreenOperator Ω l2 dol) (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (HasGreenOperator.greenCorrection l2 dol k s) ≤ C_r * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s)
• correctionHolAtZero (fam : ApproxHolomorphicSectionFamily) (p : VF) : dol.delbar (fam.section_ 0 p + HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) = 0
• correctionL2ZeroEdge (fam : ApproxHolomorphicSectionFamily) (c_G C_g lam : ℝ) : C_g > 0 → lam > 0 → (∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) → ∀ (p : VF), L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) ≤ √c_G * C_g * Real.exp (-lam * 0 ^ (1 / 3))

noncomputable def cutoff_gaussian_data_exists' {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [hpde : HasDonaldsonPDEData Ω wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) : CutoffGaussianData l2 dol fam

Pull the cutoff Gaussian data out of the Donaldson PDE-axioms instance.

theorem cauchy_estimates_for_green_op' {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [hpde : HasDonaldsonPDEData Ω wdn l2 dol] (greenOp : HasGreenOperator Ω l2 dol) (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (HasGreenOperator.greenCorrection l2 dol k s) ≤ C_r * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s)

Cauchy estimates for the Green correction of any Green operator, taken from the Donaldson PDE axioms.

theorem gaussian_decay_delbar_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [HasDonaldsonPDEData Ω wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))

Exponential ($k^{1/3}$) Gaussian decay of $\bar\partial$ on any section family, derived from the cutoff Gaussian data via absorption.

theorem cauchy_estimates_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [HasDonaldsonPDEData Ω wdn l2 dol] (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (HasGreenOperator.greenCorrection l2 dol k s) ≤ C_r * L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol k s)

Cauchy estimates specialized to the Weitzenböck-derived Green operator.

theorem correction_hol_at_zero_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (_wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [hpde : HasDonaldsonPDEData Ω _wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) (p : VF) : dol.delbar (fam.section_ 0 p + HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) = 0

The corrected section at $k = 0$ is holomorphic: $\bar\partial(s_{0,p} + G(s_{0,p})) = 0$.

noncomputable def correction_bundle_data_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (fam : ApproxHolomorphicSectionFamily) : LineBundleData

Trivial wrapper: extract the underlying line bundle data from a section family.

theorem correction_bundle_eq_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (fam : ApproxHolomorphicSectionFamily) : fam.L = correction_bundle_data_axiom fam

Reflexivity: fam.L is the same as correction_bundle_data_axiom fam.

theorem correction_l2_zero_edge_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (_wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [hpde : HasDonaldsonPDEData Ω _wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) (c_G C_g lam : ℝ) (_hCg_pos : C_g > 0) (_hlam_pos : lam > 0) (_h_gauss : ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) (p : VF) : L2NormSpace.l2norm VF (HasGreenOperator.greenCorrection l2 dol 0 (fam.section_ 0 p)) ≤ √c_G * C_g * Real.exp (-lam * 0 ^ (1 / 3))

Edge case bound: at $k = 0$ the $L^2$-norm of the Green correction is controlled by $\sqrt{c_G}\, C_g\, e^{-\lambda \cdot 0^{1/3}}$, used to initialize the inductive Donaldson construction.

noncomputable def green_correction_data_sorry {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [HasDonaldsonPDEData Ω wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) : GreenCorrectionInput wdn l2 dol fam

Assemble the full GreenCorrectionInput for a family using the Weitzenböck decomposition, the cutoff Gaussian decay, Cauchy estimates, and the $k=0$ zero-edge bound provided by the Donaldson PDE axioms.

class HasDonaldsonProofData (Ω : ℕ → Type u_1) {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hcompat : IsCompatibleACS S J) : Type (max u_1 u_2)

Bundles all data needed to run Donaldson's Proposition 1 proof on a compact symplectic manifold with compatible almost-complex structure: a weighted sup-norm, an $L^2$-norm, a Dolbeault operator, Gaussian peak sections, a Weitzenböck decomposition, and the PDE-axioms package.

• wdn : WeightedDerivSupNorm Ω
• l2 : L2NormSpace Ω
• dol : DolbeaultOps
• gaussianPeakInst : HasGaussianPeakData Ω S J hcompat
• weitzenbockInst : HasWeitzenbockDecomp Ω (l2 hcompat) (dol hcompat)
• pdeDataInst : HasDonaldsonPDEData Ω (wdn hcompat) (l2 hcompat) (dol hcompat)

theorem donaldson_prop1_legacy_internal {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (_hcompat : IsCompatibleACS S J) [hpd : HasDonaldsonProofData Ω S J _hcompat] : ∃ (k₀ : ℕ) (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (fam : ApproxHolomorphicSectionFamily), 1 ≤ k₀ ∧ IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ (∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)) ∧ ∃ (fam' : ApproxHolomorphicSectionFamily), IsHolomorphicFamily (HasDonaldsonProofData.dol _hcompat) fam' ∧ IsExponentiallyCloseCubeRoot (HasDonaldsonProofData.wdn _hcompat) fam fam'

Legacy internal version of Donaldson's Proposition 1: on a compact Kähler manifold with the full HasDonaldsonProofData, there exist approximately holomorphic sections with Gaussian peak structure and an exponentially-close genuinely holomorphic family.

theorem donaldson_gaussian_peak_sections {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (_hcompat : IsCompatibleACS S J) [HasGaussianPeakData Ω S J _hcompat] : ∃ (fam : ApproxHolomorphicSectionFamily), IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ ∃ (pe : PointwiseEval Ω VF) (md : ManifoldDist VF), ∃ c > 0, ∀ (k : ℕ) (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)

Donaldson's Gaussian peak sections on a compact Kähler manifold, in their externally-facing form: a uniformly-bounded, approximately-holomorphic, uniformly-concentrated family with local lower bounds.

structure GreenCorrectionPDEAxioms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) : Type u_1

The PDE-axioms package for a Green correction operator on a specific section family: the Green correction, its holomorphicity, the uniform spectral gap, Gaussian decay of $\bar\partial$, Cauchy estimates, $k=0$ holomorphicity, bundle data, and the $L^2$-bound at $k=0$.

• greenCorrection : ℕ → Ω 0 → Ω 0
• green_holomorphic (k : ℕ) (_hk : k ≠ 0) (s : Ω 0) : dol.delbar (s + self.greenCorrection k s) = 0
• uniform_spectral_gap : ∃ C > 0, ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), L2NormSpace.l2norm VF (self.greenCorrection k s) * L2NormSpace.l2norm VF (self.greenCorrection k s) ≤ C / ↑k * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))
• gaussian_decay : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))
• cauchy_estimates (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (self.greenCorrection k s) ≤ C_r * L2NormSpace.l2norm VF (self.greenCorrection k s)
• hol_at_zero (p : VF) : dol.delbar (fam.section_ 0 p + self.greenCorrection 0 (fam.section_ 0 p)) = 0
• same_bundle_data : LineBundleData
• corrected_bundle_eq : fam.L = self.same_bundle_data
• correction_l2_at_zero : ∃ B > 0, ∀ (p : VF), L2NormSpace.l2norm VF (self.greenCorrection 0 (fam.section_ 0 p)) ≤ B

theorem correction_l2_exp_bound_from_spectral_gap {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (pde : GreenCorrectionPDEAxioms wdn l2 dol fam) : ∃ (C_l2 : ℝ) (lam_l2 : ℝ), C_l2 > 0 ∧ lam_l2 > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (pde.greenCorrection k (fam.section_ k p)) ≤ C_l2 * Real.exp (-lam_l2 * ↑k ^ (1 / 3))

From the uniform spectral gap, Gaussian decay of $\bar\partial$, and the $L^2$-bound at $k = 0$, derive the exponential $L^2$-bound for the Green correction at every $k$: $\|G(s_{k,p})\|_{L^2} \le C_{L^2}\, e^{-\lambda k^{1/3}}$.

noncomputable def GreenCorrectionInput_of_pde_axioms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (pde : GreenCorrectionPDEAxioms wdn l2 dol fam) : GreenCorrectionInput wdn l2 dol fam

Convert a GreenCorrectionPDEAxioms package into the GreenCorrectionInput structure used by correctedFamily and the holomorphic-correction theorems.

noncomputable def donaldson_green_correction_pde_axioms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (_hcompat : IsCompatibleACS S J) (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [wb : HasWeitzenbockDecomp Ω l2 dol] [hpde : HasDonaldsonPDEData Ω wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) : GreenCorrectionPDEAxioms wdn l2 dol fam

Construct the Donaldson Green-correction PDE-axiom package on a compact Kähler manifold by combining the Weitzenböck decomposition with the Donaldson PDE-data infrastructure.

noncomputable def donaldson_green_correction_exists {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (_hK : IsKahler S J) (_hcompat : IsCompatibleACS S J) (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) [HasWeitzenbockDecomp Ω l2 dol] [HasDonaldsonPDEData Ω wdn l2 dol] (fam : ApproxHolomorphicSectionFamily) : GreenCorrectionInput wdn l2 dol fam

Existence of a GreenCorrectionInput on a compact Kähler manifold equipped with the Weitzenböck decomposition and Donaldson PDE data: obtained by composing donaldson_green_correction_pde_axioms with GreenCorrectionInput_of_pde_axioms.

structure NormalizedLocalSectionData {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type (max u_1 u_2)

Normalized local section data: a section family together with the pointwise-evaluation and manifold-distance structures, plus a starting index $k_0 \ge 1$ from which all estimates begin to hold.

• fam : ApproxHolomorphicSectionFamily
• pe : PointwiseEval Ω VF
• md : ManifoldDist VF
• k₀ : ℕ
• hk₀ : 1 ≤ self.k₀

theorem kahler_normal_coordinates_with_section {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) : ∃ (nls : NormalizedLocalSectionData), IsUniformlyConcentrated nls.fam ∧ IsUniformlyBounded nls.fam ∧ IsApproxHolomorphic nls.fam ∧ ∃ c > 0, ∀ (k : ℕ), nls.k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (nls.fam.section_ k p)

Existence of normalized local Kähler coordinates with attached approximately holomorphic peak sections, satisfying uniform concentration/boundedness, approximate holomorphicity, and a local lower bound on Gaussian peaks.

theorem compact_manifold_smooth_cutoff {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (nls : NormalizedLocalSectionData) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (nls.fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))

Smooth cutoff axiom on a compact manifold: after multiplying the peak sections by a suitable cutoff, $\bar\partial$ of the resulting sections has cube-root exponential decay $\|\bar\partial s_{k,p}\|_{L^2} \le C_g e^{-\lambda k^{1/3}}$.

theorem peak_section_gaussian_decay {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) : ∃ (nls : NormalizedLocalSectionData), IsUniformlyConcentrated nls.fam ∧ IsUniformlyBounded nls.fam ∧ IsApproxHolomorphic nls.fam ∧ ∃ c > 0, ∀ (k : ℕ), nls.k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (nls.fam.section_ k p)

Repackaging of kahler_normal_coordinates_with_section: there exists a normalized local section family that is uniformly concentrated, uniformly bounded, approximately holomorphic, and locally bounded below by Gaussian peaks.

theorem peak_section_delbar_estimate {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (nls : NormalizedLocalSectionData) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (nls.fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))

$\bar\partial$ estimate for the peak sections: the cube-root exponential decay bound on $\|\bar\partial s_{k,p}\|_{L^2}$, obtained from the smooth-cutoff axiom.

theorem peak_section_full_from_primitives {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) : ∃ (k₀ : ℕ) (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (fam : ApproxHolomorphicSectionFamily), 1 ≤ k₀ ∧ IsUniformlyConcentrated fam ∧ IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ (∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)) ∧ ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))

Combined existence statement: on a compact Kähler manifold there exist peak sections together with both the local lower-bound (Gaussian peak) and the $\bar\partial$ cube-root exponential decay bound.

theorem cauchy_estimates_holomorphic_sections {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) : (∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (HasGreenOperator.greenCorrection l2 dol k s) ≤ C_r * L2NormSpace.l2norm VF (dol.delbar s)) ∧ ∀ (s : Ω 0), dol.delbar (s + HasGreenOperator.greenCorrection l2 dol 0 s) = 0

Cauchy estimates for the Green-corrected sections on a compact Kähler manifold: weighted $C^r$ norms of the Green correction are bounded by the $L^2$-norm of $\bar\partial s$, and the corrected $k=0$ section is holomorphic.

theorem donaldson_delbar_correction_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (fam : ApproxHolomorphicSectionFamily) (lam : ℝ) (hlam : lam > 0) (C_delbar : ℝ) (hC_delbar : C_delbar > 0) (hdelbar_decay : ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_delbar * Real.exp (-lam * ↑k ^ (1 / 3))) : ∃ (fam' : ApproxHolomorphicSectionFamily), fam'.L = fam.L ∧ (∀ (k : ℕ) (p : VF), dol.delbar (fam'.section_ k p) = 0) ∧ ∀ (r : ℕ), ∃ C'_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p - fam'.section_ k p) ≤ C'_r * Real.exp (-lam * ↑k ^ (1 / 3))

Donaldson's $\bar\partial$-correction theorem: given a section family with cube-root exponential $\bar\partial$ decay, there exists an exponentially close genuinely holomorphic family on the same line bundle, with controlled weighted $C^r$ approximation rate.

theorem donaldson_proposition_1_with_hypotheses {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (h_normal_coords : ∃ (nls : NormalizedLocalSectionData), IsUniformlyConcentrated nls.fam ∧ IsUniformlyBounded nls.fam ∧ IsApproxHolomorphic nls.fam ∧ ∃ c > 0, ∀ (k : ℕ), nls.k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (nls.fam.section_ k p)) (h_cutoff : ∀ (nls : NormalizedLocalSectionData), ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (nls.fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) (h_curvature : (greenCorrection : ℕ → Ω 0 → Ω 0) ×' (C_geom : ℝ) ×' C_geom > 0 ∧ (∀ (k : ℕ) (s : Ω 0), ↑k > C_geom → L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ 1 / (↑k - C_geom) * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) ∧ ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), ∃ B > 0, L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ B * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) (h_hodge : ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), dol.delbar (s + h_curvature.fst k s) = 0) (h_cauchy : (∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (h_curvature.fst k s) ≤ C_r * L2NormSpace.l2norm VF (dol.delbar s)) ∧ ∀ (s : Ω 0), dol.delbar (s + h_curvature.fst 0 s) = 0) : ∃ (k₀ : ℕ) (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (fam : ApproxHolomorphicSectionFamily), 1 ≤ k₀ ∧ IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ (∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)) ∧ ∃ (fam' : ApproxHolomorphicSectionFamily), IsHolomorphicFamily dol fam' ∧ IsExponentiallyCloseCubeRoot wdn fam fam'

Donaldson's Proposition 1 with explicit hypotheses: given normalized coordinates, cutoff Gaussian decay, curvature lower bound, Hodge orthogonality and Cauchy estimates, there exists an exponentially-close holomorphic family approximating the peak sections at the cube-root rate.

theorem donaldson_proposition_1_book {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (hcompat : IsCompatibleACS S J) (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (dol : DolbeaultOps) (h_normal_coords : ∃ (nls : NormalizedLocalSectionData), IsUniformlyConcentrated nls.fam ∧ IsUniformlyBounded nls.fam ∧ IsApproxHolomorphic nls.fam ∧ ∃ c > 0, ∀ (k : ℕ), nls.k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (nls.fam.section_ k p)) (h_cutoff : ∀ (nls : NormalizedLocalSectionData), ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (nls.fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))) (h_curvature : (greenCorrection : ℕ → Ω 0 → Ω 0) ×' (C_geom : ℝ) ×' C_geom > 0 ∧ (∀ (k : ℕ) (s : Ω 0), ↑k > C_geom → L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ 1 / (↑k - C_geom) * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) ∧ ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), ∃ B > 0, L2NormSpace.l2norm VF (greenCorrection k s) * L2NormSpace.l2norm VF (greenCorrection k s) ≤ B * (L2NormSpace.l2norm VF (dol.delbar s) * L2NormSpace.l2norm VF (dol.delbar s))) (h_hodge : ∀ (k : ℕ), k ≠ 0 → ∀ (s : Ω 0), dol.delbar (s + h_curvature.fst k s) = 0) (h_cauchy : (∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (s : Ω 0), WeightedDerivSupNorm.weighted_supnorm VF k r (h_curvature.fst k s) ≤ C_r * L2NormSpace.l2norm VF (dol.delbar s)) ∧ ∀ (s : Ω 0), dol.delbar (s + h_curvature.fst 0 s) = 0) : ∃ (k₀ : ℕ) (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (fam : ApproxHolomorphicSectionFamily), 1 ≤ k₀ ∧ IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ (∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)) ∧ ∃ (fam' : ApproxHolomorphicSectionFamily), IsHolomorphicFamily dol fam' ∧ IsExponentiallyCloseCubeRoot wdn fam fam'

Donaldson's Proposition 1 (book statement): on a compact Kähler manifold $(M, \omega, J)$ with normalized coordinates, the line bundles $L^k$ admit approximately holomorphic Gaussian peak sections and, for $k$ sufficiently large, there is a genuinely holomorphic family exponentially close (at the cube-root rate) to the peak sections.

theorem cutoff_delbar_linear_decay {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (l2 : L2NormSpace Ω) (fam : ApproxHolomorphicSectionFamily) (dol : DolbeaultOps) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : VF), L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k / 3)

Linear-decay variant of the cutoff $\bar\partial$ bound: $\|\bar\partial s_{k,p}\|_{L^2} \le C_g\, e^{-\lambda k / 3}$.

theorem green_correction_weighted_bound {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (fam : ApproxHolomorphicSectionFamily) (dol : DolbeaultOps) : ∃ (fam' : ApproxHolomorphicSectionFamily), fam.L = fam'.L ∧ (∀ (k : ℕ) (p : VF), dol.delbar (fam'.section_ k p) = 0) ∧ ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : VF), WeightedDerivSupNorm.weighted_supnorm VF k r (fam.section_ k p - fam'.section_ k p) ≤ C_r * L2NormSpace.l2norm VF (dol.delbar (fam.section_ k p))

Weighted-norm Green correction theorem: for any section family on a compact Kähler manifold, the Green correction yields a holomorphic family $\text{fam}'$ on the same line bundle with weighted $C^r$ differences controlled by the $L^2$-norm of $\bar\partial s_{k,p}$.

theorem donaldson_holomorphic_approximation_linear {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsCompactSymplectic Ω VF] [HasLieBracket Ω VF] (wdn : WeightedDerivSupNorm Ω) (l2 : L2NormSpace Ω) (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) (hK : IsKahler S J) (fam : ApproxHolomorphicSectionFamily) (hUB : IsQuantUniformlyBounded wdn fam) (hAH : IsQuantApproxHolomorphic wdn l2 fam) (hUC : IsQuantUniformlyConcentrated wdn fam) (hLB : HasLocalLowerBound wdn fam) (dol : DolbeaultOps) : ∃ (fam' : ApproxHolomorphicSectionFamily), IsHolomorphicFamily dol fam' ∧ IsExponentiallyClose wdn fam fam'

Donaldson holomorphic approximation theorem (linear decay version): an approximately holomorphic, uniformly bounded/concentrated section family with a local lower bound admits an exponentially-close (rate $e^{-\lambda k / 3}$) genuinely holomorphic family.

class HasSymplecticHypersurface {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Prop

A symplectic manifold admits a "symplectic hypersurface" in the sense of Donaldson's construction: there exist Dolbeault operators, weighted norms, and a family of holomorphic peak sections with uniform Gaussian concentration together with an exponentially-close holomorphic family approximating them. The zero sets of these holomorphic sections give the desired symplectic submanifolds.

• has_holomorphic_peak_sections : ∃ (dol : DolbeaultOps) (wdn : WeightedDerivSupNorm Ω) (k₀ : ℕ) (pe : PointwiseEval Ω VF) (md : ManifoldDist VF) (fam : ApproxHolomorphicSectionFamily), 1 ≤ k₀ ∧ IsUniformlyBounded fam ∧ IsApproxHolomorphic fam ∧ IsUniformlyConcentrated fam ∧ (∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : VF), ManifoldDist.mdist p q ≤ 1 / √↑k → c ≤ PointwiseEval.peval q (fam.section_ k p)) ∧ ∃ (fam' : ApproxHolomorphicSectionFamily), IsHolomorphicFamily dol fam' ∧ IsExponentiallyCloseCubeRoot wdn fam fam'