Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(ModularForms/JacobiTheta): derivative of theta function #11824

Closed
wants to merge 9 commits into from
43 changes: 12 additions & 31 deletions Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ open scoped Real BigOperators UpperHalfPlane
noncomputable def jacobiTheta (τ : ℂ) : ℂ := ∑' n : ℤ, cexp (π * I * (n : ℂ) ^ 2 * τ)
#align jacobi_theta jacobiTheta

lemma jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ := tsum_congr (by simp)
lemma jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ :=
tsum_congr (by simp [jacobiTheta₂_term])

theorem jacobiTheta_two_add (τ : ℂ) : jacobiTheta (2 + τ) = jacobiTheta τ := by
simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]
Expand All @@ -44,14 +45,13 @@ set_option linter.uppercaseLean3 false in
theorem jacobiTheta_S_smul (τ : ℍ) :
jacobiTheta ↑(ModularGroup.S • τ) = (-I * τ) ^ (1 / 2 : ℂ) * jacobiTheta τ := by
have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)
simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂]
conv_rhs => erw [← ofReal_zero, jacobiTheta₂_functional_equation 0 τ.2]
rw [zero_pow two_ne_zero, mul_zero, zero_div, Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div]
erw [div_self]
rw [one_mul, UpperHalfPlane.coe_mk, inv_neg, neg_div, one_div]
· rfl
· rw [Ne, cpow_eq_zero_iff, not_and_or]
have h1 : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
rw [Ne, cpow_eq_zero_iff, not_and_or]
exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0
simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂]
conv_rhs => erw [← ofReal_zero, jacobiTheta₂_functional_equation 0 τ]
rw [zero_pow two_ne_zero, mul_zero, zero_div, Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div,
div_self h1, one_mul, UpperHalfPlane.coe_mk, inv_neg, neg_div, one_div]
set_option linter.uppercaseLean3 false in
#align jacobi_theta_S_smul jacobiTheta_S_smul

Expand All @@ -72,30 +72,11 @@ theorem norm_exp_mul_sq_le {τ : ℂ} (hτ : 0 < τ.im) (n : ℤ) :
exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)
#align norm_exp_mul_sq_le norm_exp_mul_sq_le

theorem exists_summable_bound_exp_mul_sq {R : ℝ} (hR : 0 < R) :
∃ bd : ℤ → ℝ, Summable bd ∧ ∀ {τ : ℂ} (_ : R ≤ τ.im) (n : ℤ),
‖cexp (π * I * (n : ℂ) ^ 2 * τ)‖ ≤ bd n := by
let y := rexp (-π * R)
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hR)
refine ⟨fun n ↦ y ^ n.natAbs, .of_nat_of_neg ?_ ?_, fun hτ n ↦ ?_⟩; pick_goal 3
· refine' (norm_exp_mul_sq_le (hR.trans_le hτ) n).trans _
dsimp [y]
gcongr rexp ?_ ^ _
rwa [mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos)]
all_goals
simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using
summable_geometric_of_lt_one (Real.exp_pos _).le h
#align exists_summable_bound_exp_mul_sq exists_summable_bound_exp_mul_sq

theorem summable_exp_mul_sq {τ : ℂ} (hτ : 0 < τ.im) :
Summable fun n : ℤ => cexp (π * I * (n : ℂ) ^ 2 * τ) :=
let ⟨_, h, h'⟩ := exists_summable_bound_exp_mul_sq hτ
.of_norm_bounded _ h (h' <| le_refl _)
#align summable_exp_mul_sq summable_exp_mul_sq

theorem hasSum_nat_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
HasSum (fun n : ℕ => cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2) := by
have := (summable_exp_mul_sq hτ).hasSum.sum_nat_of_sum_int
have := hasSum_jacobiTheta₂_term 0 hτ
simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this
have := this.sum_nat_of_sum_int
rw [← hasSum_nat_add_iff' 1] at this
simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero,
Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two,
Expand Down Expand Up @@ -154,7 +135,7 @@ set_option linter.uppercaseLean3 false in
theorem differentiableAt_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
DifferentiableAt ℂ jacobiTheta τ := by
simp_rw [funext jacobiTheta_eq_jacobiTheta₂]
exact differentiableAt_jacobiTheta₂ 0 hτ
exact differentiableAt_jacobiTheta₂_snd 0 hτ
#align differentiable_at_jacobi_theta differentiableAt_jacobiTheta

theorem continuousAt_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) : ContinuousAt jacobiTheta τ :=
Expand Down