Skip to main content

If the limit of the sequence u(n) is a and c ∈ ℝ, then the limit of u(n)c is ac

In Lean, a sequence \(u_₀, u_₁, u_₂, ... \) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is \(u_n\).

It is defined that \(a\) is the limit of the sequence \(u\), by

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

Prove that if the limit of \(u_n\) is \(a\), then the limit of \(u_nc\) is \(ac\).

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

variable (u : ℕ → ℝ)
variable (a c : ℝ)

def TendsTo : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : TendsTo u a)
  : TendsTo (fun n ↦ (u n) * c) (a * c) :=
by sorry

1. Proof in natural language

In a previous exercise proofs have been presented of the following property

If \(\lim_{n \to \infty} u_n = a\) and \(c ∈ ℝ\), then \(\lim_{n \to \infty} cu_n = ca\).

From this property, it is demonstrated that

If \(\lim_{n \to \infty} u_n = a\) and \(c ∈ ℝ\), then \(\lim_{n \to \infty} u_nc = ac\).

Indeed, suppose that \[ \lim_{n \to \infty} u_n = a \] Then, by the previous property, \[ \lim_{n \to \infty} cu_n = ca \tag{1} \] But, by the commutativity of the product, we have that \[ (∀n ∈ ℕ)[cu_n = u_nc] \tag{2} \] \[ ca = ac \tag{3} \] By (1), (2) and (3) we have that \[ \lim_{n \to \infty} u_nc = ac \]

2. Proofs with Lean4

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

variable (u : ℕ → ℝ)
variable (a c : ℝ)

def TendsTo : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- The following theorem, demonstrated in a previous exercise, is used.
theorem tendsTo_const_mul
  (h : TendsTo u a)
  : TendsTo (fun n ↦ c * (u n)) (c * a) :=
by
  by_cases hc : c = 0
  . -- hc : c = 0
    subst hc
    -- ⊢ TendsTo (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|
    cases' h with N hN
    -- 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')

example
  (h : TendsTo u a)
  : TendsTo (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]
  -- ⊢ TendsTo (fun n => c * u n) (c * a)
  exact tendsTo_const_mul u a c h

-- Used lemmas
-- ===========

-- variable (b c : ℝ)
-- #check (abs_mul a b : |a * b| = |a| * |b|)
-- #check (abs_pos.mpr : a ≠ 0 → 0 < |a|)
-- #check (div_pos : 0 < a → 0 < b → 0 < a / b)
-- #check (lt_div_iff₀' : 0 < c → (a < b / c ↔ c * a < b))
-- #check (mul_comm a b : a * b = b * a)
-- #check (mul_div_cancel₀ a : b ≠ 0 → b * (a / b) = a)
-- #check (mul_lt_mul_left : 0 < a → (a * b < a * c ↔ b < c))
-- #check (mul_sub a b c : a * (b - c) = a * b - a * c)

You can interact with the previous proofs at Lean 4 Web.