noncomputable def RealAnalysis.bwSeq (a : ℕ → ℝ) (y₁ y₂ : ℚ) (n : ℕ) : ℚ × ℚ

Equations

• RealAnalysis.bwSeq a y₁ y₂ 0 = (y₁, y₂)
• RealAnalysis.bwSeq a y₁ y₂ n_2.succ = if {i : ℕ | ↑y₁ ≤ a i ∧ a i ≤ ↑((y₁ + y₂) / 2)}.Infinite then RealAnalysis.bwSeq a y₁ ((y₁ + y₂) / 2) n_2 else RealAnalysis.bwSeq a ((y₁ + y₂) / 2) y₂ n_2

noncomputable def RealAnalysis.bwLimit (a : ℕ → ℝ) (M : ℚ) : ℝ

Equations

• RealAnalysis.bwLimit a M = if h : IsCauSeq abs fun (x : ℕ) => (RealAnalysis.bwSeq a (-M) M x).1 then Real.mk ⟨fun (x : ℕ) => (RealAnalysis.bwSeq a (-M) M x).1, h⟩ else 0

@[irreducible]

noncomputable def RealAnalysis.bwSubseq (a : ℕ → ℝ) (M : ℚ) (n : ℕ) : ℕ

Equations

• RealAnalysis.bwSubseq a M n = Classical.epsilon fun (i : ℕ) => (∀ k < n, RealAnalysis.bwSubseq a M k < i) ∧ match RealAnalysis.bwSeq a (-M) M n with | (y₁, y₂) => ↑y₁ ≤ a i ∧ a i ≤ ↑y₂

theorem RealAnalysis.le_bwSeq_fst {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n : ℕ} (hy : y₁ < y₂) : y₁ ≤ (bwSeq a y₁ y₂ n).1

theorem RealAnalysis.bwSeq_snd_le {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ n).2 ≤ y₂

theorem RealAnalysis.bwSeq_add {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n k : ℕ} (hy : y₁ < y₂) : bwSeq a y₁ y₂ (n + k) = bwSeq a (bwSeq a y₁ y₂ n).1 (bwSeq a y₁ y₂ n).2 k

theorem RealAnalysis.bwSeq_fst_lt_snd' {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ n).1 < (bwSeq a y₁ y₂ n).2

theorem RealAnalysis.bwSeq_fst_le_of_le {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n m : ℕ} (hy : y₁ < y₂) (hn : m ≤ n) : (bwSeq a y₁ y₂ m).1 ≤ (bwSeq a y₁ y₂ n).1

theorem RealAnalysis.le_bwSeq_snd_of_le {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n m : ℕ} (hy : y₁ < y₂) (hn : m ≤ n) : (bwSeq a y₁ y₂ n).2 ≤ (bwSeq a y₁ y₂ m).2

theorem RealAnalysis.fst_lt_snd_of_bwSeq_eq {a : ℕ → ℝ} {y₁ y₂ y₁' y₂' : ℚ} {n : ℕ} (hy : y₁ < y₂) (h : bwSeq a y₁ y₂ n = (y₁', y₂')) : y₁' < y₂'

theorem RealAnalysis.bwSeq_snd_sub_fst_eq {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ n).2 - (bwSeq a y₁ y₂ n).1 = (y₂ - y₁) / 2 ^ n

theorem RealAnalysis.bwSeq_fst_eq_snd_sub {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ n).1 = (bwSeq a y₁ y₂ n).2 - (y₂ - y₁) / 2 ^ n

theorem RealAnalysis.bwSeq_snd_eq_fst_sub {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ n).2 = (bwSeq a y₁ y₂ n).1 + (y₂ - y₁) / 2 ^ n

theorem RealAnalysis.bwSeq_add_fst_sub_lt {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n k : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ (n + k)).1 - (bwSeq a y₁ y₂ n).1 < (y₂ - y₁) / 2 ^ n

theorem RealAnalysis.isCauSeq_bwSeq_fst {a : ℕ → ℝ} {y₁ y₂ : ℚ} (hy : y₁ < y₂) : IsCauSeq abs fun (x : ℕ) => (bwSeq a y₁ y₂ x).1

