SectionOrder.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Local, orbit, and marked order of normal polynomial sections

def OAI.Nagata.CoefficientSpaces.logarithmicPoints line 16
Source documentation
Actual covering lifts of the moving logarithmic centers, on fibre value one.
```
noncomputable def logarithmicPoints {q : ℕ} (z₀ : ℂ) (ξ : Fin q → ℂ) : Fin q → ℂ × ℂ :=
…
```
theorem OAI.Nagata.CoefficientSpaces.localScalar_order_of_cover_order line 21
Source documentation
The actual exponential coordinate expression inherits genuine Taylor order by analytic substitution in both base and fibre coordinates.
```
theorem localScalar_order_of_cover_order {τ γL γP : ℂ} {d : ℤ} {m : ℕ} {P : ℂ → ℂ}
    (F : Nagata.W20.ActualSection τ γL γP d m P) (z₀ ξ : ℂ)
    (horder : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
Mentions: OAI.Nagata.W20.ActualSection
def OAI.Nagata.CoefficientSpaces.ambientNormalScalar line 49
Source documentation
Actual evaluation of an ambient normal polynomial on the chosen cubic coordinate functions and the normal fibre coordinate.
```
noncomputable def ambientNormalScalar {σ : Type*} (X : σ → ℂ → ℂ)
    (F : Polynomial (MvPolynomial σ ℂ)) (y : ℂ × ℂ) : ℂ :=
…
```
theorem OAI.Nagata.CoefficientSpaces.restrictedNormalPolynomial_order_iff line 55
Source documentation
Coefficientwise global restriction preserves precisely the genuine local Taylor order at every point of the punctured covering surface.
```
theorem restrictedNormalPolynomial_order_iff {σ : Type*} (X : σ → ℂ → ℂ)
    (F : Polynomial (MvPolynomial σ ℂ)) (x : ℂ × ℂ) (hx : x.1 ≠ 0) (m : ℕ) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```

theorem OAI.Nagata.CoefficientSpaces.automorphic_order_period line 76

Source documentation

Ordinary analytic order is invariant under the actual period multiplier.

theorem automorphic_order_period {τ γ : ℂ} {n : ℤ}
    (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (f : Nagata.W08.automorphicSections τ n γ) {z : ℂ} (hz : z ≠ 0) :
    analyticOrderAt f.val (τ * z) = analyticOrderAt f.val z := by
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.automorphic_order_orbit line 98

Source documentation

The same order holds at every representative of a marked period orbit.

theorem automorphic_order_orbit {τ γ : ℂ} {n : ℤ}
    (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (f : Nagata.W08.automorphicSections τ n γ) {a : ℂ} (ha : a ≠ 0) (k : ℤ) :
    analyticOrderAt f.val (a * τ ^ k) = analyticOrderAt f.val a := by
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.finite_product_finite_order line 126

Source documentation

A finite product of actual analytic functions of finite order has finite order. Repeated zeros are allowed; no disjointness assumption is required.

theorem finite_product_finite_order {ι : Type*} (S : Finset ι) (f : ι → ℂ → ℂ) (z : ℂ)
    (ha : ∀ i ∈ S, AnalyticAt ℂ (f i) z)
    (hf : ∀ i ∈ S, analyticOrderAt (f i) z ≠ ⊤) :
    AnalyticAt ℂ (fun w => ∏ i ∈ S, f i w) z ∧
      analyticOrderAt (fun w => ∏ i ∈ S, f i w) z ≠ ⊤ := by
…

theorem OAI.Nagata.CoefficientSpaces.shiftedTheta_finite_order line 151

Source documentation

All actual shifted theta factors have finite order at every point of C*.

theorem shiftedTheta_finite_order {τ a z : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0)
    (ha : a ≠ 0) (hz : z ≠ 0) :
    AnalyticAt ℂ (fun w => thetaProduct τ (w / a)) z ∧
      analyticOrderAt (fun w => thetaProduct τ (w / a)) z ≠ ⊤ := by
…

theorem OAI.Nagata.CoefficientSpaces.markedThetaSection_finite_order line 168

Source documentation

Actual marked theta sections have finite order even with repeated marked orbits; the finite-product proof supplies the required noncancellation.

theorem markedThetaSection_finite_order {ι : Type*} [Fintype ι]
    {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (a : ι → ℂ) (ha : ∀ i, a i ≠ 0)
    {z : ℂ} (hz : z ≠ 0) :
    analyticOrderAt (Nagata.W08.markedThetaSection hτ hτ0 a ha).val z ≠ ⊤ := by
…

Mentions: OAI.Nagata.W08.markedThetaSection

theorem OAI.Nagata.CoefficientSpaces.rayMarkedSection_analyticOnNhd line 179

Source documentation

Analyticity input for the genuine polynomial-basis multiplication map.

theorem rayMarkedSection_analyticOnNhd {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (ξ : Fin 9 → ℝ) :
    AnalyticOnNhd ℂ (Nagata.W22.rayMarkedSection hτ hτone ξ).val {z : ℂ | z ≠ 0} :=
…

Mentions: OAI.Nagata.W22.rayMarkedSection

theorem OAI.Nagata.CoefficientSpaces.rayMarkedSection_finite_order line 185

Source documentation

Finite-order input for injectivity of the genuine Pi-power map.

theorem rayMarkedSection_finite_order {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (ξ : Fin 9 → ℝ) {z : ℂ} (hz : z ≠ 0) :
    analyticOrderAt (Nagata.W22.rayMarkedSection hτ hτone ξ).val z ≠ ⊤ :=
…

Mentions: OAI.Nagata.W22.rayMarkedSection

theorem OAI.Nagata.CoefficientSpaces.rayMarkedMultiplier line 201
Source documentation
The exact multiplier of the actual nine-factor section is the fixed source scalar, retaining the odd sign and the sum of marked exponents.
```
theorem rayMarkedMultiplier {τ : ℝ} (hτ : 0 < τ) (ξ : Fin 9 → ℝ) :
    (∏ i, -((τ ^ ξ i : ℝ) : ℂ)) =
      -Nagata.Workers.W10.tauPower τ (∑ i, ξ i) := by
…
```
Mentions: OAI.Nagata.Workers.W10.tauPower