Documentation

LeanPool.Chudnovsky.WeierstrassMore

The zeros of ℘′ and the factorization of ℘′² #

Statements from chapter 1 of Milla (arXiv:1809.00533v6, file 060_ElliptFunct.tex):

These results are proved here elementarily; the distinctness of e₁, e₂, e₃ and the characterisation of the zeros of ℘' use the third Liouville theorem (from LeanPool.Chudnovsky.Liouville) as a pinned interface.

source
noncomputable def PeriodPair.e₁ (L : PeriodPair) :
ℂ

The first half-lattice value e₁ = ℘(ω₁/2) (paper pstrichprod).

Equations
Instances For
    source
    noncomputable def PeriodPair.e₂ (L : PeriodPair) :
    ℂ

    The second half-lattice value e₂ = ℘(ω₂/2) (paper pstrichprod).

    Equations
    Instances For
      source
      noncomputable def PeriodPair.e₃ (L : PeriodPair) :
      ℂ

      The third half-lattice value e₃ = ℘((ω₁+ω₂)/2) (paper pstrichprod).

      Equations
      Instances For

        Zeros of ℘′ (paper zerowp) #

        source
        theorem PeriodPair.derivWeierstrassP_half_lattice (L : PeriodPair) (l : ↥L.lattice) :
        L.derivWeierstrassP (↑l / 2) = 0

        ℘' vanishes at every half-lattice point l/2 for l ∈ L. This is purely algebraic: ℘' is odd and L-periodic, so ℘'(l/2) = ℘'(l/2 - l) = ℘'(-l/2) = -℘'(l/2).

        source
        theorem PeriodPair.derivWeierstrassP_ω₁_div_two (L : PeriodPair) :
        L.derivWeierstrassP (L.ω₁ / 2) = 0

        ℘' vanishes at the half-period ω₁/2.

        source
        theorem PeriodPair.derivWeierstrassP_ω₂_div_two (L : PeriodPair) :
        L.derivWeierstrassP (L.ω₂ / 2) = 0

        ℘' vanishes at the half-period ω₂/2.

        source
        theorem PeriodPair.derivWeierstrassP_add_div_two (L : PeriodPair) :
        L.derivWeierstrassP ((L.ω₁ + L.ω₂) / 2) = 0

        ℘' vanishes at the half-period (ω₁+ω₂)/2.

        Auxiliary lemmas for the Liouville counting arguments #

        source
        theorem PeriodPair.notMem_lattice_of_mem_fund (L : PeriodPair) {z : ℂ} (hz : z ∈ L.fundamentalParallelogram) (hz0 : z ≠ 0) :
        z ∉ L.lattice

        The only lattice point of the fundamental parallelogram is 0.

        source
        theorem PeriodPair.meromorphicOrderAt_weierstrassP_sub (L : PeriodPair) {c l₀ : ℂ} (h : l₀ ∈ L.lattice) :
        meromorphicOrderAt (fun (z : ℂ) => L.weierstrassP z - c) l₀ = -2

        ℘ - c has a pole of order 2 at each lattice point.

        source
        theorem PeriodPair.isEllipticWith_weierstrassP_sub (L : PeriodPair) (c : ℂ) :
        L.IsEllipticWith fun (z : ℂ) => L.weierstrassP z - c

        ℘ - c is an elliptic function.

        source
        theorem PeriodPair.sum_untop₀_meromorphicOrderAt_le_two (L : PeriodPair) (c : ℂ) (A : Finset ℂ) (hAf : ∀ a ∈ A, a ∈ L.fundamentalParallelogram) (hAl : ∀ a ∈ A, a ∉ L.lattice) (hAz : ∀ a ∈ A, L.weierstrassP a = c) :
        ∑ a ∈ A, (meromorphicOrderAt (fun (z : ℂ) => L.weierstrassP z - c) a).untop₀ ≤ 2

        Counting bound from the third Liouville theorem: the elliptic function ℘ - c has, counted with multiplicity, at most 2 zeros in the fundamental parallelogram, since it has a single double pole (at 0). Concretely, for any finite set A of non-lattice points of the fundamental parallelogram at which ℘ = c, the multiplicities add up to at most 2.

        source
        theorem PeriodPair.two_le_untop₀_meromorphicOrderAt (L : PeriodPair) {c a : ℂ} (ha : a ∉ L.lattice) (hc : L.weierstrassP a = c) (hderiv : L.derivWeierstrassP a = 0) :
        2 ≤ (meromorphicOrderAt (fun (z : ℂ) => L.weierstrassP z - c) a).untop₀

        At a point a ∉ L where ℘ a = c and ℘' a = 0, the function ℘ - c has a zero of order at least 2.

        The factorization of ℘′² (paper pstrichprod) #

        source
        theorem PeriodPair.add_div_two_notMem_lattice (L : PeriodPair) :
        (L.ω₁ + L.ω₂) / 2 ∉ L.lattice

        (ω₁+ω₂)/2 is not a lattice point.

        source
        theorem PeriodPair.half_ne_half (L : PeriodPair) {a b a' b' : ℝ} (h : ¬(a = a' ∧ b = b')) :
        a • L.ω₁ + b • L.ω₂ ≠ a' • L.ω₁ + b' • L.ω₂

        Two distinct real-linear combinations of the periods with coefficients in [0,1) differ.

        source
        theorem PeriodPair.weierstrassP_ne_of_half (L : PeriodPair) {p q : ℂ} (hpf : p ∈ L.fundamentalParallelogram) (hqf : q ∈ L.fundamentalParallelogram) (hpl : p ∉ L.lattice) (hql : q ∉ L.lattice) (hpq : p ≠ q) (hp' : L.derivWeierstrassP p = 0) (hq' : L.derivWeierstrassP q = 0) :
        L.weierstrassP p ≠ L.weierstrassP q

        If two half-period points of the fundamental parallelogram are distinct, ℘ takes different values there (both are double zeros of ℘ - value, and ℘ - c has at most a double zero, by the counting bound).

        source
        theorem PeriodPair.e₁_ne_e₂ (L : PeriodPair) :
        L.e₁ ≠ L.e₂

        The half-lattice values are pairwise distinct: e₁ ≠ e₂.

        source
        theorem PeriodPair.e₁_ne_e₃ (L : PeriodPair) :
        L.e₁ ≠ L.e₃

        The half-lattice values are pairwise distinct: e₁ ≠ e₃.

        source
        theorem PeriodPair.e₂_ne_e₃ (L : PeriodPair) :
        L.e₂ ≠ L.e₃

        The half-lattice values are pairwise distinct: e₂ ≠ e₃.

        source
        theorem PeriodPair.derivWeierstrassP_sq_eq_four_mul_prod (L : PeriodPair) (z : ℂ) (hz : z ∉ L.lattice) :
        L.derivWeierstrassP z ^ 2 = 4 * (L.weierstrassP z - L.e₁) * (L.weierstrassP z - L.e₂) * (L.weierstrassP z - L.e₃)

        The factorization ℘'(z)² = 4(℘(z)-e₁)(℘(z)-e₂)(℘(z)-e₃) (paper pstrichprod).

        Characterisation of the zeros of ℘' (paper zerowp) #

        source
        theorem PeriodPair.exists_mem_fund (L : PeriodPair) (z₀ : ℂ) :
        ∃ p ∈ L.fundamentalParallelogram, z₀ - p ∈ L.lattice

        Every point of ℂ is congruent modulo L to a point of the fundamental parallelogram.

        source
        theorem PeriodPair.derivWeierstrassP_eq_zero_iff (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) :
        L.derivWeierstrassP z = 0 ↔ 2 * z ∈ L.lattice

        The zeros of ℘' are exactly the points ω/2 with ω ∈ L but ω/2 ∉ L, i.e. for z ∉ L we have ℘'(z) = 0 iff 2z ∈ L (paper zerowp).