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
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120

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 =>
    rw [sum_range_succ, ih]
    ring

-- How to rw the inside of a sum
example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.range n, (2 * (k + 1) - 1)) := by
  apply Finset.sum_congr rfl
  intro k hk
  omega

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 telescope_sum (N : ℕ) (h : N ≥ 2): ∑ 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
      apply Finset.sum_congr rfl
      intro b bico
      have h₁ : (b : ℝ) ≥ 2 := by
        have h₂ : b ≥ 2 := List.left_le_of_mem_range' bico
        exact Nat.ofNat_le_cast.mpr h₂
      exact geom_sum b N h h₁
    _ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := sum_sub_distrib
    _ = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by
      have h₁ : ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (N - 1) := by
        induction h with
        | refl =>
          field_simp
          linarith
        | step h ih =>
          rw [sum_Ico_succ_top, ih]
          field_simp
          exact h
      rw [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 (2 / ε)) 2
  intro N Nlarge
  simp
  have h₁ : N ≥ 2 := by
    exact le_of_max_le_right Nlarge
  rw [abs_lt]
  constructor
  -- Greater than 1 - ε
  field_simp
  rw [telescope_sum N h₁]
  ring_nf

  -- have h₂ : -ε < ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) - 1 := by
    -- rw [telescope_sum N h₁]
    -- sorry
  -- simp
  -- simp at h₂
  -- exact h₂
  sorry
  -- Less than 1
  field_simp
  rw [telescope_sum N h₁]
  ring_nf
  field_simp
  have h₂ : (1 : ℝ) / (-1 + N) > 0 := by
    field_simp
    linarith
  have h₃ : ∀ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) > 0 := by
    intro b bico
    field_simp
    have h₄ : b ≥ 2 := List.left_le_of_mem_range' bico
    have h₅ : (b : ℝ) > 1 := Nat.one_lt_cast.mpr h₄
    have h₆ : (b : ℝ) ^ (N - 1) > 0 := by
      have h₇ : (b : ℝ) > 0 := by linarith
      apply pow_pos h₇
    have h₇ : (b : ℝ) - 1 > 0 := by
      linarith
    apply mul_pos h₆ h₇
  have h₄ : ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) ≥ 0 := by
    have h₅ : ∀ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) ≥ 0 := by
      exact fun b a => le_of_lt (h₃ b a)
    exact sum_nonneg h₅
  ring_nf at h₄
  field_simp at h₄
  have h₅ : -(1 : ℝ) / (-1 + N) < 0 := by
    nth_rw 1 [← mul_neg_one, mul_comm, mul_div_assoc]
    linarith
  linarith