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.

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

theorem PeriodPair.isOpen_compl_lattice_diff (L : PeriodPair) {s : Set ℂ} : IsOpen (↑L.lattice \ 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.weierstrassP_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.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

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

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₀})ᶜ

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

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

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.