Various properties about convergent sequences

convergent_sequences.lean

import algebra.pi_instances
import data.real.basic

-- https://www.youtube.com/playlist?list=PLgKTLlHQn951EjYi6UhygYNoCHLF1Z6E7
-- https://www.math.wustl.edu/~freiwald/310sequences2.pdf
-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Achievement.3A.20multiply.20convergent.20sequences

local attribute [instance] classical.prop_decidable

class metric_space (α : Type*) :=
(dist : α → α → ℝ)
(dist_self : ∀ x, dist x x = 0)
(eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
(dist_comm : ∀ x y : α, dist x y = dist y x)
(dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)

open metric_space

section

variables {α : Type*} [metric_space α]
variables {u v : ℕ → α} {l l₁ l₂ : α}

def limit (u : ℕ → α) (l : α) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) l ≤ ε

theorem dist_nonneg {x y : α}: 0 ≤ dist x y :=
begin
  have : dist x x ≤ dist x y + dist y x, from dist_triangle _ _ _,
  rw dist_comm y x at this,
  rw dist_self at this,
  linarith
end

theorem dist_pos {x y : α} : 0 < dist x y ↔ x ≠ y :=
begin
  split; contrapose!,
  { rintro rfl,
    have : dist x x = 0, from dist_self _,
    linarith },
  { intro h,
    apply eq_of_dist_eq_zero,
    have : 0 ≤ dist x y, from dist_nonneg,
    linarith }
end

lemma limit_unique (h₁ : limit u l₁) (h₂ : limit u l₂) : l₁ = l₂ :=
begin
  by_contra h,
  let ε := dist l₁ l₂,
  have : ε > 0, from dist_pos.mpr h,
  cases h₁ (ε/3) (by linarith) with N₁ hN₁,
  cases h₂ (ε/3) (by linarith) with N₂ hN₂,
  let n := max N₁ N₂,
  specialize hN₁ n (le_max_left _ _),
  specialize hN₂ n (le_max_right _ _),
  have : dist (u n) l₁ + dist (u n) l₂ < ε, by linarith,
  have : ε ≤ dist l₁ (u n) + dist (u n) l₂, from dist_triangle _ _ _,
  linarith [dist_comm l₁ (u n)]
end

end

notation `|`x`|` := abs x

noncomputable instance : metric_space ℝ :=
{ dist := λ x y, |x - y|,
  -- This proof term is hideous and beautiful simultaneously.
  dist_self := λ x, eq.symm (sub_self x) ▸ abs_zero,
  eq_of_dist_eq_zero := λ x y, eq_of_abs_sub_eq_zero,
  dist_comm := abs_sub,
  dist_triangle := abs_sub_le }

variables {u v : ℕ → ℝ} {c l l₁ l₂ : ℝ}

@[simp] def const (l : ℝ) : ℕ → ℝ := function.const _ l

lemma neg_const : -const l = const (-l) := by funext; simp

theorem const_limit : limit (const c) c :=
begin
  intros ε ε_pos,
  use 0,
  intros n hn,
  unfold dist,
  simp,
  linarith
end

theorem limit_add_limit (h₁ : limit u l₁) (h₂ : limit v l₂) :
  limit (u + v) (l₁ + l₂) :=
begin
  intros ε ε_pos,
  cases h₁ (ε/2) (by linarith) with N₁ hN₁,
  cases h₂ (ε/2) (by linarith) with N₂ hN₂,
  use max N₁ N₂,
  intros n hn,
  specialize hN₁ n (le_of_max_le_left hn),
  specialize hN₂ n (le_of_max_le_right hn),
  unfold dist at *,
  calc
  |(u + v) n - (l₁ + l₂)| = |(u n + v n) - (l₁ + l₂)| : rfl
  ...                     = |(u n - l₁) + (v n - l₂)| : by congr; ring
  ...                     ≤ |u n - l₁| + |v n - l₂|   : by apply abs_add
  ...                     ≤ ε                         : by linarith
end

lemma limit_add_const (h : limit u l) : limit (u + const c) (l + c) := 
limit_add_limit h const_limit

lemma limit_sub_self (h : limit u l) : limit (u - const l) 0 :=
begin
  rw [←sub_self l, sub_eq_add_neg, sub_eq_add_neg, neg_const],
  exact limit_add_const h
end

example (α : Type*) [linear_ordered_field α] (a b c : α) (h : a ≤ b / c) (H : c > 0) : a*c ≤ b := by refine (le_div_iff H).mp h

