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

import Mathlib
open Finset BigOperators

-- OK let's do some warm-up
example (b : ℝ) (h : b ≥ 2) : 1 / ((b - 1) * b) = 1 / (b - 1) - 1 / b := by
  have h₁ : b - 1 ≠ 0 := by linarith
  field_simp

-- More easy stuff
example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = n ^ 2 := by
  induction n with
  | zero => trivial
  | succ n ih =>
    -- have blah (k : ℕ) : 2 * k + 1 = 2 * (k + 1) - 1 := by sorry
    -- rw [blah]
    rw [sum_range_succ, ih]
    ring

-- example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.range n, (2 * k + 1)) := by

def converges_to (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

-- Important: b should be in ℝ so that it's real div not nat div
-- This was so excruciating wow
lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ≥ 2) : ∑ a ∈ Ico 2 N, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) :=
  calc
    ∑ a ∈ Ico 2 N, 1 / (b ^ a) = ∑ a ∈ Ico 2 N, (1 / b) ^ a := by simp
    _ = ((1 / b) ^ 2 - (1 / b) ^ N) / (1 - (1 / b)) := by
      rw [geom_sum_Ico']
      by_contra h
      simp at h
      linarith
      exact h₁
    _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by
      have h₃ : b - 1 ≠ 0 := by linarith
      field_simp
      ring
    _ = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := by
      have h₃ : b ≠ 0 := by linarith
      have h₄ : b ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by
        rw [← mul_assoc, ← pow_succ' b (N - 1), Nat.sub_one_add_one]
        linarith
      simp [h₄, div_mul_cancel_left₀ h₃]

lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, 1 / (b ^ a)) 1 := by
  intro ε εpos
  use max (Nat.floor (1 / ε)) 2
  intro n nlarge
  simp
  have h₁ : n ≥ 2 := by
    exact le_of_max_le_right nlarge
  have h₂ (b : ℕ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ∈ Ico 2 N) : ∑ a ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = (1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by
    have h₃ : (b : ℝ) ≥ 2 := by
      have h₄ : b ≥ 2 := List.left_le_of_mem_range' h₂
      exact Nat.ofNat_le_cast.mpr h₄
    exact geom_sum ↑b N h₁ h₃
  have h₃ : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by
    calc
      ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 n, ∑ a ∈ Ico 2 n, (1 : ℝ) / (b ^ a) := sum_comm
      _ = ∑ b ∈ Ico 2 n, (1 / (b - 1) - 1 / b - 1 / (b ^ (n - 1) * (b - 1))) := by
        rw [h₂ _ n h₁]


      _ = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by
        induction n with
        | zero => trivial
        | succ n ih =>
          cases h₁
          field_simp
          rename_i h₃
          push_cast
          push_cast at ih
          rw [sum_Ico_succ_top, ih _ h₃]


  -- rw [h₂]


  -- then telescope the sums and bound the other sum
  -- qed