Analysis
5.4. Ordering the reals

Imports

import Mathlib.Tactic
import Analysis.Section_5_3

Analysis I, Section 5.4: Ordering the reals

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Ordering on the real line

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Chapter5

Definition 5.4.1 (sequences bounded away from zero with sign). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.

abbrev BoundedAwayPos (a:ℕ → ℚ) : Prop :=
  ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c

Definition 5.4.1 (sequences bounded away from zero with sign).

abbrev BoundedAwayNeg (a:ℕ → ℚ) : Prop :=
  ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c

Definition 5.4.1 (sequences bounded away from zero with sign).

theorem boundedAwayPos_def (a:ℕ → ℚ) : BoundedAwayPos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := bya:ℕ → ℚ⊢ BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c
  rflAll goals completed! 🐙

Definition 5.4.1 (sequences bounded away from zero with sign).

theorem boundedAwayNeg_def (a:ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := bya:ℕ → ℚ⊢ BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c
  rflAll goals completed! 🐙

              /-- Examples 5.4.2 -/
example : BoundedAwayPos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := ⟨ 1, by⊢ 1 > 0 norm_numAll goals completed! 🐙, by⊢ ∀ (n : ℕ), (fun n ↦ 1 + 10 ^ (-↑n - 1)) n ≥ 1 introsn✝:ℕ⊢ (fun n ↦ 1 + 10 ^ (-↑n - 1)) n✝ ≥ 1; simpn✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); positivityAll goals completed! 🐙 ⟩/-- Examples 5.4.2 -/
example : BoundedAwayNeg (fun n ↦ -1 - 10^(-(n:ℤ)-1)) := ⟨ 1, by⊢ 1 > 0 norm_numAll goals completed! 🐙, by⊢ ∀ (n : ℕ), (fun n ↦ -1 - 10 ^ (-↑n - 1)) n ≤ -1 introsn✝:ℕ⊢ (fun n ↦ -1 - 10 ^ (-↑n - 1)) n✝ ≤ -1; simpn✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); positivityAll goals completed! 🐙 ⟩/-- Examples 5.4.2 -/
example : ¬ BoundedAwayPos (fun n ↦ (-1)^n) := by⊢ ¬BoundedAwayPos fun n ↦ (-1) ^ n
  intro ⟨ c, h1, h2 ⟩c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n ↦ (-1) ^ n) n ≥ c⊢ False; specialize h2 1c:ℚh1:c > 0h2:(fun n ↦ (-1) ^ n) 1 ≥ c⊢ False; grindAll goals completed! 🐙/-- Examples 5.4.2 -/
example : ¬ BoundedAwayNeg (fun n ↦ (-1)^n) := by⊢ ¬BoundedAwayNeg fun n ↦ (-1) ^ n
  intro ⟨ c, h1, h2 ⟩c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n ↦ (-1) ^ n) n ≤ -c⊢ False; specialize h2 0c:ℚh1:c > 0h2:(fun n ↦ (-1) ^ n) 0 ≤ -c⊢ False; grindAll goals completed! 🐙/-- Examples 5.4.2 -/
example : BoundedAwayZero (fun n ↦ (-1)^n) := ⟨ 1, by⊢ 1 > 0 norm_numAll goals completed! 🐙, by⊢ ∀ (n : ℕ), |(fun n ↦ (-1) ^ n) n| ≥ 1 introsn✝:ℕ⊢ |(fun n ↦ (-1) ^ n) n✝| ≥ 1; simpAll goals completed! 🐙 ⟩theorem BoundedAwayZero.boundedAwayPos {a:ℕ → ℚ} (ha: BoundedAwayPos a) : BoundedAwayZero a := bya:ℕ → ℚha:BoundedAwayPos a⊢ BoundedAwayZero a
  peel 3 ha with c h1 n h2h.h.ha:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ |a n| ≥ c; rwa [abs_of_nonneg (bya:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ 0 ≤ a n linarithAll goals completed! 🐙)]h.h.ha:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ a n ≥ ctheorem BoundedAwayZero.boundedAwayNeg {a:ℕ → ℚ} (ha: BoundedAwayNeg a) : BoundedAwayZero a := bya:ℕ → ℚha:BoundedAwayNeg a⊢ BoundedAwayZero a
  peel 3 ha with c h1 n h2h.h.ha:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ |a n| ≥ c; rw [abs_of_neg (by linarith)]h.h.ha:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ -a n ≥ c; linarithAll goals completed! 🐙theorem not_boundedAwayPos_boundedAwayNeg {a:ℕ → ℚ} : ¬ (BoundedAwayPos a ∧ BoundedAwayNeg a) := bya:ℕ → ℚ⊢ ¬(BoundedAwayPos a ∧ BoundedAwayNeg a)
  intro ⟨ ⟨ _, _, h2⟩ , ⟨ _, _, h4 ⟩ ⟩a:ℕ → ℚw✝¹:ℚleft✝¹:w✝¹ > 0h2:∀ (n : ℕ), a n ≥ w✝¹w✝:ℚleft✝:w✝ > 0h4:∀ (n : ℕ), a n ≤ -w✝⊢ False; linarith [h2 0, h4 0]All goals completed! 🐙abbrev Real.IsPos (x:Real) : Prop :=
  ∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM aabbrev Real.IsNeg (x:Real) : Prop :=
  ∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM atheorem Real.isPos_def (x:Real) :
    IsPos x ↔ ∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := byx:Real⊢ x.IsPos ↔ ∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a rflAll goals completed! 🐙theorem Real.isNeg_def (x:Real) :
    IsNeg x ↔ ∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := byx:Real⊢ x.IsNeg ↔ ∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a rflAll goals completed! 🐙