OAI/AlgebraicGeometry/PlaneCurves/ThetaSections.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.W08.exists_complex_nonroot line 19
2. theorem OAI.Nagata.W08.exists_cubic_second_mark line 37
3. def OAI.Nagata.W08.thetaProductSection line 88

   Source documentation

   A translate of the source theta product defines a section with multiplier -a.

   def thetaProductSection {τ a : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) :
       automorphicSections τ 1 (-a) :=
   …

   Mentions: OAI.Nagata.W08.automorphicSections

4. theorem OAI.Nagata.W08.thetaProductSection_apply line 101

   Source documentation

   The packaged section has exactly the source covering-frame scalar values on ℂ*.

   @[simp] theorem thetaProductSection_apply {τ a z : ℂ}
       (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0) :
       (thetaProductSection hτ hτ0 ha).val z = thetaProduct τ (z / a) := by
   …

   Mentions: OAI.Nagata.W08.thetaProductSection

5. theorem OAI.Nagata.W08.orbit_avoidance_symm line 119
6. theorem OAI.Nagata.W08.exists_three_distinct_orbit_marks line 126
7. theorem OAI.Nagata.W08.markedThetaProduct_automorphy line 179

   Source documentation

   The marked product has the exact tensor-product multiplier.

   theorem markedThetaProduct_automorphy {ι : Type*} [Fintype ι]
       {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (a : ι → ℂ) (ha : ∀ i, a i ≠ 0)
       {z : ℂ} (hz : z ≠ 0) :
       markedThetaProduct τ a (τ * z) =
         (∏ i, -a i) * z ^ (-(Fintype.card ι : ℤ)) * markedThetaProduct τ a z := by
   …

8. def OAI.Nagata.W08.markedThetaSection line 191

   Source documentation

   The actual marked divisor product as a genuine section of degree card ι.

   def markedThetaSection {ι : Type*} [Fintype ι]
       {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (a : ι → ℂ) (ha : ∀ i, a i ≠ 0) :
       automorphicSections τ (Fintype.card ι : ℤ) (∏ i, -a i) :=
   …

   Mentions: OAI.Nagata.W08.automorphicSections

9. theorem OAI.Nagata.W08.markedThetaSection_apply line 198
10. theorem OAI.Nagata.W08.markedThetaMultiplier_nine line 206

    Source documentation

    The nine-mark multiplier retains the source's negative sign.

    theorem markedThetaMultiplier_nine (a : Fin 9 → ℂ) :
        (∏ i, -a i) = -(∏ i, a i) := by
    …

11. theorem OAI.Nagata.W08.normalizedThetaTerm_summable line 224
12. theorem OAI.Nagata.W08.normalizedThetaSeries_differentiable line 231
13. theorem OAI.Nagata.W08.thetaProductSection_zero_iff line 249

    Source documentation

    The actual section has exactly the prescribed marked period orbit as its zero set on ℂ*.

    theorem thetaProductSection_zero_iff {τ a z : ℂ}
        (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0) :
        (thetaProductSection hτ hτ0 ha).val z = 0 ↔ ∃ k : ℤ, z = a * τ ^ k := by
    …

    Mentions: OAI.Nagata.W08.thetaProductSection

14. theorem OAI.Nagata.W08.thetaProductSection_at_mark line 255
15. theorem OAI.Nagata.W08.thetaProductSection_deriv line 262

    Source documentation

    The zero extension changes no derivative at a genuine point.

    theorem thetaProductSection_deriv {τ a z : ℂ}
        (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0) :
        deriv (thetaProductSection hτ hτ0 ha).val z =
          deriv (fun w ↦ thetaProduct τ (w / a)) z := by
    …

    Mentions: OAI.Nagata.W08.thetaProductSection

16. theorem OAI.Nagata.W08.thetaProductSection_zero_has_nonzero_deriv line 270

    Source documentation

    Every actual section zero has nonzero derivative in the covering coordinate.

    theorem thetaProductSection_zero_has_nonzero_deriv {τ a z : ℂ}
        (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0)
        (hf : (thetaProductSection hτ hτ0 ha).val z = 0) :
        deriv (thetaProductSection hτ hτ0 ha).val z ≠ 0 := by
    …

    Mentions: OAI.Nagata.W08.thetaProductSection

17. theorem OAI.Nagata.W08.thetaProductSection_ne_zero line 279

    Source documentation

    The constructed genuine theta section is nonzero.

    theorem thetaProductSection_ne_zero {τ a : ℂ}
        (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) :
        thetaProductSection hτ hτ0 ha ≠ 0 := by
    …

    Mentions: OAI.Nagata.W08.thetaProductSection

18. theorem OAI.Nagata.W08.markedThetaSection_zero_iff line 302

    Source documentation

    The marked section has precisely the marked period orbits as zeros on ℂ*.

    theorem markedThetaSection_zero_iff {ι : Type*} [Fintype ι]
        {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (a : ι → ℂ) (ha : ∀ i, a i ≠ 0)
        {z : ℂ} (hz : z ≠ 0) :
        (markedThetaSection hτ hτ0 a ha).val z = 0 ↔ ∃ i, ∃ k : ℤ, z = a i * τ ^ k := by
    …

    Mentions: OAI.Nagata.W08.markedThetaSection

19. theorem OAI.Nagata.W08.markedThetaSection_at_mark line 309
20. theorem OAI.Nagata.W08.markedThetaSection_deriv line 315

    Source documentation

    The forced zero value outside the genuine domain changes no derivative on ℂ*.

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

    Mentions: OAI.Nagata.W08.markedThetaSection

21. theorem OAI.Nagata.W08.markedThetaSection_zero_has_nonzero_deriv line 323

    Source documentation

    Distinct marked orbits give simple zeros of the actual section.

    theorem markedThetaSection_zero_has_nonzero_deriv {ι : Type*} [Fintype ι]
        {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (a : ι → ℂ) (ha : ∀ i, a i ≠ 0)
        (hdisjoint : Pairwise (fun i j ↦ ∀ k : ℤ, a i ≠ a j * τ ^ k))
        {z : ℂ} (hz : z ≠ 0) (hzero : (markedThetaSection hτ hτ0 a ha).val z = 0) :
        deriv (markedThetaSection hτ hτ0 a ha).val z ≠ 0 := by
    …

    Mentions: OAI.Nagata.W08.markedThetaSection

22. theorem OAI.Nagata.W08.markedThetaSection_ne_zero line 333

    Source documentation

    A nonempty disjoint marked family gives a nonzero genuine section.

    theorem markedThetaSection_ne_zero {ι : Type*} [Fintype ι] [Nonempty ι]
        {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (a : ι → ℂ) (ha : ∀ i, a i ≠ 0)
        (hdisjoint : Pairwise (fun i j ↦ ∀ k : ℤ, a i ≠ a j * τ ^ k)) :
        markedThetaSection hτ hτ0 a ha ≠ 0 := by
    …

    Mentions: OAI.Nagata.W08.markedThetaSection

23. def OAI.Nagata.W08.normalizedThetaSection line 365

    Source documentation

    The normalized integer-frequency theta series as a genuine global multiplier section.

    def normalizedThetaSection (n K : ℤ) (hn : 0 < n) (a : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) :
        automorphicSections (τ : ℂ) n (ε * ((τ ^ ((K : ℝ) - a) : ℝ) : ℂ)) :=
    …

    Mentions: OAI.Nagata.W08.automorphicSections

24. theorem OAI.Nagata.W08.normalizedThetaSection_exp line 378

    Source documentation

    Exact agreement with the normalized source series in every exponential coordinate.

    theorem normalizedThetaSection_exp (n K : ℤ) (hn : 0 < n) (a : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (x : ℂ) :
        (normalizedThetaSection n K hn a hε hτ hτone).val (Complex.exp x) =
          ∑' p : ℤ, normalizedThetaTerm (n : ℝ) a (K : ℝ) ε τ p x := by
    …

    Mentions: OAI.Nagata.W08.normalizedThetaSection

25. theorem OAI.Nagata.W08.normalizedThetaSection_centered line 401

    Source documentation

    Centering the genuine section agrees with centering each actual source summand.

    theorem normalizedThetaSection_centered (n K : ℤ) (hn : 0 < n) (a x₀ : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (x : ℂ) :
        ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) *
          (normalizedThetaSection n K hn a hε hτ hτone).val
            (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
          ∑' p : ℤ, normalizedThetaTerm (n : ℝ) (a + x₀ * (n : ℝ)) (K : ℝ) ε τ p x := by
    …

    Mentions: OAI.Nagata.W08.normalizedThetaSection

26. theorem OAI.Nagata.W08.exists_cubic_three_simple_zeros line 427
27. theorem OAI.Nagata.W08.exists_cubic_three_simple_zeros_pos_real line 453