Skip to content

Instantly share code, notes, and snippets.

@louy2
Last active October 17, 2019 18:02
Show Gist options
  • Save louy2/4c5938960dd649d0e49aa53d3f56e07c to your computer and use it in GitHub Desktop.
Save louy2/4c5938960dd649d0e49aa53d3f56e07c to your computer and use it in GitHub Desktop.
My first non-trivial proof in Lean Prover! ㊗️🎉
import tactic.norm_num
import data.real.basic
import analysis.normed_space.basic
open normed_field
def lim_inf (f : ℝ → ℝ) (L : ℝ) :=
∀ ε > 0, ∃ N > (0 : ℝ),
∀ x, x > N → ∥f x - L∥ < ε
theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (λ x, C * a x) (C * L) :=
begin
assume C : ℝ,
rw lim_inf at *, /- unfold definitions -/
assume (ε : ℝ) (Hε : ε > 0),
by_cases HC : C = 0, {
fapply exists.intro, exact 1,
fapply exists.intro, norm_num,
assume (x : ℝ) (Hx : x > 1),
rw HC, /- ∥0 * a x - 0 * L∥ < ε -/
norm_num, /- 0 < ε -/
exact Hε
}, {
have HinvC : C⁻¹ ≠ 0, by exact inv_ne_zero HC,
have HnC : ∥C⁻¹∥ > 0, by exact abs_pos_iff.mpr HinvC,
have HnCε : ∥C⁻¹∥ * ε > 0, by exact mul_pos' HnC Hε,
let HE := H (∥C⁻¹∥ * ε) HnCε,
apply exists.elim HE,
intros N H1,
apply exists.elim H1,
intros HN H2,
apply exists.intro N,
apply exists.intro HN,
assume (x : ℝ) (Hx : x > N),
let H3 := H2 x Hx,
have E1: C * (a x - L) = C * a x - C * L, by exact mul_sub C (a x) L,
rw ←E1,
norm_num, simp at H3 ⊢,
rw ←(mul_lt_mul_left HnC),
rw ←mul_assoc,
rw ←norm_mul,
rw (inv_mul_cancel HC),
simp,
exact H3
}
end
theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (λ x, C * a x) (C * L) :=
begin
assume C : ℝ,
unfold lim_inf at H ⊢, /- unfold definitions -/
assume (ε : ℝ) (Hε : ε > 0),
by_cases HC : C = 0,
{ use [1, by norm_num],
assume (x : ℝ) (Hx : x > 1),
rw HC, /- ∥0 * a x - 0 * L∥ < ε -/
simpa using Hε },
{ have HinvC : C⁻¹ ≠ 0, from inv_ne_zero HC,
have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero HinvC,
have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
specialize H (∥C⁻¹∥ * ε) HnCε,
rcases H with ⟨N, HN, H⟩,
use [N, HN],
assume (x : ℝ) (Hx : x > N),
specialize H x Hx,
rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul],
exact H }
end
/- Revised by Patrick Massot -/
theorem lim_inf_cons_mul_eq_patrick_calc (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ C, lim_inf (λ x, C * a x) (C * L) :=
begin
intros C ε Hε,
by_cases HC : C = 0,
{ use [1, by norm_num],
intros,
simpa [HC] using Hε },
{ have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC),
have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
rcases H (∥C⁻¹∥ * ε) HnCε with ⟨N, HN, H⟩,
use [N, HN],
intros x Hx,
calc ∥ C * a x - C * L ∥
= ∥ C * (a x - L) ∥ : by rw mul_sub
... = ∥ C ∥ * ∥a x - L ∥ : norm_mul _ _
... < ∥ C ∥ * (∥C⁻¹∥ * ε) : mul_lt_mul_of_pos_left (H x Hx) (abs_pos_of_ne_zero HC)
... = ε : by rw [← mul_assoc, ← norm_mul, mul_inv_cancel HC, norm_one, one_mul] }
end
theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ C, lim_inf (λ x, C * a x) (C * L) :=
begin
intros C ε Hε,
by_cases HC : C = 0,
{ use [1, by norm_num],
intros,
simpa [HC] using Hε },
{ have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC),
have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
rcases H (∥C⁻¹∥ * ε) HnCε with ⟨N, HN, H⟩,
use [N, HN],
intros x Hx,
rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul],
exact H x Hx }
end
@louy2
Copy link
Author

louy2 commented Oct 17, 2019

Forgot to state the theorem I was proving! Not everyone can read Lean yet. Written in maths the theorem is:

$$\lim_{n\to\infty} C \cdot a_n = C \cdot \lim_{n\to\infty} a_n \text{ for } C \in \mathbb{R}$$

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment