noncomputable def RealAnalysis.monoLtRatSeq (x : ℝ) (n : ℕ) : ℚ

Equations

• RealAnalysis.monoLtRatSeq x n = Classical.epsilon fun (r : ℚ) => x - 1 / 2 ^ n < ↑r ∧ ↑r < x - 1 / 2 ^ (n + 1)

theorem RealAnalysis.monoLtRatSeq_cnd {x : ℝ} {n : ℕ} : ∃ (r : ℚ), x - 1 / 2 ^ n < ↑r ∧ ↑r < x - 1 / 2 ^ (n + 1)

theorem RealAnalysis.monoLtRatSeq_btwn {x : ℝ} {n : ℕ} : x - 1 / 2 ^ n < ↑(monoLtRatSeq x n) ∧ ↑(monoLtRatSeq x n) < x - 1 / 2 ^ (n + 1)

theorem RealAnalysis.lt_monoLtRatSeq {x : ℝ} {n : ℕ} : x - 1 / 2 ^ n < ↑(monoLtRatSeq x n)

theorem RealAnalysis.monoLtRatSeq_lt {x : ℝ} {n : ℕ} : ↑(monoLtRatSeq x n) < x - 1 / 2 ^ (n + 1)

theorem RealAnalysis.lt_monoLtRatSeq₀ {x : ℝ} {n : ℕ} : x - 1 < ↑(monoLtRatSeq x n)

theorem RealAnalysis.monoLtRatSeq_lt₀ {x : ℝ} {n : ℕ} : ↑(monoLtRatSeq x n) < x

theorem RealAnalysis.monoLtRatSeq_lt_succ {x : ℝ} {n : ℕ} : monoLtRatSeq x n < monoLtRatSeq x (n + 1)

theorem RealAnalysis.monoLtRatSeq_lt_of_lt {x : ℝ} {k n : ℕ} (h : k < n) : monoLtRatSeq x k < monoLtRatSeq x n

theorem RealAnalysis.monoLt_monoLtRatSeq {x : ℝ} : monoLt fun (x_1 : ℕ) => ↑(monoLtRatSeq x x_1)

theorem RealAnalysis.tendsTo_monoLtRatSeq {x : ℝ} : tendsTo (fun (x_1 : ℕ) => ↑(monoLtRatSeq x x_1)) x

theorem RealAnalysis.exi_monoLt_rat_tendsTo_real {x : ℝ} : ∃ (a : ℕ → ℚ), (monoLt fun (x : ℕ) => ↑(a x)) ∧ tendsTo (fun (x : ℕ) => ↑(a x)) x

theorem RealAnalysis.exi_monoLe_rat_tendsTo_real {x : ℝ} : ∃ (a : ℕ → ℚ), (monoLe fun (x : ℕ) => ↑(a x)) ∧ tendsTo (fun (x : ℕ) => ↑(a x)) x

noncomputable def RealAnalysis.ratApprox (b : ℕ) (x : ℝ) (n : ℕ) : ℚ

Equations

• RealAnalysis.ratApprox b x n = ↑⌊x * ↑b ^ n⌋₊ / ↑b ^ n

theorem RealAnalysis.ratApprox_le {b : ℕ} {x : ℝ} {n : ℕ} (hb : 2 ≤ b) (hx : 0 ≤ x) : ↑(ratApprox b x n) ≤ x

theorem RealAnalysis.lt_ratApprox {b : ℕ} {x : ℝ} {n : ℕ} (hb : 2 ≤ b) : x - 1 / ↑b ^ n < ↑(ratApprox b x n)

theorem RealAnalysis.tendsTo_ratApprox {b : ℕ} {x : ℝ} (hb : 2 ≤ b) (hx : 0 ≤ x) : tendsTo (fun (x_1 : ℕ) => ↑(ratApprox b x x_1)) x