CoefficientTransforms.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Coefficient and polynomial transforms for marked normal polynomials

theorem OAI.Nagata.CoefficientSpaces.exists_transformed_coefficient line 15

Source documentation

The coefficient operation in Pi^-m F(Pi*v), with its exact algebraic identity valid even at the zeros of Pi.

theorem exists_transformed_coefficient {τ L Q : ℂ}
    (hτ : τ ≠ 0) (hL : L ≠ 0) (hQ : Q ≠ 0) (d : ℤ) (m j : ℕ)
    (P : Nagata.W08.automorphicSections τ 9 Q)
    (f : Nagata.W08.automorphicSections τ (3 * (d - 3 * (j : ℤ)))
      (L ^ (d - 3 * (j : ℤ))))
    (hzero : j ≤ m → ∀ z ≠ 0, P.val z = 0 → deriv P.val z ≠ 0 ∧
      ((m - j : ℕ) : ℕ∞) ≤ analyticOrderAt f.val z) :
    ∃ g ∈ coefficientSpace τ L Q d (m : ℤ) (j : ℤ) P.val,
      ∀ z ≠ 0, P.val z ^ m * g z = P.val z ^ j * f.val z := by
…

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

theorem OAI.Nagata.CoefficientSpaces.transformed_coefficient_nonzero line 44

Source documentation

The weighted coefficient identity cannot turn a genuine nonzero original section into the zero coefficient.

theorem transformed_coefficient_nonzero {τ L Q : ℂ} (d : ℤ) (m j : ℕ)
    (P : Nagata.W08.automorphicSections τ 9 Q)
    (hPfin : ∀ z ≠ 0, analyticOrderAt P.val z ≠ ⊤)
    (f : Nagata.W08.automorphicSections τ (3 * (d - 3 * (j : ℤ)))
      (L ^ (d - 3 * (j : ℤ)))) (g : ℂ → ℂ)
    (hfactor : ∀ z ≠ 0, P.val z ^ m * g z = P.val z ^ j * f.val z)
    (hf : f ≠ 0) : g ≠ 0 := by
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.exists_transformed_polynomial line 73

theorem OAI.Nagata.CoefficientSpaces.scalarExpression_eq_range line 142

Source documentation

Scalar evaluation may be taken over the common finite degree range.

theorem scalarExpression_eq_range (F : Polynomial (ℂ → ℂ)) (N : ℕ)
    (hbound : ∀ j, N < j → F.coeff j = 0) (z v : ℂ) :
    scalarExpression F z v = ∑ j ∈ Finset.range (N + 1), F.coeff j z * v ^ j := by
…

Mentions: OAI.Nagata.CoefficientSpaces.scalarExpression

theorem OAI.Nagata.CoefficientSpaces.scalarExpression_transform line 156

Source documentation

The coefficient identities are the manuscript's actual local scalar substitution identity, not merely a matrix or an abstract coefficient model.

theorem scalarExpression_transform (F G : Polynomial (ℂ → ℂ)) (N m : ℕ)
    (hF : ∀ j, N < j → F.coeff j = 0) (hG : ∀ j, N < j → G.coeff j = 0)
    (P : ℂ → ℂ) (z v : ℂ)
    (hfactor : ∀ j, P z ^ m * G.coeff j z = P z ^ j * F.coeff j z) :
    P z ^ m * scalarExpression G z v = scalarExpression F z (P z * v) := by
…

Mentions: OAI.Nagata.CoefficientSpaces.scalarExpression

def OAI.Nagata.CoefficientSpaces.nineThetaSection line 178

Source documentation

The actual nine-theta product as a degree-nine section.

noncomputable def nineThetaSection {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0)
    (a : Fin 9 → ℂ) (ha : ∀ i, a i ≠ 0) :
    Nagata.W08.automorphicSections τ 9 (∏ i, -a i) := by
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.exists_marked_transformed_polynomial line 186

Source documentation

Nine ordinary numerator-order conditions suffice: period automorphy propagates orders to the complete divisor, and the genuine theta product supplies simplicity.

theorem exists_marked_transformed_polynomial {τ 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 (ℂ → ℂ))
    (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)) :
    ∃ G : polynomialSections τ L (∏ i, -a i) d (m : ℤ)
        (nineThetaSection hτ hτ0 a ha).val,
…

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