structure Donaldson.CompactKahlerData : Type (u_1 + 1)

Data for a compact Kähler manifold: a metric space $M$, complex dimension $n$, a non-degenerate antisymmetric 2-form $\omega$, an almost complex structure $J$ with $J^2 = -I$, the Kähler metric $g(v,w) = \omega(v, J w)$, and an integrality condition on the symplectic volume (needed for Donaldson's pre-quantization).

• M : Type u_1
• metricInst : MetricSpace self.M
• compactInst : CompactSpace self.M
• complexDim : ℕ
• dim_pos : 0 < self.complexDim
• ω : self.M → (Fin (2 * self.complexDim) → ℝ) → (Fin (2 * self.complexDim) → ℝ) → ℝ
• ω_antisymm (p : self.M) (v w : Fin (2 * self.complexDim) → ℝ) : self.ω p v w = -self.ω p w v
• J : self.M → (Fin (2 * self.complexDim) → ℝ) → Fin (2 * self.complexDim) → ℝ
• J_sq_neg (p : self.M) (v : Fin (2 * self.complexDim) → ℝ) : self.J p (self.J p v) = fun (i : Fin (2 * self.complexDim)) => -v i
• g : self.M → (Fin (2 * self.complexDim) → ℝ) → (Fin (2 * self.complexDim) → ℝ) → ℝ
• kahler_compat (p : self.M) (v w : Fin (2 * self.complexDim) → ℝ) : 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) ^ self.complexDim * ↑N

structure Donaldson.SectionFamily (X : CompactKahlerData) : Type u_1

A family $\{\sigma_{k,p}\}$ of sections indexed by an integer $k$ and a basepoint $p \in M$.

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

structure Donaldson.WeightedSupNorm (X : CompactKahlerData) : Type u_1

Abstraction of the $k$-weighted $C^r$ sup-norm $\sup_x (k^{r/2}|\nabla^r s(x)|)$, with the basic properties (non-negativity, neg-invariance, and pointwise control for $r=0$).

• eval : ℕ → ℕ → (X.M → ℂ) → ℝ
• nonneg (k r : ℕ) (s : X.M → ℂ) : 0 ≤ self.eval k r s
• neg_le (k r : ℕ) (s : X.M → ℂ) : (self.eval k r fun (x : X.M) => -s x) ≤ self.eval k r s
• pointwise_control (k : ℕ) (s : X.M → ℂ) (B : ℝ) : 0 ≤ B → (∀ (x : X.M), ‖s x‖ ≤ B) → self.eval k 0 s ≤ B

structure Donaldson.L2Norm (X : CompactKahlerData) : Type u_1

Abstraction of an $L^2$ norm on sections, with the basic property of non-negativity.

• norm : (X.M → ℂ) → ℝ
• nonneg (s : X.M → ℂ) : 0 ≤ self.norm s

structure Donaldson.DelbarOp (X : CompactKahlerData) : Type u_1

Abstraction of the Dolbeault operator $\bar\partial$ on sections of $L^k$, together with the pointwise estimate that $|\bar\partial$ applied to the Gaussian peak section$|\leq C/\sqrt k$.

• delbar : (X.M → ℂ) → X.M → ℂ
• delbar_gaussian_pointwise_bound : ∃ C > 0, ∀ (k : ℕ) (p x : X.M), ‖self.delbar (fun (q : X.M) => ↑(Real.exp (-↑k * dist p q ^ 2 / 4))) x‖ ≤ C / √↑k

def Donaldson.IsUniformlyBounded {X : CompactKahlerData} (wdn : WeightedSupNorm X) (fam : SectionFamily X) : Prop

The family $\{\sigma_{k,p}\}$ is uniformly $C^r$-bounded for every $r$.

def Donaldson.IsApproxHolomorphic {X : CompactKahlerData} (wdn : WeightedSupNorm X) (dol : DelbarOp X) (fam : SectionFamily X) : Prop

The family is approximately holomorphic: $\|\bar\partial \sigma_{k,p}\|_{C^r} \leq C_r/\sqrt{k}$.

