[Merged by Bors] - feat(NumberTheory/ModularForms): the Dedekind Eta function

Mathlib.lean

@@ -4742,6 +4742,7 @@ import Mathlib.NumberTheory.MaricaSchoenheim
 import Mathlib.NumberTheory.Modular
 import Mathlib.NumberTheory.ModularForms.Basic
 import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
+import Mathlib.NumberTheory.ModularForms.DedekindEta
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Mathlib/Analysis/Complex/Periodic.lean

@@ -72,6 +72,19 @@ theorem norm_qParam_lt_iff (hh : 0 < h) (A : ℝ) (z : ℂ) :
   rw [norm_qParam, Real.exp_lt_exp, div_lt_div_iff_of_pos_right hh, mul_lt_mul_left_of_neg]
   simpa using Real.pi_pos
 
+lemma qParam_ne_zero (z : ℂ) : 𝕢 h z ≠ 0 := by
+  simp [qParam, exp_ne_zero]
+
+@[fun_prop]
+lemma differentiable_qParam : Differentiable ℂ (𝕢 h) := by
+    unfold qParam
+    fun_prop
+
+@[fun_prop]
+lemma contDiff_qParam (m : WithTop ℕ∞) : ContDiff ℂ m (𝕢 h) := by
+    unfold qParam
+    fun_prop
+
 @[deprecated (since := "2025-02-17")] alias abs_qParam_lt_iff := norm_qParam_lt_iff
 
 theorem qParam_tendsto (hh : 0 < h) : Tendsto (qParam h) I∞ (𝓝[≠] 0) := by

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -203,5 +203,16 @@ theorem vadd_im : (x +ᵥ z).im = z.im :=
   zero_add _
 
 end RealAddAction
+section upperHalfPlaneSet
+
+/-- The upper half plane as a subset of `ℂ`. This is convenient for taking derivatives of functions
+on the upper half plane. -/
+abbrev upperHalfPlaneSet := {z : ℂ | 0 < z.im}
+
+local notation "ℍₒ" => upperHalfPlaneSet
+
+lemma isOpen_upperHalfPlaneSet : IsOpen ℍₒ := isOpen_lt continuous_const Complex.continuous_im
+
+end upperHalfPlaneSet
 
 end UpperHalfPlane

Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

@@ -70,7 +70,7 @@ lemma mdifferentiable_iff {f : ℍ → ℂ} :
     MDifferentiable 𝓘(ℂ) 𝓘(ℂ) f ↔ DifferentiableOn ℂ (f ∘ ofComplex) {z | 0 < z.im} :=
   ⟨fun h z hz ↦ (mdifferentiableAt_iff.mp (h ⟨z, hz⟩)).differentiableWithinAt,
     fun h ⟨z, hz⟩ ↦ mdifferentiableAt_iff.mpr <| (h z hz).differentiableAt
-      <| (Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hz⟩
+     <| isOpen_upperHalfPlaneSet.mem_nhds hz⟩
 
 lemma contMDiff_num (g : GL (Fin 2) ℝ) : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (fun τ : ℍ ↦ num g τ) :=
   (contMDiff_const.smul contMDiff_coe).add contMDiff_const

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -28,7 +28,7 @@ instance : TopologicalSpace ℍ :=
   instTopologicalSpaceSubtype
 
 theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℍ → ℂ) :=
-  IsOpen.isOpenEmbedding_subtypeVal <| isOpen_lt continuous_const Complex.continuous_im
+  IsOpen.isOpenEmbedding_subtypeVal <| isOpen_upperHalfPlaneSet
 
 theorem isEmbedding_coe : IsEmbedding ((↑) : ℍ → ℂ) :=
   IsEmbedding.subtypeVal
@@ -168,7 +168,7 @@ lemma comp_ofComplex_of_im_le_zero (f : ℍ → ℂ) (z z' : ℂ) (hz : z.im ≤
 
 lemma eventuallyEq_coe_comp_ofComplex {z : ℂ} (hz : 0 < z.im) :
     UpperHalfPlane.coe ∘ ofComplex =ᶠ[𝓝 z] id := by
-  filter_upwards [(Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hz] with x hx
+  filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds hz] with x hx
   simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq, coe_mk_subtype]
 
 end ofComplex

Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

@@ -173,4 +173,22 @@ lemma multipliable_one_add_of_summable [CompleteSpace R]
   · intro x hx y hy
     exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)
 
