def RealAnalysis.isCauchy (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.isCauchy a = ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (i j : ℕ), N ≤ i → N ≤ j → |a i - a j| < ε

def RealAnalysis.isCauchyAlt₁ (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.isCauchyAlt₁ a = ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |a n - a N| < ε

def RealAnalysis.isCauchyAlt₂ (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.isCauchyAlt₂ a = ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ∀ (j : ℕ), N ≤ j → |a i - a j| < ε

def RealAnalysis.isCauchyAlt₃ (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.isCauchyAlt₃ a = ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ∀ (j : ℕ), i ≤ j → |a i - a j| < ε

theorem RealAnalysis.isCauchy_iff_alt₁ {a : ℕ → ℝ} : isCauchy a ↔ isCauchyAlt₁ a

theorem RealAnalysis.isCauchy_iff_alt₂ {a : ℕ → ℝ} : isCauchy a ↔ isCauchyAlt₂ a

theorem RealAnalysis.isCauchy_iff_alt₃ {a : ℕ → ℝ} : isCauchy a ↔ isCauchyAlt₃ a

theorem RealAnalysis.isCauSeq_of_isCauchy {a : ℕ → ℚ} (h : isCauchy fun (x : ℕ) => ↑(a x)) : IsCauSeq abs a

theorem RealAnalysis.isCauchy_of_isCauSeq {a : ℕ → ℚ} (h : IsCauSeq abs a) : isCauchy fun (x : ℕ) => ↑(a x)

theorem RealAnalysis.isCauSeq_iff_isCauchy {a : ℕ → ℚ} : IsCauSeq abs a ↔ isCauchy fun (x : ℕ) => ↑(a x)

theorem RealAnalysis.forall_eps_iff {p : ℝ → Prop} (h : ∀ {ε₁ ε₂ : ℝ}, 0 < ε₁ → ε₁ < ε₂ → p ε₁ → p ε₂) : (∀ (ε : ℝ), 0 < ε → p ε) ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → p ε

def RealAnalysis.isFakeCauchy (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.isFakeCauchy a = ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → |a i - a (i + 1)| < ε

theorem RealAnalysis.isFakeCauchy_iff {a : ℕ → ℝ} : isFakeCauchy a ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → |a i - a (i + 1)| < ε

theorem RealAnalysis.isFakeCauchy_sqrt : isFakeCauchy fun (x : ℕ) => √↑x

theorem RealAnalysis.isCauchy_of_converges {a : ℕ → ℝ} (h : converges a) : isCauchy a

theorem RealAnalysis.bounded_of_isCauchy {a : ℕ → ℝ} (h : isCauchy a) : bounded a

theorem RealAnalysis.tendsTo_of_isCauchy_and_subseq_tendsTo {a : ℕ → ℝ} {σ : ℕ → ℕ} {L : ℝ} (hσ : Subseq σ) (ha : isCauchy a) (h : tendsTo (a ∘ σ) L) : tendsTo a L

theorem RealAnalysis.tendsTo_of_converges_and_subseq_tendsTo {a : ℕ → ℝ} {σ : ℕ → ℕ} {L : ℝ} (hσ : Subseq σ) (ha : converges a) (h : tendsTo (a ∘ σ) L) : tendsTo a L

theorem RealAnalysis.converges_of_isCauchy {a : ℕ → ℝ} (h : isCauchy a) : converges a

theorem RealAnalysis.isCauchy_iff_converges {a : ℕ → ℝ} : isCauchy a ↔ converges a

theorem RealAnalysis.converges_iff_isCauchy {a : ℕ → ℝ} : converges a ↔ isCauchy a

theorem RealAnalysis.not_converges_sqrt : ¬converges fun (x : ℕ) => √↑x

theorem RealAnalysis.not_isCauchy_sqrt : ¬isCauchy fun (x : ℕ) => √↑x

theorem RealAnalysis.isFakeCauchy_ne_isCauchy : isFakeCauchy ≠ isCauchy

theorem RealAnalysis.isCauchy_add {a b : ℕ → ℝ} (ha : isCauchy a) (hb : isCauchy b) : isCauchy (a + b)

@[simp]

theorem RealAnalysis.isCauchy_neg {a : ℕ → ℝ} : isCauchy (-a) ↔ isCauchy a

theorem RealAnalysis.isCauchy_of_monoLe_and_bounded_top {a : ℕ → ℝ} (h₁ : monoLe a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), a n ≤ M) : isCauchy a

theorem RealAnalysis.isCauchy_of_monoGe_and_bounded_bottom {a : ℕ → ℝ} (h₁ : monoGe a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), M ≤ a n) : isCauchy a

theorem RealAnalysis.isCauchy_of_monoLt_and_bounded_top {a : ℕ → ℝ} (h₁ : monoLt a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), a n ≤ M) : isCauchy a

theorem RealAnalysis.isCauchy_of_monoGt_and_bounded_bottom {a : ℕ → ℝ} (h₁ : monoGt a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), M ≤ a n) : isCauchy a

theorem RealAnalysis.converges_of_monoLe_and_bounded_top {a : ℕ → ℝ} (h₁ : monoLe a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), a n ≤ M) : converges a

theorem RealAnalysis.converges_of_monoGe_and_bounded_bottom {a : ℕ → ℝ} (h₁ : monoGe a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), M ≤ a n) : converges a

theorem RealAnalysis.converges_of_monoLt_and_bounded_top {a : ℕ → ℝ} (h₁ : monoLt a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), a n ≤ M) : converges a

theorem RealAnalysis.converges_of_monoGt_and_bounded_bottom {a : ℕ → ℝ} (h₁ : monoGt a) (h₂ : ∃ (M : ℝ), ∀ (n : ℕ), M ≤ a n) : converges a

theorem RealAnalysis.isCauSeq_rat_iff {a : ℕ → ℚ} : IsCauSeq abs a ↔ ∀ (ε : ℚ), 0 < ε → ∃ (N : ℕ), ∀ (i j : ℕ), N ≤ i → N ≤ j → |a i - a j| < ε