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

Mathlib.lean

@@ -4729,6 +4729,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,16 @@ 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
 
+@[fun_prop]
+lemma qParam_differentiable (n : ℝ) : Differentiable ℂ (𝕢 n) := by
+    rw [show 𝕢 n = fun x => exp (2 * π * Complex.I * x / n)  by rfl]
+    fun_prop
+
+@[fun_prop]
+lemma qParam_ContDiff (n : ℝ) (m : WithTop ℕ∞) : ContDiff ℂ m (𝕢 n) := by
+    rw [show 𝕢 n = fun x => exp (2 * π * Complex.I * x / n)  by rfl]
+    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 complexUpperHalfPlane
+
+/-- The UpperHalfPlane as a subset of `ℂ`. This is convinient for takind derivatives of functions
+on the upper half plane. -/
+abbrev complexUpperHalfPlane := {z : ℂ | 0 < z.im}
+
+local notation "ℍₒ" => complexUpperHalfPlane
+
+lemma complexUpperHalPlane_isOpen : IsOpen ℍₒ := (isOpen_lt continuous_const Complex.continuous_im)
+
+end complexUpperHalfPlane
 
 end UpperHalfPlane

Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

@@ -42,6 +42,14 @@ lemma summable_log_one_add_of_summable {f : ι → ℂ} (hf : Summable f) :
   filter_upwards [hf.norm.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi
     using norm_log_one_add_half_le_self hi
 
+lemma tprod_one_add_ne_zero_of_summable {α : Type*} (x : α) {f : ι → α → ℂ}
+    (hf : ∀ i x, 1 + f i x ≠ 0) (hu : ∀ x : α, Summable fun n => f n x) :
+    (∏' i : ι, (1 + f i) x) ≠ 0 := by
+  simp only [Pi.add_apply, Pi.one_apply, ne_eq]
+  rw [← Complex.cexp_tsum_eq_tprod (f := fun n => 1 + f n x) (fun n => hf n x)]
+  · simp only [exp_ne_zero, not_false_eq_true]
+  · exact Complex.summable_log_one_add_of_summable (hu x)
+
 protected lemma multipliable_one_add_of_summable (hf : Summable f) :
     Multipliable (fun i ↦ 1 + f i) :=
   multipliable_of_summable_log (summable_log_one_add_of_summable hf)

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

@@ -0,0 +1,143 @@
+/-
+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.Algebra.Order.Ring.Star
+import Mathlib.Analysis.CStarAlgebra.Classes
+import Mathlib.Analysis.Complex.LocallyUniformLimit
+import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
+import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+import Mathlib.Data.Complex.FiniteDimensional
+
+/-!
+# 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 UpperHalfPlane TopologicalSpace Set MeasureTheory intervalIntegral
+ Metric Filter Function Complex
+
+open scoped Interval Real NNReal ENNReal Topology BigOperators Nat
+
+local notation "𝕢" => Periodic.qParam
+
+local notation "ℍₒ" => complexUpperHalfPlane
+
+/-- 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 * π * Complex.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 * π * Complex.I * z) ^ (n + 1) := by
+  simp [eta_q, Periodic.qParam]
+
+lemma one_add_eta_q_ne_zero (n : ℕ) (z : ℍ) : 1 - eta_q n z ≠ 0 := by
+  rw [eta_q_eq_cexp, sub_ne_zero]
+  intro h
+  have := norm_exp_two_pi_I_lt_one ⟨(n + 1) • z, by
+    have : 0 < (n + 1 : ℝ) := by linarith
+    simpa [this] using z.2⟩
+  simp [← mul_assoc, ← h] at *
+
+/-- The product term in the eta function, defined as `∏' 1 - q ^ (n + 1)` for `q = e ^ 2 π i z`. -/
+noncomputable abbrev etaProdTerm (z : ℂ) := ∏' (n : ℕ), (1 - eta_q n z)
+
+local notation "ηₚ" => etaProdTerm
+
+/-- The eta function, whose value at z is `q^ 1 / 24 * ∏' 1 - q ^ (n + 1)` for `q = e ^ 2 π i z`. -/
+noncomputable def ModularForm.eta (z : ℂ) := 𝕢 24 z * ηₚ 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 hasProdLocallyUniformlyOn_eta : HasProdLocallyUniformlyOn (fun n a ↦ 1 - eta_q n a) ηₚ ℍₒ:= by
+  simp_rw [sub_eq_add_neg]
+  apply hasProdLocallyUniformlyOn_of_forall_compact complexUpperHalPlane_isOpen
+  intro K hK hcK
+  by_cases hN : K.Nonempty
+  · have hc : ContinuousOn (fun x ↦ ‖cexp (2 * π * Complex.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, by simpa using (hK hz)⟩).hasProdUniformlyOn_nat_one_add hcK
+    · filter_upwards with n x hx
+      simpa only [eta_q, eta_q_eq_pow n x, norm_neg, norm_pow, coe_mk_subtype,
+          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
+
+theorem etaProdTerm_ne_zero (z : ℍ) : ηₚ z ≠ 0 := by
+  simp only [etaProdTerm, eta_q, ne_eq]
+  refine tprod_one_add_ne_zero_of_summable z (f := fun n x ↦ -eta_q n x) ?_ ?_
+  · refine fun i x ↦ by simpa using one_add_eta_q_ne_zero i x
+  · intro x
+    simpa [eta_q, ← summable_norm_iff] using Summable_eta_q x
+
+/-- Eta is non-vanishing on the upper half plane. -/
+lemma eta_ne_zero_on_UpperHalfPlane (z : ℍ) : η z ≠ 0 := by
+  simpa [ModularForm.eta, Periodic.qParam] using etaProdTerm_ne_zero z
+
+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 : ℂ) (i : ℕ) : logDeriv (fun x ↦ 1 - eta_q i x) z =
+    2 * π * Complex.I * (i + 1) * -eta_q i z / (1 - eta_q i z) := by
+  have h2 : (fun x ↦ 1 - cexp (2 * ↑π * Complex.I * (↑i + 1) * x)) =
+      ((fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * Complex.I * (↑i + 1) * x) := by aesop
+  have h3 : deriv (fun x : ℂ ↦ (2 * π * Complex.I * (i + 1) * x)) =
+      fun _ ↦ 2 * π * Complex.I * (i + 1) := by
+    ext y
+    simpa using deriv_const_mul (2 * π * Complex.I * (i + 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 * π * Complex.I * (i + 1) * x)) (by fun_prop), h3]
+  simp
+
+lemma tsum_log_deriv_eta_q (z : ℂ) : ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) z =
+  (2 * π * Complex.I) * ∑' n : ℕ, (n + 1) * (-eta_q n z) / (1 - eta_q n z) := by
+  suffices ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) z =
+  ∑' n : ℕ, (2 * ↑π * Complex.I * (n + 1)) * (-eta_q n z) / (1 - eta_q n z) by
+    rw [this, ← tsum_mul_left]
+    congr 1
+    ext i
+    ring
+  exact tsum_congr (fun i ↦ one_sub_eta_logDeriv_eq z i)
+
+theorem etaProdTerm_differentiableAt (z : ℍ) : DifferentiableAt ℂ ηₚ z := by
+  have hD := hasProdLocallyUniformlyOn_eta.tendstoLocallyUniformlyOn_finsetRange.differentiableOn ?_
+    complexUpperHalPlane_isOpen
+  · exact (hD z z.2).differentiableAt (complexUpperHalPlane_isOpen.mem_nhds z.2)
+  · 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
+
+lemma eta_DifferentiableAt_UpperHalfPlane (z : ℍ) : DifferentiableAt ℂ eta z :=
+  DifferentiableAt.mul (by fun_prop) (etaProdTerm_differentiableAt z)