def Donaldson.IsUniformlyConcentrated {X : CompactKahlerData} (fam : SectionFamily X) : Prop

The family is uniformly Gaussian-concentrated around $p$: $|\sigma_{k,p}(x)| \leq C \exp(-\lambda k\, d(p,x)^2)$.

def Donaldson.IsHolomorphicFamily {X : CompactKahlerData} (dol : DelbarOp X) (fam : SectionFamily X) : Prop

A family is truly holomorphic if $\bar\partial \sigma_{k,p} = 0$ for all $k, p$.

def Donaldson.IsExponentiallyClose {X : CompactKahlerData} (wdn : WeightedSupNorm X) (fam fam' : SectionFamily X) : Prop

Two families are exponentially close in every $C^r$-norm: $\|\sigma_{k,p} - \tilde\sigma_{k,p}\|_{C^r} \leq C_r \exp(-\lambda k^{1/3})$.

noncomputable def Donaldson.gaussianPeakSection (X : CompactKahlerData) : SectionFamily X

The Gaussian peak section family $\sigma_{k,p}(q) = e^{-k\, d(p,q)^2/4}$ used as a model for Donaldson's near-holomorphic peak sections.

theorem Donaldson.gaussian_pointwise_le_one (X : CompactKahlerData) (k : ℕ) (p x : X.M) : ‖(gaussianPeakSection X).section_ k p x‖ ≤ 1

The Gaussian peak section is pointwise bounded by 1 since $e^{-k d^2/4} \leq 1$.

theorem Donaldson.gaussian_peak_concentrated (X : CompactKahlerData) : IsUniformlyConcentrated (gaussianPeakSection X)

The Gaussian peak section is uniformly concentrated with constants $C = 1$, $\lambda = 1/4$.

theorem Donaldson.gaussian_peak_lower_bound (X : CompactKahlerData) : ∃ c > 0, ∀ (k : ℕ), 1 < k → ∀ (p q : X.M), dist p q ≤ 1 / √↑k → c ≤ ‖(gaussianPeakSection X).section_ k p q‖

Lower bound on the Gaussian peak section within a $1/\sqrt{k}$-ball: $|\sigma_{k,p}(q)| \geq e^{-1/4}$ when $d(p,q) \leq 1/\sqrt{k}$.

theorem Donaldson.gaussian_peak_higher_derivatives_bounded (X : CompactKahlerData) (wdn : WeightedSupNorm X) (r : ℕ) : 0 < r → ∃ C_r > 0, ∀ (k : ℕ) (p : X.M), wdn.eval k r ((gaussianPeakSection X).section_ k p) ≤ C_r

Higher derivatives of the Gaussian peak section are uniformly bounded in the weighted norm.

theorem Donaldson.delbar_gaussian_higher_derivatives_bounded (X : CompactKahlerData) (wdn : WeightedSupNorm X) (dol : DelbarOp X) (r : ℕ) : 0 < r → ∃ C_r > 0, ∀ (k : ℕ) (p : X.M), wdn.eval k r (dol.delbar ((gaussianPeakSection X).section_ k p)) ≤ C_r / √↑k

Higher derivatives of $\bar\partial$ applied to the Gaussian peak section decay like $1/\sqrt{k}$ in the weighted norm.

theorem Donaldson.gaussian_peak_bounded (X : CompactKahlerData) (wdn : WeightedSupNorm X) : IsUniformlyBounded wdn (gaussianPeakSection X)

The Gaussian peak section family is uniformly $C^r$-bounded for all $r$.

theorem Donaldson.gaussian_peak_approx_holo (X : CompactKahlerData) (wdn : WeightedSupNorm X) (dol : DelbarOp X) : IsApproxHolomorphic wdn dol (gaussianPeakSection X)

The Gaussian peak section family is approximately holomorphic: $\bar\partial$ decays as $1/\sqrt k$.

theorem Donaldson.peak_section_construction (X : CompactKahlerData) (wdn : WeightedSupNorm X) (dol : DelbarOp X) : ∃ (fam : SectionFamily X) (k₀ : ℕ), 1 ≤ k₀ ∧ IsUniformlyBounded wdn fam ∧ IsApproxHolomorphic wdn dol fam ∧ IsUniformlyConcentrated fam ∧ ∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : X.M), dist p q ≤ 1 / √↑k → c ≤ ‖fam.section_ k p q‖

