1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86

/-
This file was edited by Aristotle.

Lean Toolchain version: leanprover/lean4:v4.20.0-rc5
Mathlib version: d62eab0cc36ea522904895389c301cf8d844fd69 (May 9, 2025)

The following was proved by Aristotle:

- theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ))
-/

import Mathlib


open Finset Filter Topology

theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by
  rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)]
  intro ε εpos
  simp only [true_and, Set.mem_Ici, Set.mem_Ioo]
  -- Let's consider the sum $\sum_{b=2}^{\infty} \sum_{a=2}^{\infty} \frac{1}{b^a}$. We can rewrite this as $\sum_{b=2}^{\infty} \frac{1}{b(b-1)}$.
  have h_sum_b : ∑' (b : ℕ), ∑' (a : ℕ), (if b ≥ 2 ∧ a ≥ 2 then (1 / (b : ℝ) ^ a) else 0) = ∑' (b : ℕ), (if b ≥ 2 then (1 / (b : ℝ) * (1 / (b - 1))) else 0) := by
    refine' tsum_congr fun b => _ ; aesop;
    · -- Evaluate the inner sum $\sum_{a=2}^{\infty} \frac{1}{b^a}$.
      have h_inner : ∀ b : ℕ, 2 ≤ b → ∑' (a : ℕ), (if 2 ≤ a then (1 / (b : ℝ) ^ a) else 0) = (1 / (b : ℝ) ^ 2) / (1 - (1 / (b : ℝ))) := by
        intro b hb; erw [ div_eq_mul_inv ] ; erw [ ← tsum_geometric_of_lt_one ( by positivity ) ( by simpa using inv_lt_one_of_one_lt₀ <| Nat.one_lt_cast.mpr hb ) ] ; erw [ ← sum_add_tsum_nat_add 2 ] ; norm_num;
        · norm_num [ Finset.sum_range_succ', pow_add, tsum_mul_left ];
        · exact Summable.of_norm_bounded _ ( summable_geometric_of_lt_one ( by positivity ) ( inv_lt_one_of_one_lt₀ ( by norm_cast ) : ( b : ℝ ) ⁻¹ < 1 ) ) fun n => by split_ifs <;> norm_num;
      aesop;
      field_simp;
      rw [ div_eq_div_iff ] <;> nlinarith [ show ( b : ℝ ) ≥ 2 by norm_cast, sq ( b - 1 : ℝ ) ];
    · interval_cases b <;> norm_num;
  -- The sum $\sum_{b=2}^{\infty} \frac{1}{b(b-1)}$ is a telescoping series that converges to 1.
  have h_telescope : ∑' (b : ℕ), (if b ≥ 2 then (1 / (b : ℝ) * (1 / (b - 1))) else 0) = 1 := by
    -- We can rewrite the sum as a telescoping series.
    have h_telescope : ∀ N : ℕ, ∑ b ∈ Finset.Icc 2 (N + 1), (1 / (b : ℝ) * (1 / (b - 1))) = 1 - 1 / (N + 1) := by
      intro N; induction N <;> simp_all +decide [ Finset.sum_Ioc_succ_top, Nat.Icc_succ_left ] ; ring;
      -- Combine and simplify the terms on the left-hand side.
      field_simp
      ring;
    -- By the definition of the limit of a series, we have that if the partial sums converge to $L$, then the series converges to $L$.
    have h_limit : Filter.Tendsto (fun N : ℕ => ∑ b ∈ Finset.Icc 2 (N + 1), (1 / (b : ℝ) * (1 / (b - 1)))) Filter.atTop (nhds (∑' (b : ℕ), (if b ≥ 2 then (1 / (b : ℝ) * (1 / (b - 1))) else 0))) := by
      have h_limit : Filter.Tendsto (fun N : ℕ => ∑ b ∈ Finset.range (N + 2), (if b ≥ 2 then (1 / (b : ℝ) * (1 / (b - 1))) else 0)) Filter.atTop (nhds (∑' (b : ℕ), (if b ≥ 2 then (1 / (b : ℝ) * (1 / (b - 1))) else 0))) := by
        refine' ( Summable.hasSum _ ) |> HasSum.tendsto_sum_nat |> Filter.Tendsto.comp <| Filter.tendsto_add_atTop_nat 2;
        rw [ ← summable_nat_add_iff 2 ] ; aesop;
        field_simp;
        exact Summable.of_nonneg_of_le ( fun n => by ring_nf; positivity ) ( fun n => by rw [ div_le_div_iff ] <;> norm_num <;> ring <;> nlinarith ) ( summable_nat_add_iff 1 |>.2 <| Real.summable_one_div_nat_pow.2 one_lt_two );
      convert h_limit using 2 ; erw [ Finset.sum_Ico_eq_sub _ _ ] <;> norm_num [ Finset.sum_range_succ' ];
    exact tendsto_nhds_unique h_limit ( by simpa only [ h_telescope ] using by simpa using tendsto_const_nhds.sub ( tendsto_one_div_add_atTop_nhds_zero_nat ) );
  -- Since the partial sums of the telescoping series converge to 1, for any ε > 0, there exists an N such that for all x ≥ N, the partial sum is within ε of 1.
  have h_partial_sums : Filter.Tendsto (fun x : ℕ => ∑ a ∈ Finset.Ico 2 x, ∑ b ∈ Finset.Ico 2 x, (1 / (b : ℝ) ^ a)) Filter.atTop (nhds 1) := by
    have h_partial_sums : Filter.Tendsto (fun x : ℕ => ∑ a ∈ Finset.range x, ∑ b ∈ Finset.range x, (if b ≥ 2 ∧ a ≥ 2 then (1 / (b : ℝ) ^ a) else 0)) Filter.atTop (nhds 1) := by
      have h_partial_sums : Filter.Tendsto (fun x : ℕ => ∑ b ∈ Finset.range x, ∑ a ∈ Finset.range x, (if b ≥ 2 ∧ a ≥ 2 then (1 / (b : ℝ) ^ a) else 0)) Filter.atTop (nhds (∑' (b : ℕ), ∑' (a : ℕ), (if b ≥ 2 ∧ a ≥ 2 then (1 / (b : ℝ) ^ a) else 0))) := by
        have h_partial_sums : Summable (fun p : ℕ × ℕ => (if p.1 ≥ 2 ∧ p.2 ≥ 2 then (1 / (p.1 : ℝ) ^ p.2) else 0)) := by
          have h_abs_conv : Summable (fun p : ℕ × ℕ => (if p.1 ≥ 2 ∧ p.2 ≥ 2 then (1 / (p.1 : ℝ) ^ 2) * (1 / (p.1 : ℝ) ^ (p.2 - 2)) else 0)) := by
            have h_abs_conv : Summable (fun p : ℕ × ℕ => (if p.1 ≥ 2 ∧ p.2 ≥ 2 then (1 / (p.1 : ℝ) ^ 2) * (1 / (2 : ℝ) ^ (p.2 - 2)) else 0)) := by
              have h_abs_conv : Summable (fun p : ℕ × ℕ => (if p.1 ≥ 2 then (1 / (p.1 : ℝ) ^ 2) else 0) * (if p.2 ≥ 2 then (1 / (2 : ℝ) ^ (p.2 - 2)) else 0)) := by
                have h_abs_conv : Summable (fun p : ℕ => (if p ≥ 2 then (1 / (p : ℝ) ^ 2) else 0)) ∧ Summable (fun p : ℕ => (if p ≥ 2 then (1 / (2 : ℝ) ^ (p - 2)) else 0)) := by
                  constructor <;> norm_num [ summable_zero ];
                  · exact Summable.of_nonneg_of_le ( fun p => by positivity ) ( fun p => by aesop ) ( Real.summable_one_div_nat_pow.2 one_lt_two );
                  · rw [ ← summable_nat_add_iff 2 ] ; norm_num;
                    simpa using summable_geometric_two;
                exact .of_norm <| by simpa using Summable.mul_norm ( h_abs_conv.1.norm ) ( h_abs_conv.2.norm ) ;
              exact h_abs_conv.congr fun p => by split_ifs <;> aesop;
            refine' h_abs_conv.of_nonneg_of_le _ _ <;> aesop;
            · positivity;
            · gcongr ; norm_cast;
          convert h_abs_conv using 2 ; aesop;
          rw [ ← mul_inv, ← pow_add, Nat.add_sub_of_le right ];
        have h_partial_sums : Filter.Tendsto (fun x : ℕ => ∑ p ∈ Finset.product (Finset.range x) (Finset.range x), (if p.1 ≥ 2 ∧ p.2 ≥ 2 then (1 / (p.1 : ℝ) ^ p.2) else 0)) Filter.atTop (nhds (∑' (p : ℕ × ℕ), (if p.1 ≥ 2 ∧ p.2 ≥ 2 then (1 / (p.1 : ℝ) ^ p.2) else 0))) := by
          refine' h_partial_sums.hasSum.comp _;
          rw [ Filter.tendsto_atTop_atTop ];
          exact fun s => ⟨ s.sup Prod.fst + s.sup Prod.snd + 1, fun n hn => Finset.le_iff_subset.mpr fun p hp => Finset.mem_product.mpr ⟨ Finset.mem_range.mpr <| by linarith [ Finset.le_sup ( f := Prod.fst ) hp ], Finset.mem_range.mpr <| by linarith [ Finset.le_sup ( f := Prod.snd ) hp ] ⟩ ⟩;
        convert h_partial_sums using 1;
        · exact funext fun x => by erw [ Finset.sum_product ] ;
        · erw [ tsum_prod ];
          assumption;
      simp_all +decide [ mul_comm ];
      exact h_partial_sums.congr fun x => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by split_ifs <;> ring );
    -- Since the partial sums ∈ h_partial_sums are equal to the partial sums ∈ the goal, we can conclude that the goal's partial sums also converge to 1.
    have h_eq_partial_sums : ∀ x : ℕ, ∑ a ∈ Finset.range x, ∑ b ∈ Finset.range x, (if b ≥ 2 ∧ a ≥ 2 then (1 / (b : ℝ) ^ a) else 0) = ∑ a ∈ Finset.Ico 2 x, ∑ b ∈ Finset.Ico 2 x, (1 / (b : ℝ) ^ a) := by
      intro x; rw [ Finset.sum_comm ] ; simp +decide [ Finset.sum_ite ] ;
      rw [ Finset.sum_sigma', Finset.sum_sigma' ];
      refine' Finset.sum_bij ( fun y hy => ⟨ y.snd, y.fst ⟩ ) _ _ _ _ <;> aesop;
    simpa only [ h_eq_partial_sums ] using h_partial_sums;
  rcases Metric.tendsto_atTop.mp h_partial_sums ε εpos with ⟨ N, hN ⟩ ; exact ⟨ N + 2, fun x hx => ⟨ by linarith [ abs_lt.mp ( hN x ( by linarith ) ) ], by linarith [ abs_lt.mp ( hN x ( by linarith ) ) ] ⟩ ⟩ ;