Weierstrass ℘ functions

Main definitions and results

• PeriodPair.weierstrassP: The Weierstrass ℘-function associated to a pair of periods.

• PeriodPair.hasSumLocallyUniformly_weierstrassP: The summands of ℘ sums to ℘ locally uniformly.

• PeriodPair.differentiableOn_weierstrassP: ℘ is differentiable away from the lattice points.

• PeriodPair.weierstrassP_add_coe: The Weierstrass ℘-function is periodic.

• PeriodPair.weierstrassP_neg: The Weierstrass ℘-function is even.

• PeriodPair.derivWeierstrassP: The derivative of the Weierstrass ℘-function associated to a pair of periods.

• PeriodPair.hasSumLocallyUniformly_derivWeierstrassP: The summands of ℘' sums to ℘' locally uniformly.

• PeriodPair.differentiableOn_derivWeierstrassP: ℘' is differentiable away from the lattice points.

• PeriodPair.derivWeierstrassP_add_coe: ℘' is periodic.

• PeriodPair.weierstrassP_neg: ℘' is odd.

• PeriodPair.deriv_weierstrassP: deriv ℘ = ℘'. This is true globally because of junk values.

• PeriodPair.analyticOnNhd_weierstrassP: ℘ is analytic away from the lattice points.

• PeriodPair.meromorphic_weierstrassP: ℘ is meromorphic on the whole plane.

• PeriodPair.order_weierstrassP: ℘ has a pole of order 2 at each of the lattice points.

• PeriodPair.derivWeierstrassP_sq : ℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃

tags

Weierstrass p-functions, Weierstrass p functions

structure PeriodPair : Type

A pair of ℝ-linearly independent complex numbers. They span the period lattice in lattice, and are the periods of the elliptic functions we shall construct.

• ω₁ : ℂ

  The first period in a PeriodPair.

• ω₂ : ℂ

  The second period in a PeriodPair.

• indep : LinearIndependent ℝ ![self.ω₁, self.ω₂]

noncomputable def PeriodPair.basis (L : PeriodPair) : Module.Basis (Fin 2) ℝ ℂ

The ℝ-basis of ℂ determined by a pair of periods.

Equations

• L.basis = basisOfLinearIndependentOfCardEqFinrank ⋯ PeriodPair.basis._proof_1

@[simp]

theorem PeriodPair.basis_zero (L : PeriodPair) : L.basis 0 = L.ω₁

@[simp]

theorem PeriodPair.basis_one (L : PeriodPair) : L.basis 1 = L.ω₂

noncomputable def PeriodPair.lattice (L : PeriodPair) : Submodule ℤ ℂ

The lattice spanned by a pair of periods.

Equations

• L.lattice = Submodule.span ℤ {L.ω₁, L.ω₂}

theorem PeriodPair.mem_lattice {L : PeriodPair} {x : ℂ} : x ∈ L.lattice ↔ ∃ (m : ℤ) (n : ℤ), ↑m * L.ω₁ + ↑n * L.ω₂ = x

theorem PeriodPair.ω₁_mem_lattice (L : PeriodPair) : L.ω₁ ∈ L.lattice

theorem PeriodPair.ω₂_mem_lattice (L : PeriodPair) : L.ω₂ ∈ L.lattice

theorem PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice {L : PeriodPair} {α β : ℚ} : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1

theorem PeriodPair.ω₁_div_two_notMem_lattice (L : PeriodPair) : L.ω₁ / 2 ∉ L.lattice

theorem PeriodPair.ω₂_div_two_notMem_lattice (L : PeriodPair) : L.ω₂ / 2 ∉ L.lattice

theorem PeriodPair.lattice_eq_span_range_basis (L : PeriodPair) : L.lattice = Submodule.span ℤ (Set.range ⇑L.basis)

instance PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice (L : PeriodPair) : DiscreteTopology ↥L.lattice

instance PeriodPair.instIsZLatticeRealComplexLattice (L : PeriodPair) : IsZLattice ℝ L.lattice

theorem PeriodPair.isClosed_lattice (L : PeriodPair) : IsClosed ↑L.lattice

theorem PeriodPair.isClosed_of_subset_lattice (L : PeriodPair) {s : Set ℂ} (hs : s ⊆ ↑L.lattice) : IsClosed s

theorem PeriodPair.isOpen_compl_lattice_diff (L : PeriodPair) {s : Set ℂ} : IsOpen (↑L.lattice \ s)ᶜ

