@@ -3,17 +3,24 @@ Copyright (c) 2025 Chris Birkbeck. All rights reserved.
33Released under Apache 2.0 license as described in the file LICENSE.
44Authors: Chris Birkbeck
55-/
6- import Mathlib.NumberTheory.Divisors
7- import Mathlib.Data.PNat.Defs
6+ import Mathlib.Analysis.SpecificLimits.Normed
7+ import Mathlib.NumberTheory.ArithmeticFunction
88
99/-!
1010# Lemmas on infinite sums over the antidiagonal of the divisors function
1111
1212This file contains lemmas about the antidiagonal of the divisors function. It defines the map from
1313`Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b` to `(a, b)`.
1414
15+ We then prove some identities about the infinite sums over this antidiagonal, such as
16+ `∑' n : ℕ+, n ^ k * r ^ n / (1 - r ^ n) = ∑' n : ℕ+, σ k n * r ^ n`
17+ which are used for Eisenstein series and their q-expansions. This is also a special case of
18+ Lambert series.
19+
1520-/
1621
22+ open Filter Complex ArithmeticFunction Nat Topology
23+
1724/-- The map from `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b`
1825to `(a, b)`. -/
1926def divisorsAntidiagonalFactors (n : ℕ+) : Nat.divisorsAntidiagonal n → ℕ+ × ℕ+ := fun x ↦
@@ -48,3 +55,68 @@ lemma sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) :
4855
4956lemma sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) :
5057 (sigmaAntidiagonalEquivProd.symm x).2 = (x.1 .1 , x.2 .1 ) := rfl
58+
59+ section tsum
60+
61+ variable {𝕜 : Type *} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜]
62+
63+ omit [NormSMulClass ℤ 𝕜] in
64+ lemma summable_norm_pow_mul_geometric_div_one_sub (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1 ) :
65+ Summable fun n : ℕ ↦ n ^ k * r ^ n / (1 - r ^ n) := by
66+ simp only [div_eq_mul_one_div ( _ * _ ^ _)]
67+ apply Summable.mul_tendsto_const (c := 1 / (1 - 0 ))
68+ (by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
69+ simpa only [Nat.cofinite_eq_atTop] using
70+ tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1 ) (by simp)
71+
72+ private lemma summable_divisorsAntidiagonal_aux (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1 ) :
73+ Summable fun c : (n : ℕ+) × {x // x ∈ (n : ℕ).divisorsAntidiagonal} ↦
74+ (c.2 .1 .2 ) ^ k * (r ^ (c.2 .1 .1 * c.2 .1 .2 )) := by
75+ apply Summable.of_norm
76+ rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]
77+ constructor
78+ · exact fun n ↦ (hasSum_fintype _).summable
79+ · simp only [norm_mul, norm_pow, tsum_fintype, Finset.univ_eq_attach]
80+ apply Summable.of_nonneg_of_le (f := fun c : ℕ+ ↦ ‖(c : 𝕜) ^ (k + 1 ) * r ^ (c : ℕ)‖)
81+ (fun b ↦ Finset.sum_nonneg (fun _ _ ↦ mul_nonneg (by simp) (by simp))) (fun b ↦ ?_)
82+ (by apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1 ) hr).subtype)
83+ transitivity ∑ _ ∈ (b : ℕ).divisors, ‖(b : 𝕜)‖ ^ k * ‖r ^ (b : ℕ)‖
84+ · rw [(b : ℕ).divisorsAntidiagonal.sum_attach (fun x ↦ ‖(x.2 : 𝕜)‖ ^ _ * _ ^ (x.1 * x.2 )),
85+ sum_divisorsAntidiagonal ((fun x y ↦ ‖(y : 𝕜)‖ ^ k * _ ^ (x * y)))]
86+ gcongr with i hi
87+ · simpa using le_of_dvd b.2 (div_dvd_of_dvd (dvd_of_mem_divisors hi))
88+ · rw [norm_pow, mul_comm, Nat.div_mul_cancel (dvd_of_mem_divisors hi)]
89+ · simp only [norm_pow, Finset.sum_const, nsmul_eq_mul, ← mul_assoc, add_comm k 1 , pow_add,
90+ pow_one, norm_mul]
91+ gcongr
92+ simpa using Nat.card_divisors_le_self b
93+
94+ theorem summable_prod_mul_pow (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1 ) :
95+ Summable fun c : (ℕ+ × ℕ+) ↦ c.2 ^ k * (r ^ (c.1 * c.2 : ℕ)) := by
96+ simpa [sigmaAntidiagonalEquivProd.summable_iff.symm] using summable_divisorsAntidiagonal_aux k hr
97+
98+ theorem tsum_prod_pow_eq_tsum_sigma (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1 ) :
99+ ∑' d : ℕ+, ∑' c : ℕ+, c ^ k * r ^ (d * c : ℕ) = ∑' e : ℕ+, σ k e * r ^ (e : ℕ) := by
100+ suffices ∑' c : ℕ+ × ℕ+, c.2 ^ k * r ^ (c.1 * c.2 : ℕ) =
101+ ∑' e : ℕ+, σ k e * r ^ (e : ℕ) by rwa [← (summable_prod_mul_pow k hr).tsum_prod]
102+ simp only [← sigmaAntidiagonalEquivProd.tsum_eq, sigmaAntidiagonalEquivProd,
103+ divisorsAntidiagonalFactors, PNat.mk_coe, Equiv.coe_fn_mk, sigma_eq_sum_div, cast_sum,
104+ cast_pow, Summable.tsum_sigma (summable_divisorsAntidiagonal_aux k hr)]
105+ refine tsum_congr fun n ↦ ?_
106+ simpa [tsum_fintype, Finset.sum_mul,
107+ (n : ℕ).divisorsAntidiagonal.sum_attach fun x : ℕ × ℕ ↦ x.2 ^ k * r ^ (x.1 * x.2 ),
108+ sum_divisorsAntidiagonal fun x y ↦ y ^ k * r ^ (x * y)]
109+ using Finset.sum_congr rfl fun i hi ↦ by rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]
110+
111+ lemma tsum_pow_div_one_sub_eq_tsum_sigma {r : 𝕜} (hr : ‖r‖ < 1 ) (k : ℕ) :
112+ ∑' n : ℕ+, n ^ k * r ^ (n : ℕ) / (1 - r ^ (n : ℕ)) = ∑' n : ℕ+, σ k n * r ^ (n : ℕ) := by
113+ have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
114+ (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
115+ simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
116+ ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (fun m ↦ n ^ k * (r ^ n) ^ m)]
117+ have h00 := tsum_prod_pow_eq_tsum_sigma k hr
118+ rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
119+ rw [← h00]
120+ exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm b.val c.val, pow_mul]
121+
122+ end tsum
0 commit comments