El reto de esta semana consiste en demostrar en Lean 4 la desigualdad triangular inversa; es decir, que para cualesquiera números reales \(x\) e \(y\), se cumple la siguiente relación: \[ ||x| - |y|| ≤ |x - y| \]
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (x y : ℝ) example : |(|x| - |y|)| ≤ |x - y| := by sorry
El reto de esta semana consiste en demostrar en Lean 4 que si las sucesiones \(a_n\) y \(b_n\) convergen a \(L\) y \(M\), respectivamente, con \(L < M\), entonces eventualmente \(a_n < b_n\); es decir, que existe un \(k ∈ \mathbb{N}\) tal que, para todo \(n ≥ k\), \(a_n < b_n\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b : ℕ → ℝ} variable {L M : ℝ} example (ha : SeqLim a L) (hb : SeqLim b M) (hLM : L < M) : ∃ k, ∀ n ≥ k, a n < b n := by sorry
El reto de esta semana consiste en demostrar en Lean 4 que si la sucesión \(a_n\) converge a \(L\), entonces \(|a_n|\) converge a \(|L|\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b : ℕ → ℝ} variable {L : ℝ} example (ha : SeqLim a L) (hb : ∀ n, b n = |a n|) : SeqLim b |L| := by sorry
El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión converge a un límite no nulo, entonces sus términos están eventualmente acotados inferiormente por la mitad del valor absoluto del límite; es decir, si una sucesión \(a_n\) converge a \(L\) con \(L ≠ 0\), entonces existe \(k\) tal que para todo \(n ≥ k\) se tiene que \(|aₙ| ≥ \dfrac{|L|}{2}\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L : ℝ} example (ha : SeqLim a L) (hL : L ≠ 0) : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 := by sorry
El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión \(aₙ\) converge tanto a \(L\) como a \(M\), entonces \(L = M\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L M : ℝ} example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by sorry
El reto de esta semana consiste en demostrar en Lean 4 que que una sucesión que posee infinitos términos con valor absoluto superior a 10 no puede converger a un límite cuyo valor absoluto sea menor que 5.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L : ℝ} example (ha : ∀ k, ∃ n ≥ k, |a n| > 10) : ¬ ∃ L, SeqLim a L ∧ |L| < 5 := by sorry
El reto de esta semana consiste en demostrar en Lean 4 que la composición de funciones inyectivas es inyectiva.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by sorry
El reto de esta semana consiste en demostrar en Lean 4 el teorema del emparedado; es decir que si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℕ → ℝ} variable {L : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hc : SeqLim c L) (hab : ∀ n, a n ≤ b n) (hbc : ∀ n, b n ≤ c n) : SeqLim b L := by sorry
El reto de esta semana consiste en demostrar en Lean 4 ue, 5²ⁿ - 2³ⁿ es divisible por 17 para todo número natural n.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Nat.Basic import Mathlib.Tactic variable (n : ℕ) open Nat example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by sorry
Demostrar que si la sucesión \(a\) converge a \(L\), entonces \[ (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1] \]
Para ello, completar la siguiente teoría de Lean4:
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