OAI/AlgebraicGeometry/PlaneCurves/ThetaCoefficients.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Nagata.W09.thetaCircleMajorant line 17
2. theorem OAI.Nagata.W09.thetaCircleMajorant_summable line 22
3. theorem OAI.Nagata.W09.normalizedLaurentMonomial_circle_bound line 30
4. theorem OAI.Nagata.W09.normalizedLaurentMonomial_hasSum_on_circle line 48

   Source documentation

   The exact local theta-series identity and the checked fixed-disk majorant supply a genuine monomial HasSum on the physical circle r=tau^x0.

   theorem normalizedLaurentMonomial_hasSum_on_circle
       {τ : ℝ} (hτ : 0 < τ) (hτone : τ ≤ 1) (σ x₀ : ℝ)
       {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 ≤ n) (K : ℤ)
       (hhalf : Real.exp ((n : ℝ) * (2 * Real.pi)) *
         τ ^ thetaMargin (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ)) ≤ 1 / 2)
       (f : ℂ → ℂ)
       (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
         ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
           (K : ℝ) ε τ p x)
       {z : ℂ} (hz : z ∈ sphere 0 (τ ^ x₀)) :
       HasSum (fun p : ℤ => normalizedLaurentCoefficient τ σ x₀ ε n K p * z ^ (K + n * p)) (f z) := by
   …

5. theorem OAI.Nagata.W09.analyticLaurentCoeff_of_local_theta_series line 72

   Source documentation

   Under the exact local theta identity, actual contour extraction recovers each explicit chosen Laurent coefficient; normal convergence is proved above.

   theorem analyticLaurentCoeff_of_local_theta_series
       {τ : ℝ} (hτ : 0 < τ) (hτone : τ ≤ 1) (σ x₀ : ℝ)
       {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 < n) (K : ℤ)
       (hhalf : Real.exp ((n : ℝ) * (2 * Real.pi)) *
         τ ^ thetaMargin (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ)) ≤ 1 / 2)
       (f : ℂ → ℂ)
       (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
         ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
           (K : ℝ) ε τ p x) (p : ℤ) :
       analyticLaurentCoeff (τ ^ x₀) f (K + n * p) = normalizedLaurentCoefficient τ σ x₀ ε n K p := by
   …

   Mentions: OAI.Nagata.W09.analyticLaurentCoeff

6. theorem OAI.Nagata.W09.analyticLaurentCoeff_local_theta_off_residue line 94

   Source documentation

   The analytic coefficient vanishes outside the selected residue class.

   theorem analyticLaurentCoeff_local_theta_off_residue
       {τ : ℝ} (hτ : 0 < τ) (hτone : τ ≤ 1) (σ x₀ : ℝ)
       {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 ≤ n) (K : ℤ)
       (hhalf : Real.exp ((n : ℝ) * (2 * Real.pi)) *
         τ ^ thetaMargin (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ)) ≤ 1 / 2)
       (f : ℂ → ℂ)
       (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
         ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
           (K : ℝ) ε τ p x) (k : ℤ) (hk : k % n ≠ K % n) :
       analyticLaurentCoeff (τ ^ x₀) f k = 0 := by
   …

   Mentions: OAI.Nagata.W09.analyticLaurentCoeff

7. theorem OAI.Nagata.W09.analyticLaurentCoeff_local_theta_eq_supportedOrbit line 119

   Source documentation

   Literal analytic extraction of the normalized local theta series equals the explicitly constructed recurrence coefficient sequence at every integer.

   theorem analyticLaurentCoeff_local_theta_eq_supportedOrbit
       {τ : ℝ} (hτ : 0 < τ) (hτone : τ ≤ 1) (σ x₀ : ℝ)
       {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 < n) (K : ℤ)
       (hhalf : Real.exp ((n : ℝ) * (2 * Real.pi)) *
         τ ^ thetaMargin (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ)) ≤ 1 / 2)
       (f : ℂ → ℂ)
       (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
         ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
           (K : ℝ) ε τ p x) (k : ℤ) :
       analyticLaurentCoeff (τ ^ x₀) f k =
         supportedOrbitCoefficient (τ : ℂ) (ε * ((τ ^ σ : ℝ) : ℂ)) n K
           ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) k := by
   …

   Mentions: OAI.Nagata.W09.analyticLaurentCoeff, OAI.Nagata.W09.supportedOrbitCoefficient

