1 Mathematical Analysis

Finally some real math in Lean! In this file we show how to define limits of sequences and continuity of functions in Lean. Of course it is just a toy version, far from the real Mathlib definitions. Nevertheless, that should be enough for you to get a taste of formalizing something that is not completely trivial.

import Mathlib

section

Since we haven’t touch division quite much yet, you may find it’s difficult to deal with multiplication and division. field_simp tactic may help you a lot in such cases. It won’t break things up as simp does, and becomes quite powerful nowadays, even able to acquire some positivity information automatically. Anyway, don’t worry too much about it for now.

We will use other automation tactics like linarith and ring as well. #help tactic <tactic_name> it if you don’t know them yet.

#help tactic field_simp

def TendsTo (a : ℕ → ℝ) (t : ℝ) : Prop :=
  ∀ ε > 0, ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → |a n - t| < ε

[EXR] The limit of the constant sequence with value c is c.

theorem tendsTo_const (c : ℝ) : TendsTo (fun _ ↦ c) c := by
  unfold TendsTo
  intro ε hε
  use 1
  intro n hn
  simp [hε]

- commutes with tendsTo

theorem tendsTo_neg {a : ℕ → ℝ} {t : ℝ} (ha : TendsTo a t) : TendsTo (fun n ↦ -a n) (-t) := by
  unfold TendsTo
  intro ε hε
  specialize ha ε hε
  rcases ha with ⟨n₀, hn₀⟩
  use n₀
  intro n hn
  specialize hn₀ n hn
  simp only [sub_neg_eq_add]
  -- what theorems should I use?
  rw [← abs_neg, add_comm]
  simp only [neg_add_rev, neg_neg]
  -- what theorems should I use?
  rwa [← sub_eq_add_neg]

+ commutes with tendsTo

theorem tendsTo_add {a b : ℕ → ℝ} {A : ℝ} {B : ℝ} (ha : TendsTo a A) (hb : TendsTo b B) :
    TendsTo (fun n => a n + b n) (A + B) := by
  intro ε hε
  specialize ha (ε / 2) (by linarith only [hε])
  specialize hb (ε / 2) (by linarith only [hε])
  rcases ha with ⟨n₀, ha⟩
  rcases hb with ⟨m₀, hb⟩
  use max n₀ m₀
  intro n hn
  -- what theorems should I use?
  rw [max_le_iff] at hn
  specialize ha n (by linarith only [hn.left])
  specialize hb n (by linarith only [hn.right])
  dsimp
  -- common tactic: eliminate abs to make use of `linarith`
  -- what theorems should I use?
  rw [abs_lt] at ha hb ⊢
  constructor
  · linarith only [ha, hb]
  · linarith only [ha, hb]

[EXR] - commutes with tendsTo

theorem tendsTo_sub {a b : ℕ → ℝ} {A B : ℝ} (ha : TendsTo a A) (hb : TendsTo b B) :
    TendsTo (fun n => a n - b n) (A - B) := by
  exact tendsTo_add ha (tendsTo_neg hb)

≤ version of TendsTo is equivalent to the usual TendsTo.

def TendsTo_le (a : ℕ → ℝ) (t : ℝ) : Prop :=
  ∀ ε > 0, ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → |a n - t| ≤ ε

-- [EXR]
theorem tendsTo_le_iff_TendsTo {a : ℕ → ℝ} {t : ℝ} : TendsTo_le a t ↔ TendsTo a t := by
  constructor
  · intro h ε hε
    rcases h (ε / 2) (by linarith [hε]) with ⟨n₀, hn₀⟩
    use n₀
    intro n hn; specialize hn₀ n hn
    linarith only [hn₀, hε]
  · intro h ε hε
    rcases h ε hε with ⟨n₀, hn₀⟩
    use n₀
    intro n hn; specialize hn₀ n hn
    linarith only [hn₀, hε]

a weaker version of TendsTo where we require ε < l. When l > 0, this is equivalent to TendsTo.