theorem PeriodPair.compl_lattice_diff_singleton_mem_nhds (L : PeriodPair) (x : ℂ) : (↑L.lattice \ {x})ᶜ ∈ nhds x

instance PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice (L : PeriodPair) : ProperSpace ↥L.lattice

noncomputable def PeriodPair.latticeBasis (L : PeriodPair) : Module.Basis (Fin 2) ℤ ↥L.lattice

The ℤ-basis of the lattice determined by a pair of periods.

Equations

• L.latticeBasis = (Module.Basis.span ⋯).map (LinearEquiv.ofEq (Submodule.span ℤ (Set.range ![L.ω₁, L.ω₂])) L.lattice ⋯)

@[simp]

theorem PeriodPair.latticeBasis_zero (L : PeriodPair) : ↑(L.latticeBasis 0) = L.ω₁

@[simp]

theorem PeriodPair.latticeBasis_one (L : PeriodPair) : ↑(L.latticeBasis 1) = L.ω₂

@[simp]

theorem PeriodPair.finrank_lattice (L : PeriodPair) : Module.finrank ℤ ↥L.lattice = 2

noncomputable def PeriodPair.latticeEquivProd (L : PeriodPair) : ↥L.lattice ≃ₗ[ℤ] ℤ × ℤ

The equivalence from the lattice generated by a pair of periods to ℤ × ℤ.

Equations

• L.latticeEquivProd = L.latticeBasis.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ (Fin 2) ≪≫ₗ LinearEquiv.finTwoArrow ℤ ℤ

theorem PeriodPair.latticeEquiv_symm_apply (L : PeriodPair) (x : ℤ × ℤ) : ↑(L.latticeEquivProd.symm x) = ↑x.1 * L.ω₁ + ↑x.2 * L.ω₂

theorem PeriodPair.hasSumLocallyUniformly_aux (L : PeriodPair) (f : ↥L.lattice → ℂ → ℂ) (u : ℝ → ↥L.lattice → ℝ) (hu : ∀ r > 0, Summable (u r)) (hf : ∀ r > 0, ∀ᶠ (R : ℝ) in Filter.atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l) : HasSumLocallyUniformly f fun (x : ℂ) => ∑' (j : ↥L.lattice), f j x

theorem PeriodPair.weierstrassP_bound (r : ℝ) (hr : 0 < r) (s : ℂ) (hs : ‖s‖ < r) (l : ℂ) (h : 2 * r ≤ ‖l‖) : ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

noncomputable def PeriodPair.weierstrassPExcept (L : PeriodPair) (l₀ z : ℂ) : ℂ

The Weierstrass ℘ function with the l₀-term missing. This is mainly a tool for calculations where one would want to omit a diverging term. This has the notation ℘[L - l₀] in the namespace PeriodPairs.

Equations

• L.weierstrassPExcept l₀ z = ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2

def PeriodPair.«term℘[_-_]» : Lean.ParserDescr

The Weierstrass ℘ function with the l₀-term missing. This is mainly a tool for calculations where one would want to omit a diverging term. This has the notation ℘[L - l₀] in the namespace PeriodPairs.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.hasSumLocallyUniformly_weierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) => if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) (L.weierstrassPExcept l₀)

theorem PeriodPair.hasSum_weierstrassPExcept (L : PeriodPair) (l₀ z : ℂ) : HasSum (fun (l : ↥L.lattice) => if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) (L.weierstrassPExcept l₀ z)

theorem PeriodPair.differentiableOn_weierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : DifferentiableOn ℂ (L.weierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ

theorem PeriodPair.weierstrassPExcept_neg (L : PeriodPair) (l₀ z : ℂ) : L.weierstrassPExcept l₀ (-z) = L.weierstrassPExcept (-l₀) z

@[simp]

theorem PeriodPair.weierstrassPExcept_zero (L : PeriodPair) (l₀ : ℂ) : L.weierstrassPExcept l₀ 0 = 0

noncomputable def PeriodPair.weierstrassP (L : PeriodPair) (z : ℂ) : ℂ

The Weierstrass ℘ function. This has the notation ℘[L] in the namespace PeriodPairs.

Equations

• L.weierstrassP z = ∑' (l : ↥L.lattice), (1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2)

def PeriodPair.«term℘[_]» : Lean.ParserDescr

The Weierstrass ℘ function. This has the notation ℘[L] in the namespace PeriodPairs.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.weierstrassPExcept_add (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ) : L.weierstrassPExcept (↑l₀) z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = L.weierstrassP z

theorem PeriodPair.weierstrassPExcept_def (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ) : L.weierstrassPExcept (↑l₀) z = L.weierstrassP z + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)

