doc-next-gen

Mathlib.Data.Real.Archimedean

Module docstring

{"# The real numbers are an Archimedean floor ring, and a conditionally complete linear order.

"}

Real.instArchimedean instance
: Archimedean ℝ
Full source 
instance instArchimedean : Archimedean ℝ :=
  archimedean_iff_rat_le.2 fun x =>
    Real.ind_mk x fun f =>
      let ⟨M, _, H⟩ := f.bounded' 0
      ⟨M, mk_le_of_forall_le ⟨0, fun i _ => Rat.cast_le.2 <| le_of_lt (abs_lt.1 (H i)).2⟩⟩
The Archimedean Property of Real Numbers
Informal description
The real numbers $\mathbb{R}$ form an Archimedean structure, meaning that for any real numbers $x$ and $y$ with $0 < y$, there exists a natural number $n$ such that $x < n \cdot y$.
Real.instFloorRing instance
: FloorRing ℝ
Full source 
noncomputable instance : FloorRing ℝ :=
  Archimedean.floorRing _
The Floor Ring Structure on Real Numbers
Informal description
The real numbers $\mathbb{R}$ form a linearly ordered ring with a floor function $\lfloor \cdot \rfloor : \mathbb{R} \to \mathbb{Z}$ satisfying the Galois connection property: for all integers $z$ and real numbers $a$, $z \leq \lfloor a \rfloor$ if and only if $z \leq a$.
Real.isCauSeq_iff_lift theorem
{f : ℕ → ℚ} : IsCauSeq abs f ↔ IsCauSeq abs fun i => (f i : ℝ)
Full source 
theorem isCauSeq_iff_lift {f : ℕ → ℚ} : IsCauSeqIsCauSeq abs f ↔ IsCauSeq abs fun i => (f i : ℝ) where
  mp H ε ε0 :=
    let ⟨δ, δ0, δε⟩ := exists_pos_rat_lt ε0
    (H _ δ0).imp fun i hi j ij => by dsimp; exact lt_trans (mod_cast hi _ ij) δε
  mpr H ε ε0 :=
    (H _ (Rat.cast_pos.2 ε0)).imp fun i hi j ij => by dsimp at hi; exact mod_cast hi _ ij
Equivalence of Cauchy Sequences in Rationals and Their Real Casts
Informal description
For any sequence of rational numbers $f : \mathbb{N} \to \mathbb{Q}$, $f$ is a Cauchy sequence with respect to the absolute value norm if and only if the sequence obtained by casting each term of $f$ to a real number is a Cauchy sequence with respect to the absolute value norm in $\mathbb{R}$.
Real.of_near theorem
(f : ℕ → ℚ) (x : ℝ) (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, |(f j : ℝ) - x| < ε) : ∃ h', Real.mk ⟨f, h'⟩ = x
Full source 
theorem of_near (f : ℕ → ℚ) (x : ℝ) (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, |(f j : ℝ) - x| < ε) :
    ∃ h', Real.mk ⟨f, h'⟩ = x :=
  ⟨isCauSeq_iff_lift.2 (CauSeq.of_near _ (const abs x) h),
    sub_eq_zero.1 <|
      abs_eq_zero.1 <|
        (eq_of_le_of_forall_lt_imp_le_of_dense (abs_nonneg _)) fun _ε ε0 =>
          mk_near_of_forall_near <| (h _ ε0).imp fun _i h j ij => le_of_lt (h j ij)⟩
Construction of Real Numbers from Rational Sequences Approaching a Limit
Informal description
For any sequence of rational numbers $f : \mathbb{N} \to \mathbb{Q}$ and any real number $x$, if for every $\varepsilon > 0$ there exists an index $i$ such that for all $j \geq i$ the distance between $f(j)$ (viewed as a real number) and $x$ is less than $\varepsilon$, then there exists a proof that $f$ is a Cauchy sequence and the real number constructed from $f$ equals $x$.
Real.exists_floor theorem
(x : ℝ) : ∃ ub : ℤ, (ub : ℝ) ≤ x ∧ ∀ z : ℤ, (z : ℝ) ≤ x → z ≤ ub
Full source 
theorem exists_floor (x : ℝ) : ∃ ub : ℤ, (ub : ℝ) ≤ x ∧ ∀ z : ℤ, (z : ℝ) ≤ x → z ≤ ub :=
  Int.exists_greatest_of_bdd
    (let ⟨n, hn⟩ := exists_int_gt x
    ⟨n, fun _ h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
    (let ⟨n, hn⟩ := exists_int_lt x
    ⟨n, le_of_lt hn⟩)
Existence of Integer Floor for Real Numbers
Informal description
For every real number $x$, there exists an integer $\text{ub}$ such that: 1. The real number obtained by casting $\text{ub}$ to $\mathbb{R}$ is less than or equal to $x$. 2. For any integer $z$, if the real number obtained by casting $z$ to $\mathbb{R}$ is less than or equal to $x$, then $z$ is less than or equal to $\text{ub}$.
Real.exists_isLUB theorem
(hne : s.Nonempty) (hbdd : BddAbove s) : ∃ x, IsLUB s x
Full source 
theorem exists_isLUB (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ x, IsLUB s x := by
  rcases hne, hbdd with ⟨⟨L, hL⟩, ⟨U, hU⟩⟩
  have : ∀ d : ℕ, BddAbove { m : ℤ | ∃ y ∈ s, (m : ℝ) ≤ y * d } := by
    obtain ⟨k, hk⟩ := exists_int_gt U
    refine fun d => ⟨k * d, fun z h => ?_⟩
    rcases h with ⟨y, yS, hy⟩
    refine Int.cast_le.1 (hy.trans ?_)
    push_cast
    exact mul_le_mul_of_nonneg_right ((hU yS).trans hk.le) d.cast_nonneg
  choose f hf using fun d : ℕ =>
    Int.exists_greatest_of_bdd (this d) ⟨⌊L * d⌋, L, hL, Int.floor_le _⟩
  have hf₁ : ∀ n > 0, ∃ y ∈ s, ((f n / n : ℚ) : ℝ) ≤ y := fun n n0 =>
    let ⟨y, yS, hy⟩ := (hf n).1
    ⟨y, yS, by simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy⟩
  have hf₂ : ∀ n > 0, ∀ y ∈ s, (y - ((n : ℕ) : ℝ)⁻¹) < (f n / n : ℚ) := by
    intro n n0 y yS
    have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
    simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]
    rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]
    exact ne_of_gt (Nat.cast_pos.2 n0)
  have hg : IsCauSeq abs (fun n => f n / n : ℕ → ℚ) := by
    intro ε ε0
    suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
      refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
      rw [neg_lt, neg_sub]
      exact this _ le_rfl _ ij
    intro j ij k ik
    replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
    replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
    have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
    have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
    rcases hf₁ _ j0 with ⟨y, yS, hy⟩
    refine lt_of_lt_of_le ((Rat.cast_lt (K := ℝ)).1 ?_) ((inv_le_comm₀ ε0 (Nat.cast_pos.2 k0)).1 ik)
    simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)
  let g : CauSeq ℚ abs := ⟨fun n => f n / n, hg⟩
  refine ⟨mk g, ⟨fun x xS => ?_, fun y h => ?_⟩⟩
  · refine le_of_forall_lt_imp_le_of_dense fun z xz => ?_
    obtain ⟨K, hK⟩ := exists_nat_gt (x - z)⁻¹
    refine le_mk_of_forall_le ⟨K, fun n nK => ?_⟩
    replace xz := sub_pos.2 xz
    replace hK := hK.le.trans (Nat.cast_le.2 nK)
    have n0 : 0 < n := Nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK)
    refine le_trans ?_ (hf₂ _ n0 _ xS).le
    rwa [le_sub_comm, inv_le_comm₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _) xz]
  · exact
      mk_le_of_forall_le
        ⟨1, fun n n1 =>
          let ⟨x, xS, hx⟩ := hf₁ _ n1
          le_trans hx (h xS)⟩
