NecessarySections.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Necessary section data for normal polynomials; Polynomial multiplicity and compatibility at nine marked points; Nonzero loci of sections

theorem OAI.Nagata.CoefficientSpaces.transformed_polynomial_order_iff line 16

Source documentation

The assembled actual polynomial has exactly the normal polynomial's ordinary local analytic multiplicity after the genuine fibre change away from the divisor.

theorem transformed_polynomial_order_iff
    (F G : Polynomial (ℂ → ℂ)) (N m : ℕ)
    (hF : ∀ j, N < j → F.coeff j = 0) (hG : ∀ j, N < j → G.coeff j = 0)
    (P : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
    (hP : AnalyticOnNhd ℂ P U) (hne : ∀ z ∈ U, P z ≠ 0)
    (hfactor : ∀ j, ∀ z ∈ U, P z ^ m * G.coeff j z = P z ^ j * F.coeff j z)
    (x : ℂ × ℂ) (hx : x.1 ∈ U) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ) (fun y : ℂ × ℂ => scalarExpression G y.1 y.2) x m ↔
…

Mentions: OAI.Nagata.CoefficientSpaces.scalarExpression

theorem OAI.Nagata.CoefficientSpaces.necessary_W_of_normal_polynomial line 53

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_of_normal_polynomial {ι : 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))
    (U : Set ℂ) (hU : IsOpen U) (hU0 : ∀ z ∈ U, z ≠ 0)
    (hUP : ∀ z ∈ U, (nineThetaSection hτ hτ0 a ha).val z ≠ 0)
…

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

theorem OAI.Nagata.CoefficientSpaces.nineThetaSection_ray_eq line 93

Source documentation

The actual marked section in necessary-W and in the source basis is the same function, including its prescribed value at the omitted origin.

theorem nineThetaSection_ray_eq {τ : ℝ} (hpos : 0 < τ) (hlt : τ < 1)
    (hτ : ‖(τ : ℂ)‖ < 1) (hτ0 : (τ : ℂ) ≠ 0) (ξ : Fin 9 → ℝ)
    (ha : ∀ i, ((τ ^ ξ i : ℝ) : ℂ) ≠ 0) :
    (nineThetaSection hτ hτ0 (fun i => ((τ ^ ξ i : ℝ) : ℂ)) ha).val =
      (Nagata.W22.rayMarkedSection hpos hlt ξ).val := rfl
…

Mentions: OAI.Nagata.CoefficientSpaces.nineThetaSection, OAI.Nagata.W22.rayMarkedSection

def OAI.Nagata.CoefficientSpaces.sectionNonzeroLocus line 109
Source documentation
The genuine nonvanishing locus of a section in the punctured covering plane.
```
def sectionNonzeroLocus {τ γ : ℂ} {n : ℤ}
    (P : Nagata.W08.automorphicSections τ n γ) : Set ℂ := {z | z ≠ 0 ∧ P.val z ≠ 0}
```
Mentions: OAI.Nagata.W08.automorphicSections
theorem OAI.Nagata.CoefficientSpaces.isOpen_sectionNonzeroLocus line 114
Source documentation
Zero extension at the omitted origin does not obstruct the actual open nonvanishing locus on the covering plane.
```
theorem isOpen_sectionNonzeroLocus {τ γ : ℂ} {n : ℤ}
    (P : Nagata.W08.automorphicSections τ n γ) : IsOpen (sectionNonzeroLocus P) := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.sectionNonzeroLocus