Prove that if the sequence \(a\) converges to \(L\), then \[ (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1] \]
To do so, complete the following Lean 4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a : ℕ → ℝ} variable {L : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) : ∃ N, ∀ n ≥ N, a n ≥ L - 1 := by sorry
Prove that if \(aₙ\) converges to \(L\) and \(bₙ\) to \(M\), then \(aₙ+bₙ\) converges to \(L+M\).
To do so, complete the following Lean 4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℕ → ℝ} variable {L M : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hb : SeqLim b M) : SeqLim (a + b) (L + M) := by sorry
In Lean4, a sequence \(u_0, u_1, u_2, ...\) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is \(u_n\).
It is defined that the sequence \(u\) tends to \(c\) by:
def TendsTo (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε
Prove that if \(u_n\) tends to \(a\) and \(v_n\) tends to \(b\), then \(u_nv_n\) tends to \(ab\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u v : ℕ → ℝ} variable {a b : ℝ} def TendsTo (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε example (hu : TendsTo u a) (hv : TendsTo v b) : TendsTo (fun n ↦ u n * v n) (a * b) := by sorry
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
In Lean, a sequence \(u_0, u_1, u_2, ...\) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is the term \(u_n\).
We define that \(u\) tends to \(a\) by
def tendsTo : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε
Prove that if \(u_n\) tends to \(a\), then \(7u\_n\) tends to \(7a\).
To do this, complete the following Lean4 theory:
import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a : ℝ} def tendsTo : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : tendsTo u a) : tendsTo (fun n ↦ 7 * u n) (7 * a) := by sorry
In Lean4, we can define that \(a\) is the limit of the sequence \(u\) by:
def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε
and that \(f\) is continuous at \(a\) by:
def continuous_at (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε
To prove that if the function \(f\) is continuous at the point \(a\), and the sequence \(u(n)\) converges to \(a\), then the sequence \(f(u(n))\) converges to \(f(a)\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} variable {a : ℝ} variable {u : ℕ → ℝ} def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε def continuous_at (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε example (hf : continuous_at f a) (hu : is_limit u a) : is_limit (f ∘ u) (f a) := by sorry
In Lean4, we can define that \(a\) is the limit of the sequence \(u\) by:
def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε
and that \(a\) is an upper bound of \(u\) by:
def is_upper_bound (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a
Prove that if \(x\) is the limit of the sequence \(u\) and \(y\) is an upper bound of \(u\), then \(x ≤ y\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u : ℕ → ℝ) variable (x y : ℝ) def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε def is_upper_bound (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a example (hx : is_limit u x) (hy : is_upper_bound u y) : x ≤ y := by sorry