theorem PeriodPair.weierstrassPExcept_of_notMem (L : PeriodPair) (l₀ : ℂ) (hl : l₀ ∉ L.lattice) : L.weierstrassPExcept l₀ = L.weierstrassP

theorem PeriodPair.hasSumLocallyUniformly_weierstrassP (L : PeriodPair) : HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) => 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) L.weierstrassP

theorem PeriodPair.hasSum_weierstrassP (L : PeriodPair) (z : ℂ) : HasSum (fun (l : ↥L.lattice) => 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) (L.weierstrassP z)

theorem PeriodPair.differentiableOn_weierstrassP (L : PeriodPair) : DifferentiableOn ℂ L.weierstrassP (↑L.lattice)ᶜ

@[simp]

theorem PeriodPair.weierstrassP_neg (L : PeriodPair) (z : ℂ) : L.weierstrassP (-z) = L.weierstrassP z

theorem PeriodPair.not_continuousAt_weierstrassP (L : PeriodPair) (x : ℂ) (hx : x ∈ L.lattice) : ¬ContinuousAt L.weierstrassP x

noncomputable def PeriodPair.derivWeierstrassPExcept (L : PeriodPair) (l₀ z : ℂ) : ℂ

The derivative of Weierstrass ℘ function with the l₀-term missing. This is mainly a tool for calculations where one would want to omit a diverging term. This has the notation ℘'[L - l₀] in the namespace PeriodPairs.

Equations

• L.derivWeierstrassPExcept l₀ z = ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3

def PeriodPair.«term℘'[_-_]» : Lean.ParserDescr

The derivative of Weierstrass ℘ function with the l₀-term missing. This is mainly a tool for calculations where one would want to omit a diverging term. This has the notation ℘'[L - l₀] in the namespace PeriodPairs.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) => if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) (L.derivWeierstrassPExcept l₀)

theorem PeriodPair.hasSum_derivWeierstrassPExcept (L : PeriodPair) (l₀ z : ℂ) : HasSum (fun (l : ↥L.lattice) => if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) (L.derivWeierstrassPExcept l₀ z)

theorem PeriodPair.differentiableOn_derivWeierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : DifferentiableOn ℂ (L.derivWeierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ

theorem PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : Set.EqOn (deriv (L.weierstrassPExcept l₀)) (L.derivWeierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ

@[simp]

theorem PeriodPair.deriv_weierstrassPExcept_same (L : PeriodPair) (l : ℂ) : deriv (L.weierstrassPExcept l) l = L.derivWeierstrassPExcept l l

theorem PeriodPair.derivWeierstrassPExcept_neg (L : PeriodPair) (l₀ z : ℂ) : L.derivWeierstrassPExcept l₀ (-z) = -L.derivWeierstrassPExcept (-l₀) z

@[simp]

theorem PeriodPair.derivWeierstrassPExcept_zero_zero (L : PeriodPair) : L.derivWeierstrassPExcept 0 0 = 0

theorem PeriodPair.derivWeierstrassPExcept_add_coe (L : PeriodPair) (l₀ z : ℂ) (l : ↥L.lattice) : L.derivWeierstrassPExcept l₀ (z + ↑l) = L.derivWeierstrassPExcept (l₀ - ↑l) z

@[simp]

theorem PeriodPair.weierstrassP_add_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.weierstrassP (z + ↑l) = L.weierstrassP z

theorem PeriodPair.periodic_weierstrassP (L : PeriodPair) (l : ↥L.lattice) : Function.Periodic L.weierstrassP ↑l

@[simp]

theorem PeriodPair.weierstrassP_zero (L : PeriodPair) : L.weierstrassP 0 = 0

@[simp]

theorem PeriodPair.weierstrassP_coe (L : PeriodPair) (l : ↥L.lattice) : L.weierstrassP ↑l = 0

@[simp]

theorem PeriodPair.weierstrassP_sub_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.weierstrassP (z - ↑l) = L.weierstrassP z

noncomputable def PeriodPair.derivWeierstrassP (L : PeriodPair) (z : ℂ) : ℂ

The derivative of Weierstrass ℘ function. This has the notation ℘'[L] in the namespace PeriodPairs.

Equations

• L.derivWeierstrassP z = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

def PeriodPair.«term℘'[_]» : Lean.ParserDescr

The Weierstrass ℘ function. This has the notation ℘[L] in the namespace PeriodPairs.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.derivWeierstrassPExcept_sub (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ) : L.derivWeierstrassPExcept (↑l₀) z - 2 / (z - ↑l₀) ^ 3 = L.derivWeierstrassP z

theorem PeriodPair.derivWeierstrassPExcept_def (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ) : L.derivWeierstrassPExcept (↑l₀) z = L.derivWeierstrassP z + 2 / (z - ↑l₀) ^ 3

theorem PeriodPair.derivWeierstrassPExcept_of_notMem (L : PeriodPair) (l₀ : ℂ) (hl : l₀ ∉ L.lattice) : L.derivWeierstrassPExcept l₀ = L.derivWeierstrassP

theorem PeriodPair.hasSumLocallyUniformly_derivWeierstrassP (L : PeriodPair) : HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) => -2 / (z - ↑l) ^ 3) L.derivWeierstrassP

theorem PeriodPair.hasSum_derivWeierstrassP (L : PeriodPair) (z : ℂ) : HasSum (fun (l : ↥L.lattice) => -2 / (z - ↑l) ^ 3) (L.derivWeierstrassP z)

theorem PeriodPair.differentiableOn_derivWeierstrassP (L : PeriodPair) : DifferentiableOn ℂ L.derivWeierstrassP (↑L.lattice)ᶜ

@[simp]

theorem PeriodPair.derivWeierstrassP_neg (L : PeriodPair) (z : ℂ) : L.derivWeierstrassP (-z) = -L.derivWeierstrassP z

@[simp]

theorem PeriodPair.derivWeierstrassP_add_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.derivWeierstrassP (z + ↑l) = L.derivWeierstrassP z

theorem PeriodPair.periodic_derivWeierstrassP (L : PeriodPair) (l : ↥L.lattice) : Function.Periodic L.derivWeierstrassP ↑l

@[simp]

theorem PeriodPair.derivWeierstrassP_zero (L : PeriodPair) : L.derivWeierstrassP 0 = 0

@[simp]

theorem PeriodPair.derivWeierstrassP_coe (L : PeriodPair) (l : ↥L.lattice) : L.derivWeierstrassP ↑l = 0

@[simp]

theorem PeriodPair.derivWeierstrassP_sub_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.derivWeierstrassP (z - ↑l) = L.derivWeierstrassP z

@[simp]

theorem PeriodPair.deriv_weierstrassP (L : PeriodPair) : deriv L.weierstrassP = L.derivWeierstrassP

deriv ℘ = ℘'. This is true globally because of junk values.

noncomputable def PeriodPair.sumInvPow (L : PeriodPair) (x : ℂ) (r : ℕ) : ℂ

The sum ∑ (l - x)⁻ʳ over l ∈ L. This converges when 2 < r, see hasSum_sumInvPow.

Equations

• L.sumInvPow x r = ∑' (l : ↥L.lattice), ((↑l - x) ^ r)⁻¹

theorem PeriodPair.hasSum_sumInvPow (L : PeriodPair) (x : ℂ) {r : ℕ} (hr : 2 < r) : HasSum (fun (l : ↥L.lattice) => ((↑l - x) ^ r)⁻¹) (L.sumInvPow x r)

noncomputable def PeriodPair.weierstrassPExceptSummand (L : PeriodPair) (l₀ x : ℂ) (i : ℕ) (l : ↥L.lattice) : ℂ

In the power series expansion of ℘(z) = ∑ aᵢ (z - x)ⁱ at some x ∉ L, each aᵢ can be written as an infinite sum over l ∈ L. This is the summand of this infinite sum with the l₀-th term omitted. See PeriodPair.coeff_weierstrassPExceptSeries.

Equations

• L.weierstrassPExceptSummand l₀ x i l = if ↑l = l₀ then 0 else (↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0

noncomputable def PeriodPair.weierstrassPExceptSeries (L : PeriodPair) (l₀ x : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ

The power series expansion of ℘[L - l₀] at x. See PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.coeff_weierstrassPExceptSeries (L : PeriodPair) (l₀ x : ℂ) (i : ℕ) : (L.weierstrassPExceptSeries l₀ x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i l

theorem PeriodPair.summable_weierstrassPExceptSummand (L : PeriodPair) (l₀ z x : ℂ) (hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) : Summable (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) => L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

In the power series expansion of ℘(z) = ∑ᵢ aᵢ (z - x)ⁱ at some x ∉ L, each aᵢ can be writen as a sum over l ∈ L, i.e. aᵢ = ∑ₗ, (i + 1) * (l - x)⁻ⁱ⁻² for i ≠ 0 and a₀ = ∑ₗ, (l - x)⁻² - l⁻².

We show that the double sum converges if z falls in a ball centered at x that doesn't touch L.

theorem PeriodPair.weierstrassPExcept_eq_tsum (L : PeriodPair) (l₀ z x : ℂ) (hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) : L.weierstrassPExcept l₀ z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

theorem PeriodPair.weierstrassPExceptSeries_hasSum (L : PeriodPair) (l₀ z x : ℂ) (hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) : HasSum (fun (i : ℕ) => (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (L.weierstrassPExcept l₀ z)

theorem PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept (L : PeriodPair) (l₀ x : ℂ) (r : NNReal) (hr0 : 0 < r) (hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ) : HasFPowerSeriesOnBall (L.weierstrassPExcept l₀) (L.weierstrassPExceptSeries l₀ x) x ↑r

theorem PeriodPair.hasFPowerSeriesAt_weierstrassPExcept (L : PeriodPair) (l : ℂ) : HasFPowerSeriesAt (L.weierstrassPExcept l) (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) => if i = 0 then L.weierstrassPExcept l l else (↑i + 1) * L.sumInvPow l (i + 2)) l

theorem PeriodPair.analyticOnNhd_weierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : AnalyticOnNhd ℂ (L.weierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ

theorem PeriodPair.analyticAt_weierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : AnalyticAt ℂ (L.weierstrassPExcept l₀) l₀

theorem PeriodPair.iteratedDeriv_weierstrassPExcept_self (L : PeriodPair) (l : ℂ) {n : ℕ} : iteratedDeriv n (L.weierstrassPExcept l) l = if n = 0 then L.weierstrassPExcept l l else ↑(n + 1).factorial * L.sumInvPow l (n + 2)

noncomputable def PeriodPair.derivWeierstrassPExceptSeries (L : PeriodPair) (l₀ x : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ

The power series expansion of ℘'[L - l₀] at x. See PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept.

Equations

• L.derivWeierstrassPExceptSeries l₀ x = FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) => (↑i + 1) * (↑i + 2) * (L.sumInvPow x (i + 3) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 3))⁻¹ else 0)

theorem PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept (L : PeriodPair) (l₀ x : ℂ) (r : NNReal) (hr0 : 0 < r) (hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ) : HasFPowerSeriesOnBall (L.derivWeierstrassPExcept l₀) (L.derivWeierstrassPExceptSeries l₀ x) x ↑r

theorem PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept (L : PeriodPair) (l : ℂ) : HasFPowerSeriesAt (L.derivWeierstrassPExcept l) (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) => (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3)) l

theorem PeriodPair.analyticOnNhd_derivWeierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : AnalyticOnNhd ℂ (L.derivWeierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ

theorem PeriodPair.analyticAt_derivWeierstrassPExcept (L : PeriodPair) (l₀ : ℂ) : AnalyticAt ℂ (L.derivWeierstrassPExcept l₀) l₀

theorem PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self (L : PeriodPair) (l : ℂ) {n : ℕ} : iteratedDeriv n (L.derivWeierstrassPExcept l) l = ↑(n + 2).factorial * L.sumInvPow l (n + 3)

@[simp]

theorem PeriodPair.deriv_derivWeierstrassPExcept_self (L : PeriodPair) (l : ℂ) : deriv (L.derivWeierstrassPExcept l) l = 6 * L.sumInvPow l 4

theorem PeriodPair.analyticOnNhd_derivWeierstrassP (L : PeriodPair) : AnalyticOnNhd ℂ L.derivWeierstrassP (↑L.lattice)ᶜ

noncomputable def PeriodPair.weierstrassPSummand (L : PeriodPair) (x : ℂ) (i : ℕ) (l : ↥L.lattice) : ℂ

In the power series expansion of ℘(z) = ∑ aᵢzⁱ at some x ∉ L, each aᵢ can be written as an infinite sum over l ∈ L. This is the summand of this infinite sum. See PeriodPair.coeff_weierstrassPSeries.

Equations

• L.weierstrassPSummand x i l = (↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0

noncomputable def PeriodPair.weierstrassPSeries (L : PeriodPair) (x : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ

The power series expansion of ℘ at x. See PeriodPair.hasFPowerSeriesOnBall_weierstrassP.

Equations

• L.weierstrassPSeries x = FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) => if i = 0 then L.weierstrassP x else (↑i + 1) * L.sumInvPow x (i + 2)

theorem PeriodPair.weierstrassPExceptSeries_of_notMem (L : PeriodPair) (l₀ : ℂ) (hl₀ : l₀ ∉ L.lattice) : L.weierstrassPExceptSeries l₀ = L.weierstrassPSeries

theorem PeriodPair.weierstrassPExceptSummand_of_notMem (L : PeriodPair) (l₀ : ℂ) (hl₀ : l₀ ∉ L.lattice) : L.weierstrassPExceptSummand l₀ = L.weierstrassPSummand

theorem PeriodPair.coeff_weierstrassPSeries (L : PeriodPair) (x : ℂ) (i : ℕ) : (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l

theorem PeriodPair.summable_weierstrassPSummand (L : PeriodPair) (z x : ℂ) (hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖) : Summable (Function.uncurry fun (b : ℕ) (c : ↥L.lattice) => L.weierstrassPSummand x b c * (z - x) ^ b)

theorem PeriodPair.weierstrassPSeries_hasSum (L : PeriodPair) (z x : ℂ) (hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖) : HasSum (fun (i : ℕ) => (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (L.weierstrassP z)

theorem PeriodPair.hasFPowerSeriesOnBall_weierstrassP (L : PeriodPair) (x : ℂ) (r : NNReal) (hr0 : 0 < r) (hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ) : HasFPowerSeriesOnBall L.weierstrassP (L.weierstrassPSeries x) x ↑r

theorem PeriodPair.analyticOnNhd_weierstrassP (L : PeriodPair) : AnalyticOnNhd ℂ L.weierstrassP (↑L.lattice)ᶜ

theorem PeriodPair.ite_eq_one_sub_sq_mul_weierstrassP (L : PeriodPair) (l₀ : ℂ) (hl₀ : l₀ ∈ L.lattice) (z : ℂ) : (if z = l₀ then 1 else (z - l₀) ^ 2 * L.weierstrassP z) = (z - l₀) ^ 2 * L.weierstrassPExcept l₀ z + 1 - (z - l₀) ^ 2 / l₀ ^ 2

theorem PeriodPair.meromorphic_weierstrassP (L : PeriodPair) : Meromorphic L.weierstrassP

theorem PeriodPair.meromorphic_derivWeierstrassP (L : PeriodPair) : Meromorphic L.derivWeierstrassP

theorem PeriodPair.order_weierstrassP (L : PeriodPair) (l₀ : ℂ) (h : l₀ ∈ L.lattice) : meromorphicOrderAt L.weierstrassP l₀ = -2

noncomputable def PeriodPair.G (L : PeriodPair) (n : ℕ) : ℂ

The Eisenstein series as a function on lattices. It takes L to the sum ∑ l⁻ʳ over l ∈ L. TODO: Establish connections with the ModularForm library.

Equations

• L.G n = ∑' (l : ↥L.lattice), (↑l ^ n)⁻¹

@[simp]

theorem PeriodPair.sumInvPow_zero (L : PeriodPair) : L.sumInvPow 0 = L.G

theorem PeriodPair.G_eq_zero_of_odd (L : PeriodPair) (n : ℕ) (hn : Odd n) : L.G n = 0

noncomputable def PeriodPair.g₂ (L : PeriodPair) : ℂ

The lattice invariant g₂ := 60 G₄.

Equations

• L.g₂ = 60 * L.G 4

noncomputable def PeriodPair.g₃ (L : PeriodPair) : ℂ

The lattice invariant g₃ := 140 G₆.

Equations

• L.g₃ = 140 * L.G 6

theorem PeriodPair.derivWeierstrassP_sq (L : PeriodPair) (z : ℂ) (hz : z ∉ L.lattice) : L.derivWeierstrassP z ^ 2 = 4 * L.weierstrassP z ^ 3 - L.g₂ * L.weierstrassP z - L.g₃

℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