Existence of Supremum for Nonempty Bounded Above Sets in Real Numbers
Informal description
For any nonempty subset $s$ of the real numbers that is bounded above, there exists a real number $x$ which is the least upper bound (supremum) of $s$.
Real.exists_isGLB theorem
(hne : s.Nonempty) (hbdd : BddBelow s) : ∃ x, IsGLB s x
Full source 
/-- A nonempty, bounded below set of real numbers has a greatest lower bound. -/
theorem exists_isGLB (hne : s.Nonempty) (hbdd : BddBelow s) : ∃ x, IsGLB s x := by
  have hne' : (-s).Nonempty := Set.nonempty_neg.mpr hne
  have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hbdd
  use -Classical.choose (Real.exists_isLUB hne' hbdd')
  rw [← isLUB_neg]
  exact Classical.choose_spec (Real.exists_isLUB hne' hbdd')
Existence of Infimum for Nonempty Bounded Below Sets in Real Numbers
Informal description
For any nonempty subset $s$ of the real numbers that is bounded below, there exists a real number $x$ which is the greatest lower bound (infimum) of $s$.
Real.sSup_def theorem
(s : Set ℝ) : sSup s = if h : s.Nonempty ∧ BddAbove s then Classical.choose (exists_isLUB h.1 h.2) else 0
Full source 
theorem sSup_def (s : Set ℝ) :
    sSup s = if h : s.Nonempty ∧ BddAbove s then Classical.choose (exists_isLUB h.1 h.2) else 0 :=
  rfl
Definition of Supremum for Real Numbers
Informal description
For any set $s$ of real numbers, the supremum $\sup(s)$ is defined as follows: if $s$ is nonempty and bounded above, then $\sup(s)$ is the least upper bound of $s$ (chosen via the axiom of choice); otherwise, $\sup(s) = 0$.
Real.isLUB_sSup theorem
(h₁ : s.Nonempty) (h₂ : BddAbove s) : IsLUB s (sSup s)
Full source 
protected theorem isLUB_sSup (h₁ : s.Nonempty) (h₂ : BddAbove s) : IsLUB s (sSup s) := by
  simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
  apply Classical.choose_spec
