Weierstrass ℘ functions

Main definitions

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

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.ω₂]

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_2

@[simp]

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

@[simp]

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

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

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

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

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.℘_bound (r : ℝ) (hr : r > 0) (s : ℂ) (hs : ‖s‖ < r) (l : ℂ) (h : 2 * r ≤ ‖l‖) : ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

def PeriodPair.℘Except (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.

Equations

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

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

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

theorem PeriodPair.differentiableOn_℘Except (L : PeriodPair) (l₀ : ℂ) : DifferentiableOn ℂ (L.℘Except l₀) (↑L.lattice \ {l₀})ᶜ

theorem PeriodPair.℘Except_neg (L : PeriodPair) (l₀ z : ℂ) : L.℘Except l₀ (-z) = L.℘Except (-l₀) z

def PeriodPair.℘ (L : PeriodPair) (z : ℂ) : ℂ

The Weierstrass ℘ function.

Equations

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

theorem PeriodPair.℘Except_add (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ) : L.℘Except (↑l₀) z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = L.℘ z

theorem PeriodPair.℘Except_def (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ) : L.℘Except (↑l₀) z = L.℘ z + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)

theorem PeriodPair.℘Except_of_notMem (L : PeriodPair) (l₀ : ℂ) (hl : l₀ ∉ L.lattice) : L.℘Except l₀ = L.℘

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

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

theorem PeriodPair.differentiableOn_℘ (L : PeriodPair) : DifferentiableOn ℂ L.℘ (↑L.lattice)ᶜ

@[simp]

theorem PeriodPair.℘_neg (L : PeriodPair) (z : ℂ) : L.℘ (-z) = L.℘ z