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

My deepest appreciations go to Johan Commelin, Scott Morrison, and Floris van Doorn for helping me out on the Lean Prover Zulip.

I also thank Paul's Online Notes for the definition of lim_inf.

Practical tips I learned along the way:

  • Be on Lean Prover Zulip!
  • Once there, use the big search bar at the top to look for related questions
  • Ask! They are super friendly!
  • No parentheses needed for function application
  • begin to start the proof, end to finish the proof (this is the more helpful "tactic mode")
  • Don't forget the , after each step!
  • rw name_of_definition at h ⊢, to expand the definition
  • Use intros to automatically do universal instantiation. assume is the manual and clearer version.
  • Use have when going forward (deducing) from the hypotheses; use rw when going back from the goal
  • When using have, try by library_search when lost!
  • When using rw, try Cmd-P or Ctrl-P to search for useful equalities!
    • Keywords: eq add mul lt norm neg ...
  • let attaches temporary names to long stuff just like in Haskell or JavaScript
  • When doing algebra, try norm_num and simp!
  • If they fail, use rw with algebra theorems to do transformation

Regarding VS Code:

  • Use the jroesch.lean plugin!
  • On mac, I cannot copy from the "Lean Messages" view. Use Cmd-Shift-P > "Copy Contents to Comment" command!

Future:

  • Learn about how to improve this
  • Learn about calc mode

@louy2
Copy link
Author

louy2 commented Oct 17, 2019

Deep thank you to Kenny Lau and Patrick Massot for their critique on the code!

Two things I forgot:

  • *.intro is used to start a proof of * e.g. and.intro
  • *.elim is used to get the inner content of (peel off) * e.g. exists.elim

More learned:

  • unfold is specifically for unfolding definitions
  • simpa [rules] using h is rw [rules] then simp then exact h; without h it tries every assumption
  • use is a better exists.intro; use it to supply the positive cases all at once
  • specialize is a special tool for peeling off s
  • rcases is a better exists.elim; use it to get the Prop we know already exist
  • rcases H with ⟨W, H⟩ then use [W] is a great combo to use one to prove another

@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