-- Convergencia_de_producto.lean
-- Si uₙ converge a a y vₙ a b, entonces uₙvₙ converge a ab.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 29-noviembre-2024
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- En Lean, una sucesión u₀, u₁, u₂, ... se puede representar mediante
-- una función (u : ℕ → ℝ) de forma que u(n) es uₙ.
--
-- Se define que a límite de la sucesión u, por
--    def limite (u : ℕ → ℝ) (c : ℝ) :=
--      ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε
--
-- Demostrar que si uₙ converge a a y vₙ a b, entonces uₙvₙ
-- converge a ab.
-- ---------------------------------------------------------------------

-- Demostración en lenguaje natural
-- ================================

-- La demostración se basará en los siguientes lemas demostrados en
-- ejercicios anteriores
-- + Lema 1. El límite de uₙ es a syss el de uₙ-a es 0.
-- + Lema 2. Si uₙ y vₙ convergen a cero, entonces uₙvₙ converge a 0.
-- + Lema 3. Si el límite de uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca.
-- + Lema 4. Si el límite de uₙ es a y c ∈ ℝ, entonces el límite de uₙc es ac.
-- + Lema 5. Si uₙ converge a a y vₙ a b, entonces uₙ+vₙ converge a a+b.
--
-- Por el lema 1, puesto que lim uₙ = a y lim vₙ b, se tiene que
--    lim (uₙ - a) = 0                                             (1)
--    lim (vₙ - b) = 0                                             (2)
-- Por el lema 2, (1) y (2) se tiene que
--    lim (uₙ - a)(vₙ - b) = 0                                     (3)
-- Por el lema 3 y (2) se tiene que
--    lim a(vₙ - b) = a·0                                         (4)
-- Por el lema 4 y (1) se tiene que
--    lim (uₙ - a)b = 0·b                                          (5)
-- Por el lema 5, (3), (4) y (5) se tiene que
--    lim ((uₙ-a)(vₙ-b)+a·(vₙ-b)+(uₙ-a)·b) = 0+t·0+0·u
-- y, simplificando, queda
--    lim (uₙvₙ - ab) = 0
-- Finalmente, por el lema 1,
--    lim uₙvₙ = ab

-- Demostraciones con Lean4
-- ========================

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u v : ℕ → ℝ}
variable {a b : ℝ}

def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

-- Lema 1. El límite de uₙ es a syss el de uₙ-a es 0
-- (ver demostraciones en https://tinyurl.com/22nkht98)
lemma CNS_limite :
  limite u a ↔ limite (fun i ↦ u i - a) 0 :=
by
  rw [iff_eq_eq]
  calc limite u a
       = ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε       := rfl
     _ = ∀ ε > 0, ∃ N, ∀ n ≥ N, |(u n - a) - 0| < ε := by simp
     _ = limite (fun i ↦ u i - a) 0                 := rfl

-- Lema 2. Si uₙ y vₙ convergen a cero, entonces uₙvₙ converge a 0
-- (ver demostraciones en https://tinyurl.com/2ag9plvs )
lemma prod_convergen_a_cero
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε
  obtain ⟨U, hU⟩ := hu ε hε
  -- U : ℕ
  -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε
  obtain ⟨V, hV⟩ := hv 1 zero_lt_one
  -- V : ℕ
  -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1
  let N := max U V
  use N
  -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |(u * v) n - 0| < ε
  specialize hU n (le_of_max_le_left hn)
  -- hU : |u n - 0| < ε
  specialize hV n (le_of_max_le_right hn)
  -- hV : |v n - 0| < 1
  rw [sub_zero] at *
  -- hU : |u n - 0| < ε
  -- hV : |v n - 0| < 1
  -- ⊢ |(u * v) n - 0| < ε
  calc |(u * v) n|
       = |u n * v n|
         := rfl
     _ = |u n| * |v n|
         := abs_mul (u n) (v n)
     _ < ε * 1
         := mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))
     _ = ε
         := mul_one ε

-- Lema 3. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el
-- límite de cuₙ es ca (ver demostraciones en https://tinyurl.com/2244qcxs )
lemma limite_por_const
  (h : limite u a)
  : limite (fun n ↦ c * (u n)) (c * a) :=
by
  by_cases hc : c = 0
  . -- hc : c = 0
    subst hc
    -- ⊢ limite (fun n => 0 * u n) (0 * a)
    intros ε hε
    -- ε : ℝ
    -- hε : ε > 0
    -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => 0 * u n) n - 0 * a| < ε
    aesop
  . -- hc : ¬c = 0
    intros ε hε
    -- ε : ℝ
    -- hε : ε > 0
    -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε
    have hc' : 0 < |c| := abs_pos.mpr hc
    have hεc : 0 < ε / |c| := div_pos hε hc'
    specialize h (ε/|c|) hεc
    -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c|
    obtain ⟨N, hN⟩ := h
    -- N : ℕ
    -- hN : ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c|
    use N
    -- ⊢ ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε
    intros n hn
    -- n : ℕ
    -- hn : n ≥ N
    -- ⊢ |(fun n => c * u n) n - c * a| < ε
    specialize hN n hn
    -- hN : |u n - a| < ε / |c|
    dsimp only
    calc |c * u n - c * a|
         = |c * (u n - a)| := congr_arg abs (mul_sub c (u n) a).symm
       _ = |c| * |u n - a| := abs_mul c  (u n - a)
       _ < |c| * (ε / |c|) := (mul_lt_mul_left hc').mpr hN
       _ = ε               := mul_div_cancel₀ ε (ne_of_gt hc')

-- Lema 4. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el
-- límite de uₙc es ac (ver demostraciones en https://tinyurl.com/2xr94fh4 )
lemma const_por_limite
  (h : limite u a)
  : limite (fun n ↦ (u n) * c) (a * c) :=
by
  have h1 : ∀ n, (u n) * c = c * (u n) := by
    intro
    -- n : ℕ
    -- ⊢ u n * c = c * u n
    ring
  have h2 : a * c = c * a := mul_comm a c
  simp [h1,h2]
  -- ⊢ limite (fun n => c * u n) (c * a)
  exact limite_por_const h

-- Lema 5. Si la sucesión uₙ converge a a y la vₙ a b, entonces uₙ+vₙ
-- converge a a+b (ver demostraciones en https://tinyurl.com/294wn94r )
lemma limite_suma
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u + v) n - (a + b)| < ε
  have hε2 : 0 < ε / 2 := half_pos hε
  obtain ⟨Nu, hNu⟩ := hu (ε / 2) hε2
  -- Nu : ℕ
  -- hNu : ∀ (n : ℕ), n ≥ Nu → |u n - a| < ε / 2
  obtain ⟨Nv, hNv⟩ := hv (ε / 2) hε2
  -- Nv : ℕ
  -- hNv : ∀ (n : ℕ), n ≥ Nv → |v n - b| < ε / 2
  clear hu hv hε2 hε
  let N := max Nu Nv
  use N
  -- ⊢ ∀ (n : ℕ), n ≥ N → |(s + t) n - (a + b)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ N
  have nNu : n ≥ Nu := le_of_max_le_left hn
  specialize hNu n nNu
  -- hNu : |u n - a| < ε / 2
  have nNv : n ≥ Nv := le_of_max_le_right hn
  specialize hNv n nNv
  -- hNv : |v n - b| < ε / 2
  clear hn nNu nNv
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|  := rfl
     _ = |(u n - a) + (v n - b)|  := by { congr; ring }
     _ ≤ |u n - a| + |v n - b|    := by apply abs_add
     _ < ε / 2 + ε / 2            := by linarith [hNu, hNv]
     _ = ε                        := by apply add_halves

-- 1ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (fun n ↦ u n * v n) (a * b) :=
by
  rw [CNS_limite] at *
  -- hu : limite (fun i => u i - a) 0
  -- hv : limite (fun i => v i - b) 0
  -- ⊢ limite (fun i => u i * v i - a * b) 0
  have h : ∀ n, u n * v n - a * b
                = (u n - a) * (v n - b)
                  + a * (v n - b)
                  + (u n - a) * b := by
    intro n
    -- n : ℕ
    -- ⊢ u n * v n - a * b
    --   = (u n - a) * (v n - b) + a * (v n - b) + (u n - a) * b
    ring
  simp [h]
  -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b) + (u i - a) * b)
  --   0
  rw [show (0 : ℝ) = 0 + a * 0 + 0 * b by simp]
  -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b) + (u i - a) * b)
  --   (0 + a * 0 + 0 * b)
  have h1 : limite (fun n => (u n - a) * (v n - b)) 0
    := prod_convergen_a_cero hu hv
  have h2 : limite (fun n => a * (v n - b)) (a * 0)
    := limite_por_const hv
  have h3 : limite (fun n => (u n - a) * b) (0 * b)
    := const_por_limite hu
  exact limite_suma (limite_suma h1 h2) h3

-- 2ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (fun n ↦ u n * v n) (a * b) :=
by
  rw [CNS_limite] at *
  -- hu : limite (fun i => u i - a) 0
  -- hv : limite (fun i => v i - b) 0
  -- ⊢ limite (fun i => u i * v i - a * b) 0
  have h : ∀ n, u n * v n - a * b
                = (u n - a) * (v n - b)
                  + a * (v n - b)
                  + (u n - a) * b := by
    intro n
    -- n : ℕ
    -- ⊢ u n * v n - a * b
    --   = (u n - a) * (v n - b) + a * (v n - b) + (u n - a) * b
    ring
  simp [h]
  -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b) + (u i - a) * b)
  --   0
  rw [show (0 : ℝ) = 0 + a * 0 + 0 * b by simp]
  -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b) + (u i - a) * b)
  --   (0 + a * 0 + 0 * b)
  apply limite_suma
  . -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b)) (0 + a * 0)
    apply limite_suma
    . -- ⊢ limite (fun i => (u i - a) * (v i - b)) 0
      exact prod_convergen_a_cero hu hv
    . -- ⊢ limite (fun i => a * (v i - b)) (a * 0)
      exact limite_por_const hv
  . -- ⊢ limite (fun i => (u i - a) * b) (0 * b)
    exact const_por_limite hu

-- 3ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (fun n ↦ u n * v n) (a * b) :=
by
  rw [CNS_limite] at *
  -- hu : limite (fun i => u i - a) 0
  -- hv : limite (fun i => v i - b) 0
  -- ⊢ limite (fun i => u i * v i - a * b) 0
  have h : ∀ n, u n * v n - a * b
                = (u n - a) * (v n - b)
                  + a * (v n - b)
                  + (u n - a) * b := by
    intro n
    -- n : ℕ
    -- ⊢ u n * v n - a * b
    --   = (u n - a) * (v n - b) + a * (v n - b) + (u n - a) * b
    ring
  simp [h]
  -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b) + (u i - a) * b)
  --   0
  rw [show (0 : ℝ) = 0 + a * 0 + 0 * b by simp]
  -- ⊢ limite (fun i => (u i - a) * (v i - b) + a * (v i - b) + (u i - a) * b)
  --   (0 + a * 0 + 0 * b)
  refine' limite_suma (limite_suma _ _) _
  · -- ⊢ limite (fun i => (u i - a) * (v i - b)) 0
    exact prod_convergen_a_cero hu hv
  · -- ⊢ limite (fun i => a * (v i - b)) (a * 0)
    exact limite_por_const hv
  · -- ⊢ limite (fun i => (u i - a) * b) (0 * b)
    exact const_por_limite hu

-- Lemas usados
-- ============

-- variable (p q : Prop)
-- variable (c d x y: ℝ)
-- variable (f : ℝ → ℝ)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (abs_mul a b : |a * b| = |a| * |b|)
-- #check (abs_nonneg a : 0 ≤ |a|)
-- #check (abs_pos.mpr : a ≠ 0 → 0 < |a|)
-- #check (add_halves a : a / 2 + a / 2 = a)
-- #check (congr_arg f : x = y → f x = f y)
-- #check (div_pos : 0 < a → 0 < b → 0 < a / b)
-- #check (iff_eq_eq : (p ↔ q) = (p = q))
-- #check (le_of_max_le_left : max a b ≤ c → a ≤ c)
-- #check (le_of_max_le_right : max a b ≤ c → b ≤ c)
-- #check (mul_comm a b : a * b = b * a)
-- #check (mul_div_cancel₀ a : b ≠ 0 → b * (a / b) = a)
-- #check (mul_lt_mul'' : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d)
-- #check (mul_lt_mul_left : 0 < a → (a * b < a * c ↔ b < c))
-- #check (mul_one a : a * 1 = a)
-- #check (mul_sub a b c : a * (b - c) = a * b - a * c)
-- #check (ne_of_gt : b < a → a ≠ b)
-- #check (zero_lt_one : 0 < 1)