def TendsTo_εlt (a : ℕ → ℝ) (t : ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ε < l → ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → |a n - t| < ε

theorem tendsTo_εlt_iff_TendsTo {a : ℕ → ℝ} {t : ℝ} {l : ℝ} (l_gt_zero : l > 0) :
    TendsTo_εlt a t l ↔ TendsTo a t := by
  constructor
  · intro h ε hε
    specialize h (min ε (l / 2))
                 (by apply lt_min; all_goals linarith)
                 (by apply min_lt_of_right_lt; linarith only [l_gt_zero])
    rcases h with ⟨n₀, hn₀⟩; use n₀
    intro n hn; specialize hn₀ n hn
    rw [lt_min_iff] at hn₀
    exact hn₀.left
  · exact fun h ε hε _ ↦ h ε hε

* commutes with tendsTo.

theorem tendsTo_mul {a b : ℕ → ℝ} {A B : ℝ} (ha : TendsTo a A) (hb : TendsTo b B) :
    TendsTo (fun n ↦ a n * b n) (A * B) := by
  rw [← tendsTo_εlt_iff_TendsTo (show 1 > 0 by linarith)]
  intro ε hε hεlt1
  specialize ha (ε / (3 * (|B| + 1))) (by
    apply div_pos hε
    linarith only [abs_nonneg B])
  rcases ha with ⟨n₁, ha⟩
  specialize hb (ε / (3 * (|A| + 1))) (by
    apply div_pos hε
    linarith only [abs_nonneg A])
  rcases hb with ⟨n₂, hb⟩
  use max n₁ n₂
  intro n hn
  rw [max_le_iff] at hn
  specialize ha n hn.left
  specialize hb n hn.right

  -- grouping terms
  rw [show a n * b n - A * B = (a n - A) * (b n - B) + A * (b n - B) + B * (a n - A) by ring]
  repeat grw [abs_add_le]
  repeat grw [abs_mul]

  grw [ha, hb]

  -- sometimes you have no choice but add some manual steps
  have h1 : |A| * (ε / (3 * (|A| + 1))) < ε / 3 := by
    field_simp
    simp
  have h2 : |B| * (ε / (3 * (|B| + 1))) < ε / 3 := by
    field_simp
    simp
  have h3 : ε / (3 * (|B| + 1)) * (ε / (3 * (|A| + 1))) < ε / 3 := by
    field_simp
    grw [hεlt1, ← abs_nonneg A, ← abs_nonneg B]
    simp
  linarith only [h1, h2, h3]

squeeze theorem for sequences

theorem tendsTo_sandwich {a b c : ℕ → ℝ} {L : ℝ} (ha : TendsTo a L) (hc : TendsTo c L)
    (hab : ∀ n, a n ≤ b n) (hbc : ∀ n, b n ≤ c n) : TendsTo b L := by
  unfold TendsTo
  intro ε hε
  specialize ha ε hε
  specialize hc ε hε
  rcases ha with ⟨n₀, hn₀⟩
  rcases hc with ⟨m₀, hm₀⟩
  use max n₀ m₀
  intro n hn
  rw [max_le_iff] at hn
  specialize hab n
  specialize hn₀ n (by linarith only [hn.left])
  specialize hm₀ n (by linarith only [hn.right])
  specialize hbc n
  rw [abs_lt] at hn₀ hm₀ ⊢
  constructor
  · linarith only [hn₀, hm₀, hbc, hab]
  · linarith only [hn₀, hm₀, hbc, hab]

constant sequence tends to zero iff condition

theorem tendsTo_zero_iff_lt_ε {x : ℝ} : TendsTo (fun _ ↦ x) 0 ↔ (∀ ε > 0, |x| < ε) := by
  constructor
  · intro h ε hε
    specialize h ε hε
    rcases h with ⟨n₀, hn₀⟩
    specialize hn₀ n₀ (by linarith only)
    simpa using hn₀
  · intro h ε hε
    specialize h ε hε
    use 0
    intro n hn
    simpa using h

[EXR] zero sequence tends to x iff condition

theorem zero_tendsTo_iff_lt_ε {x : ℝ} : TendsTo (fun _ ↦ 0) x ↔ (∀ ε > 0, |x| < ε) := by
  constructor
  · intro h
    unfold TendsTo at h; simp at h
    intro ε hε
    specialize h ε hε
    rcases h with ⟨n₀, hn₀⟩
    specialize hn₀ n₀ (by linarith only)
    exact hn₀
  · intro h ε hε
    use 0
    intro n hn
    simpa using h ε hε

uniqueness of limits

theorem tendsTo_unique (a : ℕ → ℝ) (s t : ℝ) (hs : TendsTo a s) (ht : TendsTo a t) : s = t := by
  by_contra! hneq
  have hstp : 0 < |t - s| := by
    rw [abs_pos]
    contrapose! hneq
    apply_fun (· + s) at hneq
    symm; simpa using hneq
  have hst := tendsTo_sub hs ht
  simp only [sub_self] at hst
  rw [zero_tendsTo_iff_lt_ε] at hst
  specialize hst |t - s| hstp
  rw [abs_sub_comm] at hst
  linarith only [hst]

def contAt (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε

def cont (f : ℝ → ℝ) : Prop := ∀ x₀ : ℝ, contAt f x₀

continuity of function composition

def contAt_comp {f g : ℝ → ℝ} {x₀ : ℝ} (hf : contAt f (g x₀)) (hg : contAt g x₀) :
    contAt (f ∘ g) x₀ := by
  intro ε hε
  rcases hf ε hε with ⟨δf, hδf, hf⟩
  rcases hg δf hδf with ⟨δg, hδg, hg⟩
  use δg, hδg
  intro x hx
  simp only [Function.comp_apply]
  specialize hg x hx
  specialize hf (g x) hg
  exact hf

[EXR] continuity of function composition

def cont_comp {f g : ℝ → ℝ} (hf : cont f) (hg : cont g) : cont (f ∘ g) := by
  intro x
  exact contAt_comp (hf (g x)) (hg x)

[EXR] continuity implies sequential continuity

def tendsTo_of_contAt {f : ℝ → ℝ} {x₀ : ℝ} (hf : contAt f x₀)
    {a : ℕ → ℝ} (ha : TendsTo a x₀) : TendsTo (f ∘ a) (f x₀) := by
  intro ε hε
  rcases hf ε hε with ⟨δ, hδ, hδf⟩
  specialize ha δ hδ
  rcases ha with ⟨n₀, hn₀⟩
  use n₀
  intro n hn
  specialize hn₀ n hn
  specialize hδf (a n) hn₀
  exact hδf

The uniform limit of a sequence of continuous functions is continuous.

def uconv (f : ℕ → ℝ → ℝ) (f₀ : ℝ → ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ∀ x : ℝ, |f n x - f₀ x| < ε

theorem cont_of_cont_of_uconv
    (f : ℕ → ℝ → ℝ) (f_cont : ∀ n : ℕ, cont (f n))
    (f₀ : ℝ → ℝ) (h_uconv : uconv f f₀) : cont f₀ := by
  intro x₀ ε hε
  rcases h_uconv (ε / 3) (by linarith only [hε]) with ⟨N, hN⟩
  specialize hN N (by linarith)
  rcases f_cont N x₀ (ε / 3) (by linarith only [hε]) with ⟨δ, hδ, hδf⟩
  use δ, hδ
  intro x hx
  specialize hδf x hx
  have hNx := hN x
  have hNx₀ := hN x₀
  -- brute force `linarith` argument
  rw [abs_lt] at hNx hNx₀ hδf ⊢
  constructor
  all_goals linarith only [hNx, hNx₀, hδf]

The sequential definition of function continuity is equivalent to the epsilon-delta definition.

def contAt_seq (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
  ∀ a : ℕ → ℝ, TendsTo a x₀ → TendsTo (f ∘ a) (f x₀)

theorem contAt_iff_seq (f : ℝ → ℝ) (x₀ : ℝ) :
    contAt f x₀ ↔ contAt_seq f x₀ := by
  constructor
  · intro hf a ha
    exact tendsTo_of_contAt hf ha
  · contrapose
    intro hnfcont hnfseq
    unfold contAt at hnfcont
    push_neg at hnfcont
    -- construct a sequence `a n` tending to `x₀`
    let a (n : ℕ) : ℝ := 1 / (n + 1)
    have a_gt_zero (n : ℕ) : a n > 0 := by
      simp only [one_div, gt_iff_lt, inv_pos, a]
      linarith only
    have a_TendsTo_zero : TendsTo a 0 := by
      intro ε hε
      use Nat.ceil (1 / ε) -- ceiling function
      intro n hn
      rw [Nat.ceil_le] at hn
      simp only [sub_zero]
      rw [abs_of_pos (a_gt_zero n)]
      unfold a
      rw [div_lt_comm₀ (by linarith only) hε]
      linarith only [hn]

In the past, an existential quantifier inside a universal quantifier
would be troublesome to choose, e.g. `Classical.indefiniteDescription` was needed.
But with the `choose` tactic, this becomes much easier.

    rcases hnfcont with ⟨ε, hε, hnf⟩
    choose x x_lt_a fx_diverge using fun n ↦ hnf (a n) (a_gt_zero n)

    have x_tendsTo_x₀ : TendsTo x x₀ := by
      suffices TendsTo (fun n ↦ x n - x₀) 0 by
        have h_add := tendsTo_add this (tendsTo_const x₀)
        simpa using h_add
      refine tendsTo_sandwich (?_ : TendsTo (fun n ↦ -a n) 0) (?_ : TendsTo (fun n ↦ a n) 0) ?_ ?_
      · simpa using tendsTo_neg a_TendsTo_zero
      · exact a_TendsTo_zero
      all_goals
        intro n
        have := x_lt_a n
        rw [abs_lt] at this
        linarith only [this]
    -- but it is said that all such sequences converge
    have := hnfseq x x_tendsTo_x₀
    rcases this ε hε with ⟨n₀, hn₀⟩
    specialize hn₀ n₀ (by linarith only)
    dsimp only [Function.comp_apply] at hn₀
    specialize fx_diverge n₀
    linarith only [hn₀, fx_diverge]

end