Exhaustion.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth and conditional exhaustion

The model is the complex vector space Fin n → ℂ. A Kähler metric is specified by a smooth real Riemannian metric and its torsion-free metric connection, with the canonical complex structure parallel. Completeness refers to the Riemannian length distance.

Polynomial radial growth, forward smallness and an inverse-ball inclusion force an open image containing zero to fill complex space. Constructing the maps and deriving these bounds from a Kähler metric remain outside this formalization; the Kähler uniformization theorem is not proved here.

abbrev OAI.KahlerUniformization.ComplexSpace line 25
Source documentation
Complex Euclidean space of complex dimension n.
```
abbrev ComplexSpace (n : ℕ) := Fin n → ℂ
```
abbrev OAI.KahlerUniformization.complexModel line 26
abbrev OAI.KahlerUniformization.realModel line 27
instance OAI.KahlerUniformization.underlyingRealManifold line 30
Source documentation
Holomorphic transition functions are smooth over the real numbers.
```
instance underlyingRealManifold {n : ℕ} {M : Type*}
    [TopologicalSpace M] [ChartedSpace (ComplexSpace n) M]
    [IsManifold (complexModel n) ∞ M] :
    IsManifold (realModel n) ∞ M := by
…
```
Mentions: OAI.KahlerUniformization.ComplexSpace, OAI.KahlerUniformization.complexModel, OAI.KahlerUniformization.realModel
abbrev OAI.KahlerUniformization.RealTangent line 50
def OAI.KahlerUniformization.complexStructure line 54
Source documentation
The canonical almost complex structure on the underlying real tangent bundle: multiplication by i in holomorphic tangent coordinates.
```
def complexStructure (x : M) (v : RealTangent (n := n) x) : RealTangent (n := n) x :=
…
```
Mentions: OAI.KahlerUniformization.RealTangent
lemma OAI.KahlerUniformization.complexStructure_sq line 58
abbrev OAI.KahlerUniformization.SmoothMetric line 65
Source documentation
A positive definite smooth real inner product on each tangent space.
```
abbrev SmoothMetric := Bundle.ContMDiffRiemannianMetric (realModel n) ∞
…
```
Mentions: OAI.KahlerUniformization.realModel
abbrev OAI.KahlerUniformization.Connection line 68
structure OAI.KahlerUniformization.SmoothKahlerMetric line 74
Source documentation
A smooth Kähler metric, in the torsion-free metric-connection formulation. No topology, flow, coordinate-map, or uniformization conclusions occur among these fields.
```
structure SmoothKahlerMetric where
…
```
def OAI.KahlerUniformization.SmoothKahlerMetric.curvature line 105
Source documentation
The curvature operator R(u,v)w = ∇_U ∇_V W - ∇_V ∇_U W - ∇_[U,V] W, using local smooth extensions at x. This is the convention where g(R(u,v)v,u) is the sectional-curvature numerator.
```
def curvature (x : M) (u v w : RealTangent (n := n) x) : RealTangent (n := n) x :=
…
```
Mentions: OAI.KahlerUniformization.RealTangent
def OAI.KahlerUniformization.SmoothKahlerMetric.rm line 114
Source documentation
The real Riemannian curvature with all indices lowered using g.
```
def rm (x : M) (u v w z : RealTangent (n := n) x) : ℝ :=
…
```
Mentions: OAI.KahlerUniformization.RealTangent
def OAI.KahlerUniformization.SmoothKahlerMetric.PositiveHolomorphicBisectionalCurvature line 119
Source documentation
Pointwise strict positivity, for every pair of real metric-unit vectors. There is no uniform lower bound or upper curvature bound in this definition.
```
def PositiveHolomorphicBisectionalCurvature : Prop :=
…
```
def OAI.KahlerUniformization.SmoothKahlerMetric.IsComplete line 126
Source documentation
Completeness of the Riemannian length distance, not that of a chart norm.
```
def IsComplete [T2Space M] : Prop :=
…
```
lemma OAI.KahlerUniformization.SmoothKahlerMetric.inner_complexStructure_swap line 135
Source documentation
The fundamental form of a Hermitian metric is skew-symmetric.
```
lemma inner_complexStructure_swap (x : M) (u v : RealTangent (n := n) x) :
…
```
Mentions: OAI.KahlerUniformization.RealTangent
lemma OAI.KahlerUniformization.SmoothKahlerMetric.curvature_self line 142
lemma OAI.KahlerUniformization.SmoothKahlerMetric.rm_self line 146
lemma OAI.KahlerUniformization.SmoothKahlerMetric.holomorphicSectional_pos line 152
Source documentation
Strict bisectional positivity in particular implies positive holomorphic sectional curvature with the chosen curvature sign convention.
```
lemma holomorphicSectional_pos
    (h : g.PositiveHolomorphicBisectionalCurvature)
    (x : M) (u : RealTangent (n := n) x) (hu : g.metric.inner x u u = 1) :
…
```
Mentions: OAI.KahlerUniformization.RealTangent

theorem OAI.KahlerUniformization.polynomial_norm_bound_exterior line 167

Source documentation

Exterior maximum-modulus bound for a complex polynomial.

theorem polynomial_norm_bound_exterior (p : ℂ[X]) (m : ℕ) (hm : p.natDegree ≤ m)
    (C : ℝ) (hC : ∀ z : ℂ, ‖z‖ ≤ 1 → ‖p.eval z‖ ≤ C)
    (z : ℂ) (hz : 1 ≤ ‖z‖) :
    ‖p.eval z‖ ≤ ‖z‖ ^ m * C := by
…