lemma limit_mul_const (h : limit u l) : limit (u * const c) (l * c) :=
begin
  intros ε ε_pos,
  by_cases hc : c = 0,
  { use 0,
    intros n hn,
    rw hc,
    simp,
    rw dist_self,
    exact le_of_lt ε_pos },
  { change c ≠ 0 at hc,
    have : ε / |c| > 0, from div_pos_of_pos_of_pos ε_pos (by rwa abs_pos_iff),
    cases h _ this with N hN,
    use N,
    intros n hn,
    specialize hN n hn,
    unfold dist at *,
    suffices : |(u n - l) * c| ≤ ε,
    { calc
      |(u * const c) n - l * c| = |(u n * c) - l * c| : rfl
      ...                       = |(u n - l) * c|     : by congr; ring
      ...                       ≤ ε                   : this },
    rwa [abs_mul, ←le_div_iff],
    rwa abs_pos_iff }
end

theorem limit_zero_mul_limit_zero (h₁ : limit u 0) (h₂ : limit v 0) :
  limit (u * v) 0 :=
begin
  intros ε ε_pos,
  have : ε.sqrt > 0, from real.sqrt_pos.mpr ε_pos,
  cases h₁ (ε.sqrt) this with N₁ hN₁,
  cases h₂ (ε.sqrt) this with N₂ hN₂,
  use max N₁ N₂,
  intros n hn,
  specialize hN₁ n (le_of_max_le_left hn),
  specialize hN₂ n (le_of_max_le_right hn),
  unfold dist at *,
  calc
  |(u * v) n - 0| = |(u n * v n) - 0|       : rfl
  ...             = |(u n - 0) * (v n - 0)| : by ring
  ...             = |u n - 0| * |v n - 0|   : by apply abs_mul
  ...             ≤ ε.sqrt * ε.sqrt         : mul_le_mul hN₁ hN₂ (abs_nonneg _) (le_of_lt this)
  ...             = ε.sqrt ^ 2              : by ring
  ...             = ε                       : real.sqr_sqrt (le_of_lt ε_pos)
end

@[simp] lemma limit_neg_iff : limit (-u) (-l) ↔ limit u l :=
begin
  split;
  { intros h ε ε_pos,
    cases h ε ε_pos with N hN,
    use N,
    intros n hn,
    specialize hN n hn,
    unfold dist at *,
    simpa [abs_sub] using hN }
end

notation u `+` v := limit_add_limit u v

theorem limit_mul_limit (h₁ : limit u l₁) (h₂ : limit v l₂) :
  limit (u * v) (l₁ * l₂) :=
begin
  let c₁ := const l₁,
  let c₂ := const l₂,
  have w₁ : limit ((u - c₁) * (v - c₂)) 0,
  from limit_zero_mul_limit_zero (limit_sub_self h₁) (limit_sub_self h₂),
  rw (show (u - c₁) * (v - c₂) = u * v - u * c₂ - v * c₁ + c₁ * c₂, by ring) at w₁,
  have w₂ : limit (-c₁ * c₂) (-l₁ * l₂), by simp [limit_mul_const const_limit],
  have w₃ : limit (u * c₂) (l₁ * l₂), from limit_mul_const h₁,
  have w₄ : limit (v * c₁) (l₁ * l₂), by { rw mul_comm l₁, exact limit_mul_const h₂ },
  have w := w₁ + w₂ + w₃ + w₄,
  -- The most satisfying two lines.
  simp [mul_comm u, mul_comm l₁] at w,
  ring at w,
  exact w
end

def nonzero {α : Type*} [has_zero α] (u : ℕ → α) : Prop := ∀ n, u n ≠ 0

variable {φ : ℕ → ℕ}

def extraction (φ : ℕ → ℕ) := ∀ m n, m < n → φ m < φ n

lemma nonzero_extraction_of_limit_ne_zero {hl : l ≠ 0} (h : limit u l) :
  ∃ φ, extraction φ ∧ nonzero (u ∘ φ) :=
begin
  set ε := |l|/2 with hε,
  have ε_pos : ε > 0, from div_pos_of_pos_of_pos (by rwa abs_pos_iff) two_pos,
  cases h ε ε_pos with N hN,
  -- A better idea would be to define `shift φ` s.t. `shift φ → extraction φ`.
  use λ n, n + N,
  split,
  { intros m n hmn, simpa },
  -- Brace yourselves, this proof is horribly ugly.
  { intros n hn,
    simp at hn,
    specialize hN (n + N) (by linarith),
    unfold dist at *,
    rw hn at hN,
    simp at hN,
    rw hε at hN,
    linarith }