8. theorem OAI.Nagata.W09.norm_normalizedThetaTerm_imaginary line 154

   Source documentation

   On an imaginary logarithmic contour the frequency exponential has norm one.

   theorem norm_normalizedThetaTerm_imaginary {n a K τ : ℝ} {ε : ℂ}
       (hτ : 0 < τ) (hε : ‖ε‖ = 1) (p : ℤ) (θ : ℝ) :
       ‖normalizedThetaTerm n a K ε τ p ((θ : ℂ) * Complex.I)‖ =
         τ ^ thetaExponent n a (p : ℝ) := by
   …

9. theorem OAI.Nagata.W09.summable_geometric_natAbs line 162

   Source documentation

   A bilateral geometric majorant, summable for every q in [0,1).

   theorem summable_geometric_natAbs {q : ℝ} (hq : 0 ≤ q) (hqone : q < 1) :
       Summable (fun p : ℤ => q ^ p.natAbs) := by
   …

10. def OAI.Nagata.W09.thetaImaginaryMajorant line 173
11. theorem OAI.Nagata.W09.thetaImaginaryMajorant_summable line 176
12. theorem OAI.Nagata.W09.normalizedLaurentMonomial_circle_sharp_bound line 182
13. theorem OAI.Nagata.W09.normalizedThetaTerm_hasSum_imaginary line 195
14. def OAI.Nagata.W09.normalizedSourceThetaSection line 222

    Source documentation

    The manuscript's normalized theta section as a genuine holomorphic multiplier section, with the common multiplier gamma=epsilon*tau^sigma.

    def normalizedSourceThetaSection (n K : ℤ) (hn : 0 < n) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) :
        Nagata.W08.automorphicSections (τ : ℂ) n (ε * ((τ ^ σ : ℝ) : ℂ)) := by
    …

    Mentions: OAI.Nagata.W08.automorphicSections

15. theorem OAI.Nagata.W09.normalizedSourceThetaSection_apply line 242
16. theorem OAI.Nagata.W09.normalizedSourceThetaSection_centered line 250

    Source documentation

    Exact local expression of the genuine global source-normalized section.

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

    Mentions: OAI.Nagata.W09.normalizedSourceThetaSection

17. theorem OAI.Nagata.W09.normalizedLaurentMonomial_hasSum_on_circle_all_tau line 271

    Source documentation

    The exact local theta-series identity and the checked fixed-disk majorant supply a genuine monomial HasSum on the physical circle r=tau^x0.

    theorem normalizedLaurentMonomial_hasSum_on_circle_all_tau
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 ≤ n) (K : ℤ)
        (ha : 0 < (K : ℝ) - σ + x₀ * (n : ℝ))
        (han : (K : ℝ) - σ + x₀ * (n : ℝ) < (n : ℝ))
        (f : ℂ → ℂ)
        (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
          ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
            (K : ℝ) ε τ p x)
        {z : ℂ} (hz : z ∈ sphere 0 (τ ^ x₀)) :
        HasSum (fun p : ℤ => normalizedLaurentCoefficient τ σ x₀ ε n K p * z ^ (K + n * p)) (f z) := by
    …

18. theorem OAI.Nagata.W09.analyticLaurentCoeff_of_local_theta_series_all_tau line 291

    Source documentation

    Under the exact local theta identity, actual contour extraction recovers each explicit chosen Laurent coefficient; normal convergence is proved above.

    theorem analyticLaurentCoeff_of_local_theta_series_all_tau
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 < n) (K : ℤ)
        (ha : 0 < (K : ℝ) - σ + x₀ * (n : ℝ))
        (han : (K : ℝ) - σ + x₀ * (n : ℝ) < (n : ℝ))
        (f : ℂ → ℂ)
        (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
          ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
            (K : ℝ) ε τ p x) (p : ℤ) :
        analyticLaurentCoeff (τ ^ x₀) f (K + n * p) = normalizedLaurentCoefficient τ σ x₀ ε n K p := by
    …

    Mentions: OAI.Nagata.W09.analyticLaurentCoeff