+lemma Summable.summable_log_norm_one_add (hu : Summable fun n ↦ ‖f n‖) :
+    Summable fun i ↦ Real.log ‖1 + f i‖ := by
+  suffices Summable (‖1 + f ·‖ - 1) from
+    (Real.summable_log_one_add_of_summable this).congr (by simp)
+  refine .of_norm (hu.of_nonneg_of_le (fun i ↦ by positivity) fun i ↦ ?_)
+  simp only [Real.norm_eq_abs, abs_le]
+  constructor
+  · simpa using norm_add_le (1 + f i) (-f i)
+  · simpa [add_comm] using norm_add_le (f i) 1
+
+lemma tprod_one_add_ne_zero_of_summable [CompleteSpace R] [NormMulClass R]
+    (hf : ∀ i, 1 + f i ≠ 0)
+    (hu : Summable (‖f ·‖)) : ∏' i : ι, (1 + f i) ≠ 0 := by
+  rw [← norm_ne_zero_iff, Multipliable.norm_tprod]
+  · rw [← Real.rexp_tsum_eq_tprod (fun i ↦ norm_pos_iff.mpr <| hf i) hu.summable_log_norm_one_add]
+    apply Real.exp_ne_zero
+  · exact multipliable_one_add_of_summable hu
+
 end NormedRing

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -80,7 +80,7 @@ private lemma MDifferentiable.slashJ {f : ℍ → ℂ} (hf : MDifferentiable 
     simp [ofComplex_apply_of_im_pos hz]
   refine .congr (fun z hz ↦ DifferentiableAt.differentiableWithinAt ?_) this
   have : 0 < (-conj z).im := by simpa using hz
-  have := hf.differentiableAt ((Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds this)
+  have := hf.differentiableAt (isOpen_upperHalfPlaneSet.mem_nhds this)
   simpa using (this.comp _ differentiable_neg.differentiableAt).star_star.neg
 
 /-- The weight `k` slash action of `GL(2, ℝ)` preserves holomorphic functions. -/

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2024 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck, David Loeffler
+-/
+
+import Mathlib.Analysis.Complex.LocallyUniformLimit
+import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
+import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+
+/-!
+# Dedekind eta function
+
+## Main definitions
+
+* We define the Dedekind eta function as the infinite product
+`η(z) = q ^ 1/24 * ∏' (1 - q ^ (n + 1))` where `q = e ^ (2πiz)` and `z` is in the upper half-plane.
+The product is taken over all non-negative integers `n`. We then show it is non-vanishing and
+differentiable on the upper half-plane.
+
+## References
+* [F. Diamond and J. Shurman, *A First Course in Modular Forms*][diamondshurman2005]
+-/
+
+open TopologicalSpace Set MeasureTheory intervalIntegral
+ Metric Filter Function Complex
+
+open UpperHalfPlane hiding I
+
+open scoped Interval Real NNReal ENNReal Topology BigOperators Nat
+
+local notation "𝕢" => Periodic.qParam
+
+local notation "ℍₒ" => upperHalfPlaneSet
+
+namespace ModularForm
+
+/-- The q term inside the product defining the eta function. It is defined as
+`eta_q n z = e ^ (2 π i (n + 1) z)`. -/
+noncomputable abbrev eta_q (n : ℕ) (z : ℂ) := (𝕢 1 z) ^ (n + 1)
+
+lemma eta_q_eq_cexp (n : ℕ) (z : ℂ) : eta_q n z = cexp (2 * π * I * (n + 1) * z) := by
+  simp [eta_q, Periodic.qParam, ← Complex.exp_nsmul]
+  ring_nf
+
+lemma eta_q_eq_pow (n : ℕ) (z : ℂ) : eta_q n z = cexp (2 * π * I * z) ^ (n + 1) := by
+  simp [eta_q, Periodic.qParam]
+
+lemma one_sub_eta_q_ne_zero (n : ℕ) {z : ℂ} (hz : z ∈ ℍₒ) : 1 - eta_q n z ≠ 0 := by
+  rw [eta_q_eq_cexp, sub_ne_zero]
+  intro h
+  simpa [← mul_assoc, ← h] using norm_exp_two_pi_I_lt_one ⟨(n + 1) • z, by
+    simpa [(show 0 < (n + 1 : ℝ) by positivity)] using hz⟩
+
+/-- The eta function, whose value at z is `q^ 1 / 24 * ∏' 1 - q ^ (n + 1)` for `q = e ^ 2 π i z`. -/
+noncomputable def eta (z : ℂ) := 𝕢 24 z * ∏' (n : ℕ), (1 - eta_q n z)
+
+local notation "η" => ModularForm.eta
+
+open ModularForm
+
+theorem summable_eta_q (z : ℍ) : Summable fun n ↦ ‖-eta_q n z‖ := by
+  simp [eta_q, eta_q_eq_pow, summable_nat_add_iff 1, norm_exp_two_pi_I_lt_one z]
+
+lemma multipliableLocallyUniformlyOn_eta :
+    MultipliableLocallyUniformlyOn (fun n a ↦ 1 - eta_q n a) ℍₒ:= by
+  use fun z => ∏' (n : ℕ), (1 - eta_q n z)
+  simp_rw [sub_eq_add_neg]
+  apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_upperHalfPlaneSet
+  intro K hK hcK
+  by_cases hN : K.Nonempty
+  · have hc : ContinuousOn (fun x ↦ ‖cexp (2 * π * I * x)‖) K := by fun_prop
+    obtain ⟨z, hz, hB, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN hc
+    apply (summable_eta_q ⟨z, hK hz⟩).hasProdUniformlyOn_nat_one_add hcK
+    · filter_upwards with n x hx
+      simpa [eta_q, eta_q_eq_pow n x, eta_q_eq_pow n (⟨z, hK hz⟩ : ℍₒ)] using
+          pow_le_pow_left₀ (by simp [norm_nonneg]) (HB x hx) (n + 1)
+    · simp_rw [eta_q, Periodic.qParam]
+      fun_prop
+  · rw [hasProdUniformlyOn_iff_tendstoUniformlyOn]
+    simpa [not_nonempty_iff_eq_empty.mp hN] using tendstoUniformlyOn_empty
+
+-- Eta is non-vanishing on the upper half plane. -/
+lemma eta_ne_zero {z : ℂ} (hz : z ∈ ℍₒ) : η z ≠ 0 := by
+  apply mul_ne_zero (Periodic.qParam_ne_zero z)
+  simp only [eta_q, ne_eq]
+  refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z)  ?_ ?_
+  · refine fun i ↦ by simpa using one_sub_eta_q_ne_zero i hz
+  · simpa [eta_q, ← summable_norm_iff] using summable_eta_q ⟨z, hz⟩
+
+lemma logDeriv_one_sub_cexp (r : ℂ) : logDeriv (fun z ↦ 1 - r * cexp z) =
+    fun z ↦ -r * cexp z / (1 - r * cexp z) := by
+  ext z
+  simp [logDeriv]
+
+lemma logDeriv_one_sub_mul_cexp_comp (r : ℂ) {g : ℂ → ℂ} (hg : Differentiable ℂ g) :
+    logDeriv ((fun z ↦ 1 - r * cexp z) ∘ g) =
+    fun z ↦ -r * (deriv g z) * cexp (g z) / (1 - r * cexp (g z)) := by
+  ext y
+  rw [logDeriv_comp (by fun_prop) (hg y), logDeriv_one_sub_cexp]
+  ring
+
+private theorem one_sub_eta_logDeriv_eq (z : ℂ) (n : ℕ) : logDeriv (fun x ↦ 1 - eta_q n x) z =
+    2 * π * I * (n + 1) * -eta_q n z / (1 - eta_q n z) := by
+  have h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (n + 1) * x)) =
+      ((fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (n + 1) * x) := by aesop
+  have h3 : deriv (fun x : ℂ ↦ (2 * π * I * (n + 1) * x)) =
+      fun _ ↦ 2 * π * I * (n + 1) := by
+    ext y
+    simpa using deriv_const_mul (2 * π * I * (n + 1)) (d := fun (x : ℂ) ↦ x) (x := y)
+  simp_rw [eta_q_eq_cexp, h2, logDeriv_one_sub_mul_cexp_comp 1
+    (g := fun x ↦ (2 * π * I * (n + 1) * x)) (by fun_prop), h3]
+  simp
+
+lemma tsum_log_deriv_eta_q (z : ℂ) : ∑' n, logDeriv (fun x ↦ 1 - eta_q n x) z =
+    (2 * π * I) * ∑' n, (n + 1) * (-eta_q n z) / (1 - eta_q n z) := by
+  have : ∑' i, logDeriv (fun x ↦ 1 - eta_q i x) z =
+      ∑' n, (2 * ↑π * I * (n + 1)) * (-eta_q n z) / (1 - eta_q n z) :=
+    tsum_congr (fun i ↦ one_sub_eta_logDeriv_eq z i)
+  rw [this, ← tsum_mul_left]
+  grind
+
+theorem differentiableAt_eta_of_mem_upperHalfPlaneSet {z : ℂ} (hz : z ∈ ℍₒ) :
+    DifferentiableAt ℂ eta z := by
+  apply DifferentiableAt.mul (by fun_prop)
+  have hD := (MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn
+    multipliableLocallyUniformlyOn_eta).tendstoLocallyUniformlyOn_finsetRange.differentiableOn ?_
+    isOpen_upperHalfPlaneSet
+  · exact (hD z hz).differentiableAt (isOpen_upperHalfPlaneSet.mem_nhds hz)
+  · filter_upwards with b y
+    apply (DifferentiableOn.finset_prod (u := Finset.range b) (f := fun i x ↦ 1 - eta_q i x)
+      (by fun_prop)).congr
+    simp
+
+end ModularForm

Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

@@ -52,11 +52,9 @@ theorem eisensteinSeries_SIF_MDifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k)
   suffices DifferentiableAt ℂ (↑ₕeisensteinSeries_SIF a k) τ.1 by
     convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
     exact funext fun z ↦ (comp_ofComplex (eisensteinSeries_SIF a k) z).symm
-  refine DifferentiableOn.differentiableAt ?_
-    ((isOpen_lt continuous_const Complex.continuous_im).mem_nhds τ.2)
+  refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)
   exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
     (Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum
-      fun _ _ ↦ eisSummand_extension_differentiableOn _ _)
-        (isOpen_lt continuous_const continuous_im)
+    fun _ _ ↦ eisSummand_extension_differentiableOn _ _) isOpen_upperHalfPlaneSet
 
 end EisensteinSeries