UniversalSections.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Nonzero necessary sections, marked Taylor orders, and local smooth constructions; Automorphic normal polynomials on curves and smooth curves

theorem OAI.Nagata.CoefficientSpaces.necessary_W_at_nonzero_points line 19

Source documentation

The actual necessary-W implication from the normal polynomial. It uses the nine marked coefficient orders and the source multiplicities at all moving points. The source normal-specialization theorem must supply precisely these inputs.

theorem necessary_W_at_nonzero_points {ι : Type*} {τ L : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hL : L ≠ 0)
    (a : Fin 9 → ℂ) (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j => ∀ k : ℤ, a i ≠ a j * τ ^ k))
    (d : ℤ) (m : ℕ) (F : Polynomial (ℂ → ℂ)) (hneF : F ≠ 0)
    (hbound : ∀ j : ℕ, (d / 3).toNat < j → F.coeff j = 0)
    (hsource : ∀ j : ℕ, F.coeff j ∈ Nagata.W08.automorphicSections τ
      (3 * (d - 3 * (j : ℤ))) (L ^ (d - 3 * (j : ℤ))))
    (hmarked : ∀ j : ℕ, j ≤ (d / 3).toNat → j ≤ m → ∀ i : Fin 9,
      ((m - j : ℕ) : ℕ∞) ≤ analyticOrderAt (F.coeff j) (a i))
    (p : ι → ℂ × ℂ) (hp0 : ∀ i, (p i).1 ≠ 0)
    (hpP : ∀ i, (nineThetaSection hτ hτ0 a ha).val (p i).1 ≠ 0)
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.nineThetaSection

theorem OAI.Nagata.CoefficientSpaces.necessary_W_of_normal_Taylor_orders line 56

Source documentation

theorem necessary_W_of_normal_Taylor_orders {ι : Type*} {τ L : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hL : L ≠ 0)
    (a : Fin 9 → ℂ) (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j => ∀ k : ℤ, a i ≠ a j * τ ^ k))
    (d : ℤ) (m : ℕ) (F : Polynomial (ℂ → ℂ)) (hneF : F ≠ 0)
    (hbound : ∀ j : ℕ, (d / 3).toNat < j → F.coeff j = 0)
    (hsource : ∀ j : ℕ, F.coeff j ∈ Nagata.W08.automorphicSections τ
      (3 * (d - 3 * (j : ℤ))) (L ^ (d - 3 * (j : ℤ))))
    (hfixed : ∀ i : Fin 9, HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.necessary_W_of_nonzero_ambient_restriction line 92

Source documentation

The complete actual necessary-W transformation from an ambient polynomial normal section restricted by genuine degree-three coordinate sections. The nonzero restriction is a genuine polynomial inequality.

theorem necessary_W_of_nonzero_ambient_restriction {ι σ : Type*} {τ L : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hL : L ≠ 0)
    (a : Fin 9 → ℂ) (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j => ∀ k : ℤ, a i ≠ a j * τ ^ k))
    (d m : ℕ) (X : σ → Nagata.W08.automorphicSections τ 3 L)
    (F : Polynomial (MvPolynomial σ ℂ))
    (hhom : ∀ j, (F.coeff j).IsHomogeneous (d - 3 * j))
    (hbound : ∀ j, d / 3 < j → F.coeff j = 0)
    (hneF : restrictedNormalPolynomial (fun i => (X i).val) F ≠ 0)
    (hfixed : ∀ i : Fin 9, HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.Workers.W17.universalSupport_normal_polynomial_on_automorphic_curve line 134
def OAI.Nagata.CoefficientSpaces.markedNormalBase line 181
Source documentation
The actual nine marked lifts followed by the moving base lifts.
```
def markedNormalBase {q : ℕ} (a : Fin 9 → ℂ) (p : Fin q → ℂ × ℂ) : Fin (9 + q) → ℂ :=
…
```
def OAI.Nagata.CoefficientSpaces.markedNormalFibre line 185
Source documentation
Zero normal displacements at the nine marks and Pi-scaled moving displacements.
```
def markedNormalFibre {q : ℕ} (P : ℂ → ℂ) (p : Fin q → ℂ × ℂ) : Fin (9 + q) → ℂ :=
…
```
theorem OAI.Nagata.CoefficientSpaces.universalSupport_necessary_W line 188
theorem OAI.Nagata.Workers.W17.universalSupport_normal_polynomial_on_smooth_automorphic_curve line 239

theorem OAI.Nagata.CoefficientSpaces.universalSupport_necessary_W_local line 286

Source documentation

The genuine universal-support necessary-W conclusion in the actual local logarithmic scalar coordinates used by the collision and jet maps.

theorem universalSupport_necessary_W_local {q d m : ℕ} {τ L : ℂ}
    (hU : Nagata.W13.UniversalSupport (9 + q) d (fun _ => m))
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hL : L ≠ 0)
    (a : Fin 9 → ℂ) (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j => ∀ k : ℤ, a i ≠ a j * τ ^ k))
    (z₀ : ℂ) (hz₀ : z₀ ≠ 0) (ξ : Fin q → ℂ)
    (hpP : ∀ i, (nineThetaSection hτ hτ0 a ha).val ((logarithmicPoints z₀ ξ) i).1 ≠ 0)
    (C : MvPolynomial (Fin 3) ℂ) (hC : C.IsHomogeneous 3)
    (X : Fin 3 → Nagata.W08.automorphicSections τ 3 L)
    (hrelations : Nagata.Workers.W25.polynomialRelationIdeal (fun i => (X i).val) =
      Ideal.span ({C} : Set _))
    (chart : Fin (9 + q) → Fin 3)
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.CoefficientSpaces.nineThetaSection, OAI.Nagata.CoefficientSpaces.logarithmicPoints, OAI.Nagata.W08.automorphicSections, OAI.Nagata.Workers.W25.polynomialRelationIdeal

theorem OAI.Nagata.CoefficientSpaces.universalSupport_necessary_W_smooth line 325

theorem OAI.Nagata.CoefficientSpaces.universalSupport_necessary_W_smooth_local line 378

Source documentation

The genuine universal-support necessary-W conclusion in the actual local logarithmic scalar coordinates used by the collision and jet maps.

theorem universalSupport_necessary_W_smooth_local {q d m : ℕ} {τ L : ℂ}
    (hU : Nagata.W13.UniversalSupport (9 + q) d (fun _ => m))
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hL : L ≠ 0)
    (a : Fin 9 → ℂ) (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j => ∀ k : ℤ, a i ≠ a j * τ ^ k))
    (z₀ : ℂ) (hz₀ : z₀ ≠ 0) (ξ : Fin q → ℂ)
    (hpP : ∀ i, (nineThetaSection hτ hτ0 a ha).val ((logarithmicPoints z₀ ξ) i).1 ≠ 0)
    (C : MvPolynomial (Fin 3) ℂ) (hC : C.IsHomogeneous 3)
    (X : Fin 3 → Nagata.W08.automorphicSections τ 3 L)
    (hrelations : Nagata.Workers.W25.polynomialRelationIdeal (fun i => (X i).val) =
      Ideal.span ({C} : Set _))
    (chart : Fin (9 + q) → Fin 3)
…