structure CompactKahlerData (n : ℕ) : Type (u_1 + 1)

Data of a compact Kähler manifold of complex dimension $n$: an underlying metric/charted space $M$ with symplectic form $\omega$, almost complex structure $J$ satisfying $J^2 = -\mathrm{id}$, compatible Riemannian metric $g(v,w) = \omega(v, Jw)$, and a symplectic volume satisfying the integrality condition $\mathrm{vol} = (2\pi)^n N$ for some $N \in \mathbb{N}_{>0}$.

• M : Type u_1
• topM : TopologicalSpace self.M
• metricM : MetricSpace self.M
• compactM : CompactSpace self.M
• nonemptyM : Nonempty self.M
• chartedM : ChartedSpace (EuclideanSpace ℝ (Fin (2 * n))) self.M
• ω : self.M → (Fin (2 * n) → ℝ) → (Fin (2 * n) → ℝ) → ℝ
• ω_antisymm (p : self.M) (v w : Fin (2 * n) → ℝ) : self.ω p v w = -self.ω p w v
• J : self.M → (Fin (2 * n) → ℝ) → Fin (2 * n) → ℝ
• J_sq_neg (p : self.M) (v : Fin (2 * n) → ℝ) : self.J p (self.J p v) = fun (i : Fin (2 * n)) => -v i
• g : self.M → (Fin (2 * n) → ℝ) → (Fin (2 * n) → ℝ) → ℝ
• kahler_compat (p : self.M) (v w : Fin (2 * n) → ℝ) : self.g p v w = self.ω p v (self.J p w)
• symplectic_volume : ℝ
• symplectic_volume_pos : 0 < self.symplectic_volume
• integrality_condition : ∃ (N : ℕ), 0 < N ∧ self.symplectic_volume = (2 * Real.pi) ^ n * ↑N

structure SectionFamily {n : ℕ} (D : CompactKahlerData n) : Type u_1

A family of complex-valued sections $\sigma_{k,p}(q)$ indexed by $k \in \mathbb{N}$ and base points $p \in M$, evaluated at $q \in M$.

• section_ : ℕ → D.M → D.M → ℂ

structure WeightedCrNorm {n : ℕ} (D : CompactKahlerData n) : Type u_1

A family of weighted $C^r$ norms $\|\cdot\|_{C^r_k}$ on complex-valued functions on $M$, scaled according to the parameter $k$ controlling the local length scale $k^{-1/2}$.

• wnorm : ℕ → ℕ → (D.M → ℂ) → ℝ
• wnorm_nonneg (k r : ℕ) (f : D.M → ℂ) : 0 ≤ self.wnorm k r f

structure L2Norm {n : ℕ} (D : CompactKahlerData n) : Type u_1

An $L^2$ norm $\|\cdot\|_{L^2}$ on complex-valued functions on $M$.

• l2 : (D.M → ℂ) → ℝ
• l2_nonneg (f : D.M → ℂ) : 0 ≤ self.l2 f

structure DelbarOp {n : ℕ} (D : CompactKahlerData n) : Type u_1

The Dolbeault operator $\bar\partial$ acting on complex-valued functions on $M$.

• delbar : (D.M → ℂ) → D.M → ℂ

theorem donaldson_holomorphic_approximation_exp_bound {n : ℕ} (D : CompactKahlerData n) (wcr : WeightedCrNorm D) (l2 : L2Norm D) (dol : DelbarOp D) (fam : SectionFamily D) (h_delbar_decay : ∃ (C_delbar : ℝ) (lam_delbar : ℝ), C_delbar > 0 ∧ lam_delbar > 0 ∧ ∀ (k : ℕ) (p : D.M), l2.l2 (dol.delbar (fam.section_ k p)) ≤ C_delbar * Real.exp (-lam_delbar * ↑k / 3)) (h_green : ∃ (fam' : SectionFamily D), (∀ (k : ℕ) (p : D.M), dol.delbar (fam'.section_ k p) = 0) ∧ ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : D.M), (wcr.wnorm k r fun (q : D.M) => fam.section_ k p q - fam'.section_ k p q) ≤ C_r * l2.l2 (dol.delbar (fam.section_ k p))) : ∃ (fam' : SectionFamily D), (∀ (k : ℕ) (p : D.M), dol.delbar (fam'.section_ k p) = 0) ∧ ∃ lam > 0, ∀ (r : ℕ), ∃ C_r > 0, ∀ (k : ℕ) (p : D.M), (wcr.wnorm k r fun (q : D.M) => fam.section_ k p q - fam'.section_ k p q) ≤ C_r * Real.exp (-lam * ↑k / 3)

Donaldson's holomorphic approximation theorem (exponential bound version). Given a family of almost-holomorphic sections $\sigma_{k,p}$ with $\|\bar\partial \sigma_{k,p}\|_{L^2} \leq C_{\bar\partial} \exp(-\lambda_{\bar\partial} k / 3)$ and a Green's-function correction producing holomorphic sections $\tilde\sigma_{k,p}$ with $\|\sigma_{k,p} - \tilde\sigma_{k,p}\|_{C^r_k} \lesssim \|\bar\partial \sigma_{k,p}\|_{L^2}$, the difference itself decays exponentially: $\sup_q |\sigma_{k,p}(q) - \tilde\sigma_{k,p}(q)| \leq O(\exp(-\lambda k^{1/3}))$.