19. theorem OAI.Nagata.W09.analyticLaurentCoeff_local_theta_off_residue_all_tau line 313

    Source documentation

    The analytic coefficient vanishes outside the selected residue class.

    theorem analyticLaurentCoeff_local_theta_off_residue_all_tau
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 ≤ n) (K : ℤ)
        (ha : 0 < (K : ℝ) - σ + x₀ * (n : ℝ))
        (han : (K : ℝ) - σ + x₀ * (n : ℝ) < (n : ℝ))
        (f : ℂ → ℂ)
        (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
          ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
            (K : ℝ) ε τ p x) (k : ℤ) (hk : k % n ≠ K % n) :
        analyticLaurentCoeff (τ ^ x₀) f k = 0 := by
    …

    Mentions: OAI.Nagata.W09.analyticLaurentCoeff

20. theorem OAI.Nagata.W09.analyticLaurentCoeff_local_theta_eq_supportedOrbit_all_tau line 338

    Source documentation

    Literal analytic extraction of the normalized local theta series equals the explicitly constructed recurrence coefficient sequence at every integer.

    theorem analyticLaurentCoeff_local_theta_eq_supportedOrbit_all_tau
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ‖ε‖ = 1) {n : ℤ} (hn : 0 < n) (K : ℤ)
        (ha : 0 < (K : ℝ) - σ + x₀ * (n : ℝ))
        (han : (K : ℝ) - σ + x₀ * (n : ℝ) < (n : ℝ))
        (f : ℂ → ℂ)
        (hlocal : ∀ x : ℂ, f (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
          ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
            (K : ℝ) ε τ p x) (k : ℤ) :
        analyticLaurentCoeff (τ ^ x₀) f k =
          supportedOrbitCoefficient (τ : ℂ) (ε * ((τ ^ σ : ℝ) : ℂ)) n K
            ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) k := by
    …

    Mentions: OAI.Nagata.W09.analyticLaurentCoeff, OAI.Nagata.W09.supportedOrbitCoefficient

21. theorem OAI.Nagata.W09.laurentCoefficientMap_normalizedSourceThetaSection line 375

    Source documentation

    The actual analytic extraction map of the genuine global theta section is exactly the explicit supported Laurent orbit, for the concrete normal-convergence parameter range used by the degeneration.

    theorem laurentCoefficientMap_normalizedSourceThetaSection
        (n K : ℤ) (hn : 0 < n) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) (hunit : ‖ε‖ = 1)
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
        (hhalf : Real.exp ((n : ℝ) * (2 * Real.pi)) *
          τ ^ thetaMargin (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ)) ≤ 1 / 2) (k : ℤ) :
        laurentCoefficientMap (τ : ℂ) n (ε * ((τ ^ σ : ℝ) : ℂ))
          (normalizedSourceThetaSection n K hn σ x₀ hε hτ hτone) k =
          supportedOrbitCoefficient (τ : ℂ) (ε * ((τ ^ σ : ℝ) : ℂ)) n K
            ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) k := by
    …

    Mentions: OAI.Nagata.W09.laurentCoefficientMap, OAI.Nagata.W09.normalizedSourceThetaSection, OAI.Nagata.W09.supportedOrbitCoefficient

22. theorem OAI.Nagata.W09.laurentCoefficientMap_normalizedSourceThetaSection_all_tau line 395

    Source documentation

    The actual analytic extraction map of the genuine global theta section is exactly the explicit supported Laurent orbit, for the concrete normal-convergence parameter range used by the degeneration.

    theorem laurentCoefficientMap_normalizedSourceThetaSection_all_tau
        (n K : ℤ) (hn : 0 < n) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) (hunit : ‖ε‖ = 1)
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
        (ha : 0 < (K : ℝ) - σ + x₀ * (n : ℝ))
        (han : (K : ℝ) - σ + x₀ * (n : ℝ) < (n : ℝ)) (k : ℤ) :
        laurentCoefficientMap (τ : ℂ) n (ε * ((τ ^ σ : ℝ) : ℂ))
          (normalizedSourceThetaSection n K hn σ x₀ hε hτ hτone) k =
          supportedOrbitCoefficient (τ : ℂ) (ε * ((τ ^ σ : ℝ) : ℂ)) n K
            ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) k := by
    …

    Mentions: OAI.Nagata.W09.laurentCoefficientMap, OAI.Nagata.W09.normalizedSourceThetaSection, OAI.Nagata.W09.supportedOrbitCoefficient