def OAI.KahlerUniformization.polynomialOnLine line 200
Source documentation
Restriction of a multivariable polynomial to a complex line through zero.
```
def polynomialOnLine {ι : Type*} (p : MvPolynomial ι ℂ) (v : ι → ℂ) : ℂ[X] :=
…
```
lemma OAI.KahlerUniformization.polynomialOnLine_eval line 203
lemma OAI.KahlerUniformization.polynomialOnLine_natDegree_le line 217

theorem OAI.KahlerUniformization.mvPolynomial_radial_growth line 237

Source documentation

Radial growth bound for a multivariable complex polynomial.

theorem mvPolynomial_radial_growth {ι : Type*} [Fintype ι]
    (p : MvPolynomial ι ℂ) (m : ℕ) (hm : p.totalDegree ≤ m)
    {r R C : ℝ} (hr : 0 < r) (hrR : r ≤ R)
    (hC : ∀ z : ι → ℂ, ‖z‖ ≤ r → ‖MvPolynomial.eval z p‖ ≤ C)
    (z : ι → ℂ) (hz : ‖z‖ ≤ R) :
    ‖MvPolynomial.eval z p‖ ≤ (R / r) ^ m * C := by
…

theorem OAI.KahlerUniformization.polynomial_map_radial_growth line 273

Source documentation

The polynomial growth estimate for vector-valued multivariable polynomials. Here the finite-dimensional norm is the standard supremum norm on coordinate tuples.

theorem polynomial_map_radial_growth {ι κ : Type*} [Fintype ι] [Fintype κ]
    (P : κ → MvPolynomial ι ℂ) (m : ℕ) (hm : ∀ i, (P i).totalDegree ≤ m)
    {r R C : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hC : 0 ≤ C)
    (hbound : ∀ z : ι → ℂ, ‖z‖ ≤ r → ‖fun i ↦ MvPolynomial.eval z (P i)‖ ≤ C)
    (z : ι → ℂ) (hz : ‖z‖ ≤ R) :
    ‖fun i ↦ MvPolynomial.eval z (P i)‖ ≤ (R / r) ^ m * C := by
…

theorem OAI.KahlerUniformization.image_eq_univ_of_exponential_bounds line 294

Source documentation

The image-exhaustion step: exponentially small forward maps, an inverse-ball inclusion, and radial growth bounds along an unbounded subsequence force an open image containing the origin to be the whole space. The hypotheses on G are analytic inputs, not consequences of curvature proved in this file.

theorem image_eq_univ_of_exponential_bounds
    {E : Type*} [NormedAddCommGroup E]
    {Ω : Set E} (hΩ : IsOpen Ω) (hzero : (0 : E) ∈ Ω)
    (a b D : ℝ) (hD : 0 ≤ D) (hab : b < a)
    (s : ℕ → ℝ) (hs : Tendsto s atTop atTop) (G : ℕ → E → E)
    (forward : ∀ r : ℝ, 0 < r → (∀ z : E, ‖z‖ ≤ r → z ∈ Ω) →
      ∀ᶠ k in atTop, ∀ z : E, ‖z‖ ≤ r → ‖G k z‖ ≤ Real.exp (-a * s k))
    (growth : ∃ᶠ k in atTop, ∀ (r R C : ℝ), 0 < r → r ≤ R → 0 ≤ C →
      (∀ z : E, ‖z‖ ≤ r → ‖G k z‖ ≤ C) →
      ∀ z : E, ‖z‖ ≤ R →
        ‖G k z‖ ≤ Real.exp (D * s k * Real.log (R / r)) * C)
    (inverse_ball : ∀ᶠ k in atTop, ∀ z : E,
…

def OAI.KahlerUniformization.evalPolynomialMap line 360

Source documentation

Evaluation of a vector polynomial on complex affine space.

def evalPolynomialMap {n : ℕ} (P : Fin n → MvPolynomial (Fin n) ℂ)
    (z : Fin n → ℂ) : Fin n → ℂ := fun i ↦ MvPolynomial.eval z (P i)

theorem OAI.KahlerUniformization.image_eq_univ_of_polynomial_bounds line 368

Source documentation

The surjectivity endgame with actual polynomial maps rather than an assumed growth estimate. The forward degree bound is required only along an unbounded subsequence, expressed by Filter.Frequently. In particular no degree bound for inverse maps is required. Construction of these maps and estimates from a Kähler metric is not part of this lemma.

theorem image_eq_univ_of_polynomial_bounds
    {n : ℕ} {Ω : Set (Fin n → ℂ)} (hΩ : IsOpen Ω) (hzero : (0 : Fin n → ℂ) ∈ Ω)
    (a b D : ℝ) (hD : 0 ≤ D) (hab : b < a)
    (s : ℕ → ℝ) (hs : Tendsto s atTop atTop)
    (P : ℕ → Fin n → MvPolynomial (Fin n) ℂ)
    (m : ℕ → ℕ) (hdegree : ∀ k i, (P k i).totalDegree ≤ m k)
    (hcost : ∃ᶠ k in atTop, (m k : ℝ) ≤ D * s k)
    (forward : ∀ r : ℝ, 0 < r → (∀ z : Fin n → ℂ, ‖z‖ ≤ r → z ∈ Ω) →
      ∀ᶠ k in atTop, ∀ z : Fin n → ℂ, ‖z‖ ≤ r →
        ‖evalPolynomialMap (P k) z‖ ≤ Real.exp (-a * s k))
    (inverse_ball : ∀ᶠ k in atTop, ∀ z : Fin n → ℂ,
      ‖evalPolynomialMap (P k) z‖ < Real.exp (-b * s k) → z ∈ Ω) :
…

Mentions: OAI.KahlerUniformization.evalPolynomialMap