end

def lower_bound (M : ℝ) (u : ℕ → ℝ) := ∀ n, M ≤ u n

lemma lower_bound_of_abs_nonzero (hu : nonzero u) (hl : l ≠ 0) (h : limit u l) :
  ∃ M > 0, lower_bound M (abs ∘ u) :=
begin
  sorry
end

example {a b : ℝ} : a⁻¹ - b⁻¹ = (a - b) * a⁻¹ * b⁻¹ :=
begin
  sorry
end

theorem limit_inv {hu : nonzero u} {hl : l ≠ 0} (h : limit u l) :
  limit u⁻¹ l⁻¹ :=
begin
  rcases lower_bound_of_abs_nonzero hu hl h with ⟨M, M_pos, hM⟩,
  intros ε ε_pos,
  have h₁ : M * M * ε > 0, from mul_pos (mul_pos M_pos M_pos) ε_pos,
  cases h (M * M * ε) h₁ with N hN,  
  use N,
  intros n hn,
  specialize hN n hn,
  unfold dist at *,
  calc
  |u⁻¹ n - l⁻¹| = |(u n - l) * u⁻¹ n * l⁻¹| : by { sorry }
  ...           ≤ |(u n - l) * M⁻¹ * M⁻¹|   : by { sorry }
  ...           ≤ ε                         : by { sorry }
  /-
  rcases lower_bound_of_abs_nonzero hu hl h with ⟨M, M_pos, hM⟩,
  intros ε ε_pos,
  cases h ε ε_pos with N hN,  
  use N,
  intros n hn,
  unfold dist at *,
  unfold lower_bound at hM,
  simp at hM,
  have h₁ : |u⁻¹ n| ≤ M⁻¹,
  { simp only [abs_inv, pi.inv_apply],
    exact inv_le_inv_of_le M_pos (hM n) },
  have h₃ : |(u n - l) * u⁻¹ n * l⁻¹| ≤ |(u n - l) * M⁻¹ * M⁻¹|,
  { simp only [abs_mul, abs_inv, abs_of_pos M_pos] at *,
    apply mul_le_mul,
    apply mul_le_mul,
    refl,
    simpa, -- `h₁` is used here.
    apply abs_nonneg,
    apply abs_nonneg,

    exact h₂,
    rw inv_nonneg,
    apply abs_nonneg,
    rw mul_nonneg_iff_right_nonneg_of_pos,
    apply abs_nonneg,
    rw inv_pos,
    exact M_pos },
  specialize hN n hn,
  calc
  |u⁻¹ n - l⁻¹| = |(u n - l) * u⁻¹ n * l⁻¹| : by { sorry }
  ...           ≤ |(u n - l) * M⁻¹ * M⁻¹|   : h₃
  ...           ≤ ε                         : by { sorry }
  -/
  /-
  cases lt_or_gt_of_ne (ne.symm hl) with hl hl,
  { cases h (l / 2) (by linarith) with N₁ hN₁,
    have h₁ : ∀ n, n ≥ N₁ → |u⁻¹ n| ≤ 2 / l,
    { intros n hn,
      unfold dist at *,   
      specialize hN₁ n hn,
      simp only [abs_inv, pi.inv_apply],
      

      sorry },
    intros ε ε_pos,
    cases h ((l^2 / 2) * ε) (by sorry) with N₂ hN₂,
    use max N₁ N₂,
    intros n hn,
    unfold dist at *,
    calc
    |u⁻¹ n - l⁻¹| = |(u n - l) * u⁻¹ n * l⁻¹|       : by {
      rw abs_sub,
      congr,
      rw mul_assoc,
     -- ring,
     -- congr,
     -- { rw mul_assoc,
     --   unfold nonzero at hu,
     --   simp,
     --   rw inv_mul_cancel (hu n),
     --   
     --   sorry },


      sorry }
    ...           = |u n - l| * |u⁻¹ n| * |l⁻¹|     : by rw [abs_mul, abs_mul]
    ...           ≤ (l^2 / 2) * ε * |u⁻¹ n| * |l⁻¹| : by {
      specialize hN₂ n (by sorry),
      
      apply mul_le_mul_of_nonneg_right,
      apply mul_le_mul_of_nonneg_right,
      assumption,
      apply abs_nonneg,
      apply abs_nonneg }
    ...           ≤ ε                               : by {
      
      sorry } },
  { 
    sorry }
  -/
end