Supremum is Least Upper Bound in Real Numbers
Informal description
For any nonempty subset $s$ of the real numbers that is bounded above, the supremum $\sup s$ is the least upper bound of $s$.
Real.instInfSet instance
: InfSet ℝ
Full source 
noncomputable instance : InfSet ℝ :=
  ⟨fun s => -sSup (-s)⟩
The Infimum Operator on Real Numbers
Informal description
The real numbers $\mathbb{R}$ are equipped with a canonical infimum operator $\inf$ for sets, which assigns to every nonempty bounded below set $s \subseteq \mathbb{R}$ its greatest lower bound $\inf s$.
Real.sInf_def theorem
(s : Set ℝ) : sInf s = -sSup (-s)
Full source 
theorem sInf_def (s : Set ℝ) : sInf s = -sSup (-s) := rfl
Infimum-Supremum Duality for Real Numbers
Informal description
For any set $s$ of real numbers, the infimum of $s$ is equal to the negative of the supremum of the set $-s = \{-x \mid x \in s\}$, i.e., \[ \inf s = -\sup (-s). \]
Real.isGLB_sInf theorem
(h₁ : s.Nonempty) (h₂ : BddBelow s) : IsGLB s (sInf s)
Full source 
protected theorem isGLB_sInf (h₁ : s.Nonempty) (h₂ : BddBelow s) : IsGLB s (sInf s) := by
  rw [sInf_def, ← isLUB_neg', neg_neg]
  exact Real.isLUB_sSup h₁.neg h₂.neg
Infimum is Greatest Lower Bound in Real Numbers
Informal description
For any nonempty subset $s$ of the real numbers that is bounded below, the infimum $\inf s$ is the greatest lower bound of $s$.
Real.instConditionallyCompleteLinearOrder instance
: ConditionallyCompleteLinearOrder ℝ
Full source 
noncomputable instance : ConditionallyCompleteLinearOrder ℝ where
  __ := Real.linearOrder
  __ := Real.lattice
  le_csSup s a hs ha := (Real.isLUB_sSup ⟨a, ha⟩ hs).1 ha
  csSup_le s a hs ha := (Real.isLUB_sSup hs ⟨a, ha⟩).2 ha
  csInf_le s a hs ha := (Real.isGLB_sInf ⟨a, ha⟩ hs).1 ha
  le_csInf s a hs ha := (Real.isGLB_sInf hs ⟨a, ha⟩).2 ha
  csSup_of_not_bddAbove s hs := by simp [hs, sSup_def]
  csInf_of_not_bddBelow s hs := by simp [hs, sInf_def, sSup_def]
The Real Numbers as a Conditionally Complete Linear Order
Informal description
The real numbers $\mathbb{R}$ form a conditionally complete linear order, meaning every nonempty subset that is bounded above has a least upper bound and every nonempty subset that is bounded below has a greatest lower bound.
Real.lt_sInf_add_pos theorem
(h : s.Nonempty) {ε : ℝ} (hε : 0 < ε) : ∃ a ∈ s, a < sInf s + ε
Full source 
theorem lt_sInf_add_pos (h : s.Nonempty) {ε : ℝ} (hε : 0 < ε) : ∃ a ∈ s, a < sInf s + ε :=
  exists_lt_of_csInf_lt h <| lt_add_of_pos_right _ hε
Existence of Element Below Infimum Plus Epsilon: $\exists a \in s, a < \inf s + \varepsilon$
Informal description
Let $s$ be a nonempty subset of the real numbers $\mathbb{R}$ and $\varepsilon$ a positive real number. Then there exists an element $a \in s$ such that $a < \inf s + \varepsilon$.
Real.add_neg_lt_sSup theorem
(h : s.Nonempty) {ε : ℝ} (hε : ε < 0) : ∃ a ∈ s, sSup s + ε < a
Full source 
theorem add_neg_lt_sSup (h : s.Nonempty) {ε : ℝ} (hε : ε < 0) : ∃ a ∈ s, sSup s + ε < a :=
  exists_lt_of_lt_csSup h <| add_lt_iff_neg_left.2 hε
Existence of Element Below Supremum with Negative Offset
Informal description
Let $s$ be a nonempty subset of the real numbers $\mathbb{R}$. For any negative real number $\varepsilon < 0$, there exists an element $a \in s$ such that $\sup s + \varepsilon < a$.
Real.sInf_le_iff theorem
(h : BddBelow s) (h' : s.Nonempty) : sInf s ≤ a ↔ ∀ ε, 0 < ε → ∃ x ∈ s, x < a + ε
Full source 
theorem sInf_le_iff (h : BddBelow s) (h' : s.Nonempty) :
    sInfsInf s ≤ a ↔ ∀ ε, 0 < ε → ∃ x ∈ s, x < a + ε := by
  rw [le_iff_forall_pos_lt_add]
  constructor <;> intro H ε ε_pos
  · exact exists_lt_of_csInf_lt h' (H ε ε_pos)
  · rcases H ε ε_pos with ⟨x, x_in, hx⟩
    exact csInf_lt_of_lt h x_in hx
Infimum Criterion: $\inf s \leq a \leftrightarrow \forall \varepsilon > 0, \exists x \in s, x < a + \varepsilon$
Informal description
Let $s$ be a nonempty subset of the real numbers $\mathbb{R}$ that is bounded below. Then the infimum of $s$ is less than or equal to a real number $a$ if and only if for every positive real number $\varepsilon > 0$, there exists an element $x \in s$ such that $x < a + \varepsilon$.
Real.le_sSup_iff theorem
(h : BddAbove s) (h' : s.Nonempty) : a ≤ sSup s ↔ ∀ ε, ε < 0 → ∃ x ∈ s, a + ε < x
Full source 
theorem le_sSup_iff (h : BddAbove s) (h' : s.Nonempty) :
    a ≤ sSup s ↔ ∀ ε, ε < 0 → ∃ x ∈ s, a + ε < x := by
  rw [le_iff_forall_pos_lt_add]
  refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩
  · exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))
  · rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
    exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)
Supremum Criterion: $a \leq \sup s \leftrightarrow \forall \varepsilon < 0, \exists x \in s, a + \varepsilon < x$
Informal description
Let $s$ be a nonempty subset of the real numbers $\mathbb{R}$ that is bounded above. Then a real number $a$ is less than or equal to the supremum of $s$ if and only if for every negative real number $\varepsilon < 0$, there exists an element $x \in s$ such that $a + \varepsilon < x$.
Real.sSup_empty theorem
: sSup (∅ : Set ℝ) = 0
Full source 
@[simp]
theorem sSup_empty : sSup (∅ : Set ℝ) = 0 :=
  dif_neg <| by simp
Supremum of Empty Set is Zero
Informal description
The supremum of the empty set in the real numbers is equal to $0$, i.e., $\sup \emptyset = 0$.
Real.iSup_of_isEmpty theorem
[IsEmpty ι] (f : ι → ℝ) : ⨆ i, f i = 0
Full source 
@[simp] lemma iSup_of_isEmpty [IsEmpty ι] (f : ι → ℝ) : ⨆ i, f i = 0 := by
  dsimp [iSup]
  convert Real.sSup_empty
  rw [Set.range_eq_empty_iff]
  infer_instance
Supremum over Empty Index is Zero
Informal description
For any empty index type $\iota$ and any function $f : \iota \to \mathbb{R}$, the supremum of $f$ over $\iota$ is equal to $0$, i.e., $\bigsqcup_{i \in \iota} f(i) = 0$.
Real.sSup_of_not_bddAbove theorem
(hs : ¬BddAbove s) : sSup s = 0
Full source 
lemma sSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = 0 := dif_neg fun h => hs h.2
Supremum of Unbounded Above Set is Zero
Informal description
For any set $s$ of real numbers that is not bounded above, the supremum of $s$ is equal to $0$.
Real.iSup_of_not_bddAbove theorem
(hf : ¬BddAbove (Set.range f)) : ⨆ i, f i = 0
Full source 
lemma iSup_of_not_bddAbove (hf : ¬BddAbove (Set.range f)) : ⨆ i, f i = 0 := sSup_of_not_bddAbove hf
Supremum of Unbounded Above Function is Zero
Informal description
For any function $f : \iota \to \mathbb{R}$ whose range is not bounded above, the supremum of $f$ over its domain is equal to $0$, i.e., $\bigsqcup_{i} f(i) = 0$.
Real.sInf_empty theorem
: sInf (∅ : Set ℝ) = 0
Full source 
@[simp]
theorem sInf_empty : sInf (∅ : Set ℝ) = 0 := by simp [sInf_def, sSup_empty]
Infimum of Empty Set is Zero
Informal description
The infimum of the empty set in the real numbers is equal to $0$, i.e., $\inf \emptyset = 0$.
Real.iInf_of_isEmpty theorem
[IsEmpty ι] (f : ι → ℝ) : ⨅ i, f i = 0
Full source 
@[simp] nonrec lemma iInf_of_isEmpty [IsEmpty ι] (f : ι → ℝ) : ⨅ i, f i = 0 := by
  rw [iInf_of_isEmpty, sInf_empty]
Infimum over Empty Index is Zero
Informal description
For any empty index type $\iota$ and any function $f : \iota \to \mathbb{R}$, the infimum of $f$ over $\iota$ is equal to $0$, i.e., $\bigsqcap_{i \in \iota} f(i) = 0$.
Real.iInf_of_not_bddBelow theorem
(hf : ¬BddBelow (Set.range f)) : ⨅ i, f i = 0
Full source 
theorem iInf_of_not_bddBelow (hf : ¬BddBelow (Set.range f)) : ⨅ i, f i = 0 :=
  sInf_of_not_bddBelow hf
Infimum of Unbounded Below Function is Zero
Informal description
For any function $f : \iota \to \mathbb{R}$ whose range is not bounded below, the infimum of $f$ over its domain is equal to $0$, i.e., $\bigsqcap_i f(i) = 0$.
Real.sSup_le theorem
(hs : ∀ x ∈ s, x ≤ a) (ha : 0 ≤ a) : sSup s ≤ a
Full source 
/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at most some nonnegative number `a` to show that `sSup s ≤ a`.

See also `csSup_le`. -/
protected lemma sSup_le (hs : ∀ x ∈ s, x ≤ a) (ha : 0 ≤ a) : sSup s ≤ a := by
  obtain rfl | hs' := s.eq_empty_or_nonempty
  exacts [sSup_empty.trans_le ha, csSup_le hs' hs]
Supremum of Nonpositive Set is Bounded by Nonnegative Upper Bound
Informal description
For any set $s$ of real numbers and any real number $a \geq 0$, if every element $x \in s$ satisfies $x \leq a$, then the supremum of $s$ satisfies $\sup s \leq a$.
Real.iSup_le theorem
(hf : ∀ i, f i ≤ a) (ha : 0 ≤ a) : ⨆ i, f i ≤ a
Full source 
/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty, it suffices to show
that all values of `f` are at most some nonnegative number `a` to show that `⨆ i, f i ≤ a`.

See also `ciSup_le`. -/
protected lemma iSup_le (hf : ∀ i, f i ≤ a) (ha : 0 ≤ a) : ⨆ i, f i ≤ a :=
  Real.sSup_le (Set.forall_mem_range.2 hf) ha
Supremum of Nonpositive Function is Bounded by Nonnegative Upper Bound
Informal description
For any real-valued function $f$ indexed by $i$, if $f(i) \leq a$ for all $i$ and $a \geq 0$, then the supremum of $f$ satisfies $\bigsqcup_i f(i) \leq a$.
Real.le_sInf theorem
(hs : ∀ x ∈ s, a ≤ x) (ha : a ≤ 0) : a ≤ sInf s
Full source 
/-- As `sInf s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at least some nonpositive number `a` to show that `a ≤ sInf s`.

See also `le_csInf`. -/
protected lemma le_sInf (hs : ∀ x ∈ s, a ≤ x) (ha : a ≤ 0) : a ≤ sInf s := by
  obtain rfl | hs' := s.eq_empty_or_nonempty
  exacts [ha.trans_eq sInf_empty.symm, le_csInf hs' hs]
Nonpositive Lower Bound Implies Nonpositive Infimum
Informal description
Let $s$ be a set of real numbers and $a$ a nonpositive real number. If every element $x \in s$ satisfies $a \leq x$, then $a \leq \inf s$.
Real.le_iInf theorem
(hf : ∀ i, a ≤ f i) (ha : a ≤ 0) : a ≤ ⨅ i, f i
Full source 
/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty, it suffices to show
that all values of `f` are at least some nonpositive number `a` to show that `a ≤ ⨅ i, f i`.

See also `le_ciInf`. -/
protected lemma le_iInf (hf : ∀ i, a ≤ f i) (ha : a ≤ 0) : a ≤ ⨅ i, f i :=
  Real.le_sInf (Set.forall_mem_range.2 hf) ha
Nonpositive lower bound implies nonpositive infimum for indexed families
Informal description
Let $f : \iota \to \mathbb{R}$ be a real-valued function and $a \leq 0$ a nonpositive real number. If $a \leq f(i)$ for all $i \in \iota$, then $a \leq \bigsqcap_i f(i)$.
Real.sSup_nonpos theorem
(hs : ∀ x ∈ s, x ≤ 0) : sSup s ≤ 0
Full source 
/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are nonpositive to show that `sSup s ≤ 0`. -/
lemma sSup_nonpos (hs : ∀ x ∈ s, x ≤ 0) : sSup s ≤ 0 := Real.sSup_le hs le_rfl
Supremum of Nonpositive Set is Nonpositive
Informal description
For any set $s$ of real numbers, if every element $x \in s$ satisfies $x \leq 0$, then the supremum of $s$ satisfies $\sup s \leq 0$.
Real.iSup_nonpos theorem
(hf : ∀ i, f i ≤ 0) : ⨆ i, f i ≤ 0
Full source 
/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty,
it suffices to show that all values of `f` are nonpositive to show that `⨆ i, f i ≤ 0`. -/
lemma iSup_nonpos (hf : ∀ i, f i ≤ 0) : ⨆ i, f i ≤ 0 := Real.iSup_le hf le_rfl
Supremum of Nonpositive Function is Nonpositive
Informal description
For any real-valued function $f$ indexed by $i$, if $f(i) \leq 0$ for all $i$, then the supremum of $f$ satisfies $\bigsqcup_i f(i) \leq 0$.
Real.sInf_nonneg theorem
(hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sInf s
Full source 
/-- As `sInf s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are nonnegative to show that `0 ≤ sInf s`. -/
lemma sInf_nonneg (hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sInf s := Real.le_sInf hs le_rfl
Nonnegativity of Infimum for Nonnegative Sets
Informal description
For any set $s$ of real numbers, if every element $x \in s$ satisfies $0 \leq x$, then the infimum of $s$ satisfies $0 \leq \inf s$.
Real.iInf_nonneg theorem
(hf : ∀ i, 0 ≤ f i) : 0 ≤ iInf f
Full source 
/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty,
it suffices to show that all values of `f` are nonnegative to show that `0 ≤ ⨅ i, f i`. -/
lemma iInf_nonneg (hf : ∀ i, 0 ≤ f i) : 0 ≤ iInf f := Real.le_iInf hf le_rfl
Nonnegativity of Infimum for Nonnegative Indexed Functions
Informal description
For any real-valued function $f$ indexed by $i$, if $0 \leq f(i)$ for all $i$, then $0 \leq \bigsqcap_i f(i)$.
Real.sSup_nonneg' theorem
(hs : ∃ x ∈ s, 0 ≤ x) : 0 ≤ sSup s
Full source 
/-- As `sSup s = 0` when `s` is a set of reals that's unbounded above, it suffices to show that `s`
contains a nonnegative element to show that `0 ≤ sSup s`. -/
lemma sSup_nonneg' (hs : ∃ x ∈ s, 0 ≤ x) : 0 ≤ sSup s := by
  classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge
Nonnegativity of Supremum for Sets with Nonnegative Elements
Informal description
For any set $s$ of real numbers, if there exists an element $x \in s$ such that $0 \leq x$, then the supremum of $s$ satisfies $0 \leq \sup s$.
Real.iSup_nonneg' theorem
(hf : ∃ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i
Full source 
/-- As `⨆ i, f i = 0` when the real-valued function `f` is unbounded above,
it suffices to show that `f` takes a nonnegative value to show that `0 ≤ ⨆ i, f i`. -/
lemma iSup_nonneg' (hf : ∃ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i := sSup_nonneg' <| Set.exists_range_iff.2 hf
Nonnegativity of Supremum for Functions with Nonnegative Values
Informal description
For a real-valued function $f$, if there exists an index $i$ such that $0 \leq f(i)$, then the supremum of $f$ satisfies $0 \leq \bigsqcup_i f(i)$.
Real.sInf_nonpos' theorem
(hs : ∃ x ∈ s, x ≤ 0) : sInf s ≤ 0
Full source 
/-- As `sInf s = 0` when `s` is a set of reals that's unbounded below, it suffices to show that `s`
contains a nonpositive element to show that `sInf s ≤ 0`. -/
lemma sInf_nonpos' (hs : ∃ x ∈ s, x ≤ 0) : sInf s ≤ 0 := by
  classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le
Infimum of Set with Nonpositive Element is Nonpositive
Informal description
For any nonempty set $s$ of real numbers containing a nonpositive element (i.e., there exists $x \in s$ such that $x \leq 0$), the infimum of $s$ satisfies $\inf s \leq 0$.
Real.iInf_nonpos' theorem
(hf : ∃ i, f i ≤ 0) : ⨅ i, f i ≤ 0
Full source 
/-- As `⨅ i, f i = 0` when the real-valued function `f` is unbounded below,
it suffices to show that `f` takes a nonpositive value to show that `0 ≤ ⨅ i, f i`. -/
lemma iInf_nonpos' (hf : ∃ i, f i ≤ 0) : ⨅ i, f i ≤ 0 := sInf_nonpos' <| Set.exists_range_iff.2 hf
Nonpositivity condition for indexed infimum: $\bigsqcap_i f(i) \leq 0$ if $f$ takes a nonpositive value
Informal description
For any real-valued function $f$ indexed by $i$, if there exists an index $i$ such that $f(i) \leq 0$, then the infimum of $f$ satisfies $\bigsqcap_i f(i) \leq 0$.
Real.sSup_nonneg theorem
(hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sSup s
Full source 
/-- As `sSup s = 0` when `s` is a set of reals that's either empty or unbounded above,
it suffices to show that all elements of `s` are nonnegative to show that `0 ≤ sSup s`. -/
lemma sSup_nonneg (hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sSup s := by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact sSup_empty.ge
  · exact sSup_nonneg' ⟨x, hx, hs _ hx⟩
Nonnegativity of Supremum for Nonnegative Sets
Informal description
For any set $s$ of real numbers, if every element $x \in s$ satisfies $0 \leq x$, then the supremum of $s$ satisfies $0 \leq \sup s$.
Real.iSup_nonneg theorem
(hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i
Full source 
/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty or unbounded above,
it suffices to show that all values of `f` are nonnegative to show that `0 ≤ ⨆ i, f i`. -/
lemma iSup_nonneg (hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i := sSup_nonneg <| Set.forall_mem_range.2 hf
Nonnegativity of Indexed Supremum: $\bigsqcup_i f(i) \geq 0$ for Nonnegative $f$
Informal description
For any real-valued function $f$ indexed by $i$, if $f(i) \geq 0$ for all $i$, then the supremum of $f$ satisfies $0 \leq \bigsqcup_i f(i)$.
Real.sInf_nonpos theorem
(hs : ∀ x ∈ s, x ≤ 0) : sInf s ≤ 0
Full source 
/-- As `sInf s = 0` when `s` is a set of reals that's either empty or unbounded below,
it suffices to show that all elements of `s` are nonpositive to show that `sInf s ≤ 0`. -/
lemma sInf_nonpos (hs : ∀ x ∈ s, x ≤ 0) : sInf s ≤ 0 := by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact sInf_empty.le
  · exact sInf_nonpos' ⟨x, hx, hs _ hx⟩
Infimum of Nonpositive Set is Nonpositive
Informal description
For any set $s$ of real numbers where every element $x \in s$ satisfies $x \leq 0$, the infimum of $s$ satisfies $\inf s \leq 0$.
Real.iInf_nonpos theorem
(hf : ∀ i, f i ≤ 0) : ⨅ i, f i ≤ 0
Full source 
/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty or unbounded below,
it suffices to show that all values of `f` are nonpositive to show that `0 ≤ ⨅ i, f i`. -/
lemma iInf_nonpos (hf : ∀ i, f i ≤ 0) : ⨅ i, f i ≤ 0 := sInf_nonpos <| Set.forall_mem_range.2 hf
Nonpositive Function Implies Nonpositive Infimum
Informal description
For any real-valued function $f$ indexed by $i$, if $f(i) \leq 0$ for all $i$, then the infimum of $f$ satisfies $\bigsqcap_i f(i) \leq 0$.
Real.sInf_le_sSup theorem
(s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) : sInf s ≤ sSup s
Full source 
theorem sInf_le_sSup (s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) : sInf s ≤ sSup s := by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · rw [sInf_empty, sSup_empty]
  · exact csInf_le_csSup h₁ h₂ hne
Infimum-Supremum Inequality for Bounded Real Sets
Informal description
For any nonempty set $s \subseteq \mathbb{R}$ that is both bounded below and bounded above, the infimum of $s$ is less than or equal to the supremum of $s$, i.e., $\inf s \leq \sup s$.
Real.cauSeq_converges theorem
(f : CauSeq ℝ abs) : ∃ x, f ≈ const abs x
Full source 
theorem cauSeq_converges (f : CauSeq ℝ abs) : ∃ x, f ≈ const abs x := by
  let s := {x : ℝ | const abs x < f}
  have lb : ∃ x, x ∈ s := exists_lt f
  have ub' : ∀ x, f < const abs x → ∀ y ∈ s, y ≤ x := fun x h y yS =>
    le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
  have ub : ∃ x, ∀ y ∈ s, y ≤ x := (exists_gt f).imp ub'
  refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩
  · rcases h with ⟨ε, ε0, i, ih⟩
    refine (csSup_le lb (ub' _ ?_)).not_lt (sub_lt_self _ (half_pos ε0))
    refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
    rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
    exact ih _ ij
  · rcases h with ⟨ε, ε0, i, ih⟩
    refine (le_csSup ub ?_).not_lt ((lt_add_iff_pos_left _).2 (half_pos ε0))
    refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
    rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]
    exact ih _ ij
Completeness of Real Numbers: Every Cauchy Sequence Converges
Informal description
For every Cauchy sequence $f$ of real numbers (with respect to the absolute value metric), there exists a real number $x$ such that $f$ converges to $x$. That is, $\lim_{n \to \infty} f_n = x$.
Real.instIsCompleteAbs instance
: CauSeq.IsComplete ℝ abs
Full source 
instance : CauSeq.IsComplete ℝ abs :=
  ⟨cauSeq_converges⟩
Completeness of the Real Numbers with Absolute Value Metric
Informal description
The real numbers $\mathbb{R}$ with the absolute value metric form a complete metric space. That is, every Cauchy sequence of real numbers converges to a real number.
Real.iInf_Ioi_eq_iInf_rat_gt theorem
{f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Ioi x)) (hf_mono : Monotone f) : ⨅ r : Ioi x, f r = ⨅ q : { q' : ℚ // x < q' }, f q
Full source 
theorem iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Ioi x))
    (hf_mono : Monotone f) : ⨅ r : Ioi x, f r = ⨅ q : { q' : ℚ // x < q' }, f q := by
  refine le_antisymm ?_ ?_
  · have : Nonempty { r' : ℚ // x < ↑r' } := by
      obtain ⟨r, hrx⟩ := exists_rat_gt x
      exact ⟨⟨r, hrx⟩⟩
    refine le_ciInf fun r => ?_
    obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop
    refine ciInf_set_le hf (hxy.trans ?_)
    exact_mod_cast hyr
  · refine le_ciInf fun q => ?_
    have hq := q.prop
    rw [mem_Ioi] at hq
    obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq
    refine (ciInf_le ?_ ?_).trans ?_
    · refine ⟨hf.some, fun z => ?_⟩
      rintro ⟨u, rfl⟩
      suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
      exact ⟨u, u.prop, rfl⟩
    · exact ⟨y, hxy⟩
    · refine hf_mono (le_trans ?_ hyq.le)
      norm_cast
Infimum Equality for Monotone Functions over Real and Rational Intervals
Informal description
Let $f : \mathbb{R} \to \mathbb{R}$ be a monotone function and $x \in \mathbb{R}$. If the image of the open interval $(x, \infty)$ under $f$ is bounded below, then the infimum of $f$ over $(x, \infty)$ is equal to the infimum of $f$ over all rational numbers $q > x$, i.e., \[ \inf_{r > x} f(r) = \inf_{q \in \mathbb{Q}, q > x} f(q). \]
Real.not_bddAbove_coe theorem
: ¬(BddAbove <| range (fun (x : ℚ) ↦ (x : ℝ)))
Full source 
theorem not_bddAbove_coe : ¬ (BddAbove <| range (fun (x : ℚ) ↦ (x : ℝ))) := by
  dsimp only [BddAbove, upperBounds]
  rw [Set.not_nonempty_iff_eq_empty]
  ext
  simpa using exists_rat_gt _
Unboundedness of Rationals in Reals
Informal description
The range of the canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is not bounded above. In other words, there is no real number $M$ such that $x \leq M$ for all $x \in \mathbb{Q}$ when viewed as elements of $\mathbb{R}$.
Real.not_bddBelow_coe theorem
: ¬(BddBelow <| range (fun (x : ℚ) ↦ (x : ℝ)))
Full source 
theorem not_bddBelow_coe : ¬ (BddBelow <| range (fun (x : ℚ) ↦ (x : ℝ))) := by
  dsimp only [BddBelow, lowerBounds]
  rw [Set.not_nonempty_iff_eq_empty]
  ext
  simpa using exists_rat_lt _
Unboundedness Below of Rational Embedding in Reals
Informal description
The range of the canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is not bounded below. That is, the set $\{x \in \mathbb{R} \mid \exists q \in \mathbb{Q}, x = q\}$ has no lower bound.
Real.iUnion_Iic_rat theorem
: ⋃ r : ℚ, Iic (r : ℝ) = univ
Full source 
theorem iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by
  exact iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe
Union of Rational Left-Infinite Intervals Covers Reals
Informal description
The union of all left-infinite right-closed intervals \( (-\infty, r] \) for \( r \in \mathbb{Q} \) (viewed as real numbers) equals the universal set. In other words: \[ \bigcup_{r \in \mathbb{Q}} (-\infty, r] = \mathbb{R}. \]
Real.iInter_Iic_rat theorem
: ⋂ r : ℚ, Iic (r : ℝ) = ∅
Full source 
theorem iInter_Iic_rat : ⋂ r : ℚ, Iic (r : ℝ) = ∅ := by
  exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe
Empty Intersection of Rational Right-Closed Intervals in Reals
Informal description
The intersection of all left-infinite right-closed intervals $(-\infty, r]$ for $r \in \mathbb{Q}$ (considered as real numbers) is the empty set, i.e., \[ \bigcap_{r \in \mathbb{Q}} (-\infty, r] = \emptyset. \]
Real.exists_natCast_add_one_lt_pow_of_one_lt theorem
(ha : 1 < a) : ∃ m : ℕ, (m + 1 : ℝ) < a ^ m
Full source 
/-- Exponentiation is eventually larger than linear growth. -/
lemma exists_natCast_add_one_lt_pow_of_one_lt (ha : 1 < a) : ∃ m : ℕ, (m + 1 : ℝ) < a ^ m := by
  obtain ⟨k, posk, hk⟩ : ∃ k : ℕ, 0 < k ∧ 1 / k + 1 < a := by
    contrapose! ha
    refine le_of_forall_lt_rat_imp_le ?_
    intro q hq
    refine (ha q.den (by positivity)).trans ?_
    rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
    norm_cast at hq ⊢
    rw [← q.num_div_den, one_lt_div (by positivity)] at hq
    rw [q.mul_den_eq_num]
    norm_cast at hq ⊢
    omega
  use 2 * k ^ 2
  calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr
Existence of Natural Number $m$ with $m + 1 < a^m$ for $a > 1$
Informal description
For any real number $a > 1$, there exists a natural number $m$ such that $m + 1 < a^m$.
Real.exists_nat_pos_inv_lt theorem
{b : ℝ} (hb : 0 < b) : ∃ (n : ℕ), 0 < n ∧ (n : ℝ)⁻¹ < b
Full source 
lemma exists_nat_pos_inv_lt {b : ℝ} (hb : 0 < b) :
    ∃ (n : ℕ), 0 < n ∧ (n : ℝ)⁻¹ < b := by
  refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_
  have := (inv_pos_of_pos hb).trans hk
  refine ⟨Nat.cast_pos.mp this, ?_⟩
  rwa [inv_lt_comm₀ this hb]
Existence of Natural Number with Small Reciprocal: $n^{-1} < b$ for $b > 0$
Informal description
For any positive real number $b > 0$, there exists a positive natural number $n$ such that the reciprocal of $n$ (as a real number) is less than $b$, i.e., $n^{-1} < b$.