theorem RealAnalysis.isCauSeq_bwSeq_fst_of_abs_lt {a : ℕ → ℝ} {M : ℚ} (h : ∀ (n : ℕ), |a n| < ↑M) : IsCauSeq abs fun (x : ℕ) => (bwSeq a (-M) M x).1

theorem RealAnalysis.infinite_between_of_bwSeq_eq {a : ℕ → ℝ} {y₁ y₂ y₁' y₂' : ℚ} {n : ℕ} (hy : y₁ < y₂) (ha : {i : ℕ | ↑y₁ ≤ a i ∧ a i ≤ ↑y₂}.Infinite) (hr : bwSeq a y₁ y₂ n = (y₁', y₂')) : {i : ℕ | ↑y₁' ≤ a i ∧ a i ≤ ↑y₂'}.Infinite

theorem RealAnalysis.infinite_between_of_bwSeq_eq_of_abs_lt {a : ℕ → ℝ} {M y₁ y₂ : ℚ} {n : ℕ} (h : ∀ (n : ℕ), |a n| < ↑M) (hr : bwSeq a (-M) M n = (y₁, y₂)) : {i : ℕ | ↑y₁ ≤ a i ∧ a i ≤ ↑y₂}.Infinite

theorem RealAnalysis.bwSubseq_cnd' {a : ℕ → ℝ} {M : ℚ} {n : ℕ} (h : ∀ (n : ℕ), |a n| < ↑M) : ∃ (i : ℕ), (∀ k < n, bwSubseq a M k < i) ∧ match bwSeq a (-M) M n with | (y₁, y₂) => ↑y₁ ≤ a i ∧ a i ≤ ↑y₂

theorem RealAnalysis.bwSubseq_cnd {a : ℕ → ℝ} {M : ℚ} {n : ℕ} (h : ∀ (n : ℕ), |a n| < ↑M) : (∀ k < n, bwSubseq a M k < bwSubseq a M n) ∧ match bwSeq a (-M) M n with | (y₁, y₂) => ↑y₁ ≤ a (bwSubseq a M n) ∧ a (bwSubseq a M n) ≤ ↑y₂

theorem RealAnalysis.bwSubseq_lt_of_lt {a : ℕ → ℝ} {M : ℚ} {i j : ℕ} (h : ∀ (n : ℕ), |a n| < ↑M) (h₁ : i < j) : bwSubseq a M i < bwSubseq a M j

theorem RealAnalysis.subseq_bwSubseq {a : ℕ → ℝ} {M : ℚ} (h : ∀ (n : ℕ), |a n| < ↑M) : Subseq (bwSubseq a M)

theorem RealAnalysis.bwSeq_fst_lt_snd {a : ℕ → ℝ} {y₁ y₂ : ℚ} {n m : ℕ} (hy : y₁ < y₂) : (bwSeq a y₁ y₂ n).1 < (bwSeq a y₁ y₂ m).2

theorem RealAnalysis.bwLimit_eq_of {a : ℕ → ℝ} {M : ℚ} (h : ∀ (n : ℕ), |a n| < ↑M) : bwLimit a M = Real.mk ⟨fun (x : ℕ) => (bwSeq a (-M) M x).1, ⋯⟩

theorem RealAnalysis.bwSeq_fst_le_bwLimit {a : ℕ → ℝ} {M : ℚ} {n : ℕ} (h : ∀ (n : ℕ), |a n| < ↑M) : ↑(bwSeq a (-M) M n).1 ≤ bwLimit a M

theorem RealAnalysis.bwLimit_le_bwSeq_snd {a : ℕ → ℝ} {M : ℚ} {n : ℕ} (h : ∀ (n : ℕ), |a n| < ↑M) : bwLimit a M ≤ ↑(bwSeq a (-M) M n).2

theorem RealAnalysis.exi_converges_subseq_of_bounded {a : ℕ → ℝ} (h : bounded a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ converges (a ∘ σ)