Lemmas on infinite sums over the antidiagonal of the divisors function

This file contains lemmas about the antidiagonal of the divisors function. It defines the map from Nat.divisorsAntidiagonal n to ℕ+ × ℕ+ given by sending n = a * b to (a, b).

We then prove some identities about the infinite sums over this antidiagonal, such as ∑' n : ℕ+, n ^ k * r ^ n / (1 - r ^ n) = ∑' n : ℕ+, σ k n * r ^ n which are used for Eisenstein series and their q-expansions. This is also a special case of Lambert series.

def divisorsAntidiagonalFactors (n : ℕ+) : ↥(↑n).divisorsAntidiagonal → ℕ+ × ℕ+

The map from Nat.divisorsAntidiagonal n to ℕ+ × ℕ+ given by sending n = a * b to (a, b).

theorem divisorsAntidiagonalFactors_eq {n : ℕ+} (x : ↥(↑n).divisorsAntidiagonal) : ↑(divisorsAntidiagonalFactors n x).1 * ↑(divisorsAntidiagonalFactors n x).2 = ↑n

theorem divisorsAntidiagonalFactors_one (x : ↥(Nat.divisorsAntidiagonal 1)) : divisorsAntidiagonalFactors 1 x = (1, 1)

def sigmaAntidiagonalEquivProd : (n : ℕ+) × ↥(↑n).divisorsAntidiagonal ≃ ℕ+ × ℕ+

The equivalence from the union over n of Nat.divisorsAntidiagonal n to ℕ+ × ℕ+ given by sending n = a * b to (a, b).

theorem sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) : ↑(sigmaAntidiagonalEquivProd.symm x).fst = ↑x.1 * ↑x.2

theorem sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) : ↑(sigmaAntidiagonalEquivProd.symm x).snd = (↑x.1, ↑x.2)

theorem summable_norm_pow_mul_geometric_div_one_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ↑n ^ k * r ^ n / (1 - r ^ n)

theorem summable_prod_mul_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : Summable fun (c : ℕ+ × ℕ+) => ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2)

theorem tsum_prod_pow_eq_tsum_sigma {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ k * r ^ (↑d * ↑c) = ∑' (e : ℕ+), ↑((ArithmeticFunction.sigma k) ↑e) * r ^ ↑e

theorem tsum_pow_div_one_sub_eq_tsum_sigma {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) (k : ℕ) : ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma k) ↑n) * r ^ ↑n

theorem tendsto_zero_geometric_tsum_pnat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : Filter.Tendsto (fun (m : ℕ+) => ∑' (n : ℕ+), r ^ (↑n * ↑m)) Filter.atTop (nhds 0)