diff --git a/Mathlib/Analysis/Complex/IntegerCompl.lean b/Mathlib/Analysis/Complex/IntegerCompl.lean index 1ecb6481971d12..d8064ad29a9bb5 100644 --- a/Mathlib/Analysis/Complex/IntegerCompl.lean +++ b/Mathlib/Analysis/Complex/IntegerCompl.lean @@ -49,4 +49,10 @@ lemma integerComplement_pow_two_ne_pow_two {x : ℂ} (hx : x ∈ ℂ_ℤ) (n : have := not_exists.mp hx (-n) simp_all [sq_eq_sq_iff_eq_or_eq_neg, eq_comm] +lemma upperHalfPlane_inter_integerComplement : + {z : ℂ | 0 < z.im} ∩ ℂ_ℤ = {z : ℂ | 0 < z.im} := by + ext z + simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_iff_left_iff_imp] + exact fun hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩ + end Complex diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean index 2764779fab9b68..45e8c84d47c395 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Chris Birkbeck. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Birkbeck -/ +import Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow import Mathlib.Analysis.Complex.UpperHalfPlane.Exp import Mathlib.Analysis.Complex.IntegerCompl import Mathlib.Analysis.Complex.LocallyUniformLimit @@ -10,6 +11,7 @@ import Mathlib.Analysis.PSeries import Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable +import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn /-! # Cotangent @@ -18,13 +20,17 @@ This file contains lemmas about the cotangent function, including useful series In particular, we prove that `π * cot (π * z) = π * I - 2 * π * I * ∑' n : ℕ, Complex.exp (2 * π * I * z) ^ n` as well as the infinite sum representation of cotangent (also known as the Mittag-Leffler -expansion): `π * cot (π * z) = 1 / z + ∑' n : ℕ+, (1 / ((z : ℂ) - n) + 1 / (z + n))`. +expansion): `π * cot (π * z) = 1 / z + ∑' n : ℕ+, (1 / (z - n) + 1 / (z + n))`. -/ open Real Complex open scoped UpperHalfPlane +local notation "ℂ_ℤ" => integerComplement + +local notation "ℍₒ" => UpperHalfPlane.upperHalfPlaneSet + lemma Complex.cot_eq_exp_ratio (z : ℂ) : cot z = (Complex.exp (2 * I * z) + 1) / (I * (1 - Complex.exp (2 * I * z))) := by rw [Complex.cot, Complex.sin, Complex.cos] @@ -63,8 +69,6 @@ open Filter Function open scoped Topology BigOperators Nat Complex -local notation "ℂ_ℤ" => integerComplement - variable {x : ℂ} {Z : Set ℂ} /-- The main term in the infinite product for sine. -/ @@ -77,14 +81,14 @@ lemma sineTerm_ne_zero {x : ℂ} (hx : x ∈ ℂ_ℤ) (n : ℕ) : 1 + sineTerm x aesop · simp [Nat.cast_add_one_ne_zero n] -theorem tendsto_euler_sin_prod' (h0 : x ≠ 0) : +lemma tendsto_euler_sin_prod' (h0 : x ≠ 0) : Tendsto (fun n : ℕ ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop (𝓝 (sin (π * x) / (π * x))) := by rw [show (sin (π * x) / (π * x)) = sin (π * x) * (1 / (π * x)) by ring] apply (Filter.Tendsto.mul_const (b := 1 / (π * x)) (tendsto_euler_sin_prod x)).congr exact fun n ↦ by field_simp; rfl -theorem multipliable_sineTerm (x : ℂ) : Multipliable fun i ↦ (1 + sineTerm x i) := by +lemma multipliable_sineTerm (x : ℂ) : Multipliable fun i ↦ (1 + sineTerm x i) := by apply multipliable_one_add_of_summable have := summable_pow_div_add (x ^ 2) 2 1 Nat.one_lt_two simpa [sineTerm] using this @@ -108,46 +112,52 @@ private lemma sineTerm_bound_aux (hZ : IsCompact Z) : gcongr apply le_trans (hs x hx) (le_abs_self s) -theorem multipliableUniformlyOn_euler_sin_prod_on_compact (hZC : IsCompact Z) : +lemma multipliableUniformlyOn_euler_sin_prod_on_compact (hZC : IsCompact Z) : MultipliableUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) {Z} := by obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_ · filter_upwards with n z hz using hu2 n z hz · fun_prop -theorem HasProdUniformlyOn_sineTerm_prod_on_compact (hZ2 : Z ⊆ ℂ_ℤ) +lemma HasProdUniformlyOn_sineTerm_prod_on_compact (hZ2 : Z ⊆ ℂ_ℤ) (hZC : IsCompact Z) : HasProdUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) (fun x => (Complex.sin (↑π * x) / (↑π * x))) {Z} := by apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right exact fun s hs x hx => euler_sineTerm_tprod (by aesop) -theorem HasProdLocallyUniformlyOn_euler_sin_prod : +lemma HasProdLocallyUniformlyOn_euler_sin_prod : HasProdLocallyUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) (fun x => (Complex.sin (π * x) / (π * x))) ℂ_ℤ := by apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_compl_range_intCast exact fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC -theorem sin_pi_z_ne_zero (hz : x ∈ ℂ_ℤ) : Complex.sin (π * x) ≠ 0 := by +/-- `sin π z` is non vanishing on the complement of the integers in `ℂ`. -/ +theorem sin_pi_mul_ne_zero (hx : x ∈ ℂ_ℤ) : Complex.sin (π * x) ≠ 0 := by apply Complex.sin_ne_zero_iff.2 intro k nth_rw 2 [mul_comm] exact Injective.ne (mul_right_injective₀ (ofReal_ne_zero.mpr Real.pi_ne_zero)) (by aesop) -theorem tendsto_logDeriv_euler_sin_div (hx : x ∈ ℂ_ℤ) : +lemma cot_pi_mul_contDiffWithinAt (k : ℕ∞) (hx : x ∈ ℂ_ℤ) : + ContDiffWithinAt ℂ k (fun x ↦ (↑π * x).cot) ℍₒ x := by + simp_rw [Complex.cot, Complex.cos, Complex.sin] + exact ContDiffWithinAt.div (by fun_prop) (by fun_prop) (sin_pi_mul_ne_zero hx) + +lemma tendsto_logDeriv_euler_sin_div (hx : x ∈ ℂ_ℤ) : Tendsto (fun n : ℕ ↦ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop (𝓝 <| logDeriv (fun t ↦ (Complex.sin (π * t) / (π * t))) x) := by refine logDeriv_tendsto (isOpen_compl_range_intCast) ⟨x, hx⟩ HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_ · filter_upwards with n using by fun_prop · simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or] - exact ⟨sin_pi_z_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩ + exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩ -theorem logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) : +lemma logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) : logDeriv (fun t ↦ (Complex.sin (π * t) / (π * t))) x = π * cot (π * x) - 1 / x := by have : (fun t ↦ (Complex.sin (π * t)/ (π * t))) = fun z ↦ (Complex.sin ∘ fun t ↦ π * t) z / (π * z) := by simp - rw [this, logDeriv_div _ (by apply sin_pi_z_ne_zero hz) ?_ + rw [this, logDeriv_div _ (by apply sin_pi_mul_ne_zero hz) ?_ (DifferentiableAt.comp _ (Complex.differentiableAt_sin) (by fun_prop)) (by fun_prop), logDeriv_comp (Complex.differentiableAt_sin) (by fun_prop), Complex.logDeriv_sin, deriv_const_mul _ (by fun_prop), deriv_id'', logDeriv_const_mul, logDeriv_id'] @@ -159,7 +169,7 @@ theorem logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) : /-- The term in the infinite sum expansion of cot. -/ noncomputable abbrev cotTerm (x : ℂ) (n : ℕ) : ℂ := 1 / (x - (n + 1)) + 1 / (x + (n + 1)) -theorem logDeriv_sineTerm_eq_cotTerm (hx : x ∈ ℂ_ℤ) (i : ℕ) : +lemma logDeriv_sineTerm_eq_cotTerm (hx : x ∈ ℂ_ℤ) (i : ℕ) : logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i := by have h1 := integerComplement_add_ne_zero hx (i + 1) have h2 : ((x : ℂ) - (i + 1)) ≠ 0 := by @@ -182,7 +192,7 @@ lemma logDeriv_prod_sineTerm_eq_sum_cotTerm (hx : x ∈ ℂ_ℤ) (n : ℕ) : · exact fun i _ ↦ sineTerm_ne_zero hx i · fun_prop -theorem tendsto_logDeriv_euler_cot_sub (hx : x ∈ ℂ_ℤ) : +lemma tendsto_logDeriv_euler_cot_sub (hx : x ∈ ℂ_ℤ) : Tendsto (fun n : ℕ => ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 <| π * cot (π * x)- 1 / x) := by simp_rw [← logDeriv_sin_div_eq_cot hx, ← logDeriv_prod_sineTerm_eq_sum_cotTerm hx] @@ -196,7 +206,7 @@ lemma cotTerm_identity (hz : x ∈ ℂ_ℤ) (n : ℕ) : · simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hz (-(n + 1) : ℤ) · simpa using (integerComplement_add_ne_zero hz ((n : ℤ) + 1)) -theorem Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n := by +lemma Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n := by rw [funext fun n ↦ cotTerm_identity hz n] apply Summable.mul_left suffices Summable fun i : ℕ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by @@ -207,7 +217,7 @@ theorem Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n : apply (EisensteinSeries.summable_linear_sub_mul_linear_add x 1 1).congr simp [mul_comm] -theorem cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x = +lemma cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x = ∑' n : ℕ, (1 / (x - (n + 1)) + 1 / (x + (n + 1))) := by rw [HasSum.tsum_eq] apply (Summable.hasSum_iff_tendsto_nat (Summable_cotTerm hz)).mpr @@ -223,3 +233,171 @@ theorem cot_series_rep (hz : x ∈ ℂ_ℤ) : ring end MittagLeffler + +section iteratedDeriv + +open Set UpperHalfPlane + +open scoped Nat + +variable (k : ℕ) + +private lemma contDiffOn_inv_linear (d : ℤ) : ContDiffOn ℂ k (fun z : ℂ ↦ 1 / (z + d)) ℂ_ℤ := by + simpa using ContDiffOn.inv (by fun_prop) (fun x hx ↦ integerComplement_add_ne_zero hx d) + +lemma eqOn_iteratedDeriv_cotTerm (d : ℕ) : EqOn (iteratedDeriv k (fun z ↦ cotTerm z d)) + (fun z ↦ (-1)^ k * k ! * ((z + (d + 1))^ (-1 - k : ℤ) + (z - (d + 1)) ^ (-1 - k : ℤ))) ℂ_ℤ := by + intro z hz + rw [← Pi.add_def, iteratedDeriv_add] + · have h2 := iter_deriv_inv_linear_sub k 1 ((d + 1 : ℂ)) + have h3 := iter_deriv_inv_linear k 1 (d + 1 : ℂ) + simp only [one_div, one_mul, one_pow, mul_one, Int.reduceNeg, iteratedDeriv_eq_iterate] at * + rw [h2, h3] + ring + · simpa [sub_eq_add_neg] using (contDiffOn_inv_linear k (-(d + 1))).contDiffAt + ((isOpen_compl_range_intCast).mem_nhds hz) + · simpa using (contDiffOn_inv_linear k (d + 1)).contDiffAt + ((isOpen_compl_range_intCast).mem_nhds hz) + +lemma eqOn_iteratedDerivWithin_cotTerm_integerComplement (d : ℕ) : + EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℂ_ℤ) + (fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) + + (z - (d + 1)) ^ (-1 - k : ℤ))) ℂ_ℤ := by + apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen isOpen_compl_range_intCast) + exact eqOn_iteratedDeriv_cotTerm .. + +lemma eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet (d : ℕ) : + EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℍₒ) + (fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) + + (z - (d + 1)) ^ (-1 - k : ℤ))) ℍₒ := by + apply Set.EqOn.trans (upperHalfPlane_inter_integerComplement ▸ + iteratedDerivWithin_congr_right_of_isOpen (fun z ↦ cotTerm z d) k + isOpen_upperHalfPlaneSet (isOpen_compl_range_intCast)) + intro z hz + simpa using eqOn_iteratedDerivWithin_cotTerm_integerComplement k d + (coe_mem_integerComplement ⟨z, hz⟩) + +open EisensteinSeries in +private noncomputable abbrev cotTermUpperBound (A B : ℝ) (hB : 0 < B) (a : ℕ) := + k ! * (2 * (r (⟨⟨A, B⟩, by simp [hB]⟩) ^ (-1 - k : ℤ)) * ‖((a + 1) ^ (-1 - k : ℤ) : ℝ)‖) + +private lemma summable_cotTermUpperBound (A B : ℝ) (hB : 0 < B) {k : ℕ} (hk : 1 ≤ k) : + Summable fun a : ℕ ↦ cotTermUpperBound k A B hB a := by + simp_rw [← mul_assoc] + apply Summable.mul_left + conv => enter [1, n]; rw [show (-1 - k : ℤ) = -(1 + k :) by omega, zpow_neg, zpow_natCast]; + enter [1, 1, 1]; norm_cast + rw [summable_norm_iff, summable_nat_add_iff (f := fun n : ℕ ↦ ((n : ℝ) ^ (1 + k))⁻¹)] + exact summable_nat_pow_inv.mpr <| by omega + +open EisensteinSeries in +private lemma iteratedDerivWithin_cotTerm_bounded_uniformly + {k : ℕ} (hk : 1 ≤ k) {K : Set ℂ} (hK : K ⊆ ℍₒ) (A B : ℝ) (hB : 0 < B) + (HABK : inclusion hK '' univ ⊆ verticalStrip A B) (n : ℕ) {a : ℂ} (ha : a ∈ K) : + ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ a‖ ≤ cotTermUpperBound k A B hB n := by + simp only [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (hK ha), Complex.norm_mul, + norm_pow, norm_neg,norm_one, one_pow, Complex.norm_natCast, one_mul, cotTermUpperBound, + Int.reduceNeg, norm_zpow, Real.norm_eq_abs, two_mul, add_mul] + gcongr + have h1 := summand_bound_of_mem_verticalStrip (k := k + 1) (by norm_cast; omega) ![1, n + 1] hB + (z := ⟨a, (hK ha)⟩) (A := A) (by aesop) + have h2 := abs_norm_eq_max_natAbs_neg n ▸ (summand_bound_of_mem_verticalStrip (k := k + 1) + (by norm_cast; omega) ![1, -(n + 1)] hB (z := ⟨a, (hK ha)⟩) (A := A) (by aesop)) + simp only [Fin.isValue, Matrix.cons_val_zero, Int.cast_one, coe_mk_subtype, one_mul, + Matrix.cons_val_one, Matrix.cons_val_fin_one, Int.cast_add, Int.cast_natCast, neg_add_rev, + abs_norm_eq_max_natAbs, Int.reduceNeg, Int.cast_neg, sub_eq_add_neg, ge_iff_le] at h1 h2 ⊢ + refine le_trans (norm_add_le _ _) (add_le_add ?_ ?_) <;> + {simp only [Int.reduceNeg, norm_zpow]; norm_cast at h1 h2 ⊢} + +lemma summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm {k : ℕ} (hk : 1 ≤ k) : + SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ) ℍₒ := by + apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet + intro K hK hKc + obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact + ((isCompact_iff_isCompact_univ.mp hKc).image_of_continuousOn + (continuous_inclusion hK |>.continuousOn)) + exact ⟨cotTermUpperBound k A B hB, summable_cotTermUpperBound A B hB hk, + iteratedDerivWithin_cotTerm_bounded_uniformly hk hK A B hB HABK⟩ + +lemma differentiableOn_iteratedDerivWithin_cotTerm (n l : ℕ) : + DifferentiableOn ℂ (iteratedDerivWithin l (fun z ↦ cotTerm z n) ℍₒ) ℍₒ := by + suffices DifferentiableOn ℂ (fun z : ℂ ↦ (-1) ^ l * l ! * ((z + (n + 1)) ^ (-1 - l : ℤ) + + (z - (n + 1)) ^ (-1 - l : ℤ))) ℍₒ by + exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz + apply DifferentiableOn.const_mul + apply DifferentiableOn.add <;> refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_ + · simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_int ⟨x, hx⟩ (-(n + 1))).symm + · simpa [sub_eq_zero] using (UpperHalfPlane.ne_int ⟨x, hx⟩ (n + 1)) + +private lemma aux_summable_add {k : ℕ} (hk : 1 ≤ k) (x : ℂ) : + Summable fun (n : ℕ) ↦ (x + (n + 1)) ^ (-1 - k : ℤ) := by + apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp + (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by omega))).1).congr + simp [← zpow_neg, sub_eq_add_neg] + +private lemma aux_summable_sub {k : ℕ} (hk : 1 ≤ k) (x : ℂ) : + Summable fun (n : ℕ) ↦ (x - (n + 1)) ^ (-1 - k : ℤ) := by + apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp + (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by omega))).2).congr + simp [← zpow_neg, sub_eq_add_neg] + +variable {z : ℂ} + +-- We have this auxiliary ugly version on the lhs so the the rhs looks nicer. +private lemma aux_iteratedDeriv_tsum_cotTerm {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ ℍₒ) : + (-1) ^ k * (k !) * z ^ (-1 - k : ℤ) + iteratedDerivWithin k + (fun z ↦ ∑' n : ℕ, cotTerm z n) ℍₒ z = + (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ) := by + rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet hz + (fun t ht ↦ Summable_cotTerm (coe_mem_integerComplement ⟨t, ht⟩)) + (fun l hl hl2 ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm hl) + (fun n l z hl hz ↦ (differentiableOn_iteratedDerivWithin_cotTerm n l).differentiableAt + (isOpen_upperHalfPlaneSet.mem_nhds hz))] + conv => + enter [1, 2, 1, n] + rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])] + rw [tsum_of_add_one_of_neg_add_one (by simpa using aux_summable_add hk z) + (by simpa [sub_eq_add_neg] using aux_summable_sub hk z), + tsum_mul_left, Summable.tsum_add (aux_summable_add hk z) (aux_summable_sub hk z)] + push_cast + ring_nf + +lemma iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ ℍₒ) : + iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x) - 1 / x) ℍₒ z = + -(-1) ^ k * k ! * (z ^ (-1 - k : ℤ)) + (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ) := by + simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left] + refine iteratedDerivWithin_congr (fun z hz ↦ ?_) hz + simpa [cotTerm] using (cot_series_rep' (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩)) + +private lemma iteratedDerivWithin_cot_pi_mul_sub_inv {z : ℂ} (hz : z ∈ ℍₒ) : + iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x) - 1 / x) ℍₒ z = + (iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z) - + (-1) ^ k * k ! * (z ^ (-1 - k : ℤ)) := by + simp_rw [sub_eq_add_neg] + rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn] + · simpa [iteratedDerivWithin_fun_neg] using iteratedDerivWithin_one_div k + isOpen_upperHalfPlaneSet hz + · exact ContDiffWithinAt.smul (by fun_prop) (cot_pi_mul_contDiffWithinAt k + (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩)) + · simp only [one_div] + apply ContDiffWithinAt.neg + exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩) + +lemma iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ ℍₒ) : + iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z = + (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ):= by + have h0 := iteratedDerivWithin_cot_pi_mul_sub_inv k hz + rw [iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum hk hz, add_comm] at h0 + rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0] + ring + +/-- The series expansion of the iterated derivative of `π cot (π z)`. -/ +theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} + (hz : z ∈ ℍₒ) : + iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z = + (-1) ^ k * k ! * ∑' n : ℤ, 1 / (z + n) ^ (k + 1) := by + convert iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow hk hz with n + rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; omega, zpow_neg_coe_of_pos _ (by omega), + one_div] + +end iteratedDeriv diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean index 76389f1b787e14..53f41b26f042f9 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean +++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean @@ -48,6 +48,20 @@ theorem abs_le_right_of_norm (m n : ℤ) : |m| ≤ ‖![n, m]‖ := by rw [Int.abs_eq_natAbs] exact Preorder.le_refl _ +lemma abs_norm_eq_max_natAbs (n : ℕ) : + ‖![1, (n + 1 : ℤ)]‖ = n + 1 := by + simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_fin_one] + norm_cast + simp + +lemma abs_norm_eq_max_natAbs_neg (n : ℕ) : + ‖![1, -(n + 1 : ℤ)]‖ = n + 1 := by + simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_fin_one] + norm_cast + simp + section bounding_functions /-- Auxiliary function used for bounding Eisenstein series, defined as