Construction of peak sections (Step 1 of Donaldson's proof): there exists a family of sections that is uniformly bounded, approximately holomorphic, uniformly concentrated, and bounded below on $1/\sqrt{k}$-balls.

theorem Donaldson.cutoff_delbar_decay (X : CompactKahlerData) (l2 : L2Norm X) (dol : DelbarOp X) (fam : SectionFamily X) : ∃ (C_g : ℝ) (lam : ℝ), C_g > 0 ∧ lam > 0 ∧ ∀ (k : ℕ) (p : X.M), l2.norm (dol.delbar (fam.section_ k p)) ≤ C_g * Real.exp (-lam * ↑k ^ (1 / 3))

Sub-exponential decay of $\bar\partial$ of a cutoff section in $L^2$: $\|\bar\partial \sigma_{k,p}\|_{L^2} \leq C_g \exp(-\lambda k^{1/3})$.

theorem Donaldson.green_correction_exists (X : CompactKahlerData) (l2 : L2Norm X) (dol : DelbarOp X) : ∃ (greenCorr : ℕ → (X.M → ℂ) → X.M → ℂ), (∀ (k : ℕ), k ≠ 0 → ∀ (s : X.M → ℂ), (dol.delbar fun (x : X.M) => s x + greenCorr k s x) = 0) ∧ (∀ (s : X.M → ℂ), (dol.delbar fun (x : X.M) => s x + greenCorr 0 s x) = 0) ∧ ∃ c_G > 0, ∀ (k : ℕ), k ≠ 0 → ∀ (s : X.M → ℂ), l2.norm (greenCorr k s) ≤ c_G / √↑k * l2.norm (dol.delbar s)

Existence of a Green's operator correction: for each $k$ and each section $s$, there is a correction whose $L^2$ norm is bounded by $c_G/\sqrt{k}$ times $\|\bar\partial s\|_{L^2}$, and which makes $s + \mathrm{corr}(s)$ truly holomorphic.

theorem Donaldson.cauchy_l2_to_cr_estimates (X : CompactKahlerData) (wdn : WeightedSupNorm X) (l2 : L2Norm X) (dol : DelbarOp X) (greenCorr : ℕ → (X.M → ℂ) → X.M → ℂ) (r : ℕ) : ∃ C_r > 0, ∀ (k : ℕ) (s : X.M → ℂ), wdn.eval k r (greenCorr k s) ≤ C_r * l2.norm (dol.delbar s)

Elliptic Cauchy estimates: the $C^r$-norm of the Green correction is controlled by the $L^2$-norm of $\bar\partial s$.

theorem Donaldson.donaldson_proposition_1_book (X : CompactKahlerData) (wdn : WeightedSupNorm X) (l2 : L2Norm X) (dol : DelbarOp X) : ∃ (fam : SectionFamily X) (k₀ : ℕ), 1 ≤ k₀ ∧ IsUniformlyBounded wdn fam ∧ IsApproxHolomorphic wdn dol fam ∧ IsUniformlyConcentrated fam ∧ (∃ c > 0, ∀ (k : ℕ), k₀ < k → ∀ (p q : X.M), dist p q ≤ 1 / √↑k → c ≤ ‖fam.section_ k p q‖) ∧ ∃ (fam' : SectionFamily X), IsHolomorphicFamily dol fam' ∧ IsExponentiallyClose wdn fam fam'

Donaldson's Proposition 1 on approximately holomorphic sections: there exists a peak section family $\{\sigma_{k,p}\}$ and a truly holomorphic family $\{\tilde\sigma_{k,p}\}$ with $\sup |\sigma_{k,p} - \tilde\sigma_{k,p}|_{C^r} \leq O(\exp(-\lambda k^{1/3}))$.