prove a theorem

Stream: new members

[Yujie Wang]

import Mathlib

section lattice_version

variable (Λ : Submodule ℤ ℂ) [DiscreteTopology Λ] [IsZLattice ℝ Λ]

-- lattice version
noncomputable def Weierstrass_𝓟_lattice (z : ℂ) :=
  ∑' ω : Λ, if ω = 0 then 1 / z^2 else (1/(z-ω^2) - 1/ω^2)

end lattice_version

section non_lattice_version

-- non-lattice version (my guess is that is the easiest to work with)
noncomputable def Weierstrass_𝓟_basis (z ω₁ ω₂: ℂ) :=
  ∑' a : ℤ, ∑' b : ℤ, if (a = 0 ∧ b = 0) then 1 / z^2 else
    let ω := a * ω₁ + b * ω₂
    1/(z-ω^2) - 1/ω^2

end non_lattice_version

-- To prove that this sum converges if z ∉ Λ



variable (z ω₁ ω₂ : ℂ)

-- The inner sum always converges
theorem Weierstrass_𝓟_basis_converges₁ (hz : ∀ c d : ℤ, z ≠ c * ω₁ + d * ω₂) : -- assume z not in the lattice:
  ∀ (a : ℤ), Summable (fun b : ℤ ↦ if (a = 0 ∧ b = 0) then 1 / z^2 else
    let ω := a * ω₁ + b * ω₂
    1/(z-ω^2) - 1/ω^2) :=



    sorry

Hi guys, I'm trying to prove this with lean4, however I'm kinda confused what to do at first. Since I'm not very sure what the structure should be with lean. Maybe does anyone could help me or have any examples or resourses? Many thanks !

[Yujie Wang]

image.png

[Yujie Wang]

image.png

[Johan Commelin]

@Yujie Wang It looks like your question became part of the code block. Could you please edit your top post to fix the formatting?

[Johan Commelin]

Presumably @Chris Birkbeck has some ideas on what the best Lean approach here.

[Chris Birkbeck]

So I think defining it using an if in the sum might get annoying. I would define the infinite sum as an auxilary function and then just add 1/z to get your defn. As for proving the convergence, you should be able to use docs#EisensteinSeries.r to give you the upper bound you need for the M-test. Have a look at the proof of docs#EisensteinSeries.summable_norm_eisSummand

[Yujie Wang]

Thanks! let me try it