noncomputable def RealAnalysis.bounds (a : ℕ → ℝ) (n : ℕ) : ℝ

Equations

• RealAnalysis.bounds a n = RealAnalysis.lub |fun (x : ℕ) => a (n + x)|

theorem RealAnalysis.bounds_le_bounds_of_tendsTo {a : ℕ → ℝ} {L : ℝ} {k n : ℕ} (h₁ : tendsTo a L) (h₂ : k ≤ n) : bounds a n ≤ bounds a k

theorem RealAnalysis.bounds_le_bounds_of_converges {a : ℕ → ℝ} {k n : ℕ} (h₁ : converges a) (h₂ : k ≤ n) : bounds a n ≤ bounds a k

theorem RealAnalysis.abs_le_bounds_of_tendsTo {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h : tendsTo a L) : |a n| ≤ bounds a n

theorem RealAnalysis.abs_le_bounds_of_converges {a : ℕ → ℝ} {n : ℕ} (h : converges a) : |a n| ≤ bounds a n

theorem RealAnalysis.tendsTo_lub_seq_of_nonneg {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) : tendsTo (fun (n : ℕ) => lub fun (x : ℕ) => a (n + x)) L

theorem RealAnalysis.tendsTo_bounds_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : tendsTo (bounds a) |L|

@[simp]

theorem RealAnalysis.bounds_abs {a : ℕ → ℝ} : bounds |a| = bounds a

theorem RealAnalysis.bounds_nonneg_of_tendsTo {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h : tendsTo a L) : 0 ≤ bounds a n

theorem RealAnalysis.bounds_nonneg_of_converges {a : ℕ → ℝ} {n : ℕ} (h : converges a) : 0 ≤ bounds a n

theorem RealAnalysis.abs_bounds_of_tendsTo {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h : tendsTo a L) : |bounds a n| = bounds a n

theorem RealAnalysis.abs_bounds_of_converges {a : ℕ → ℝ} {n : ℕ} (h : converges a) : |bounds a n| = bounds a n

theorem RealAnalysis.monoGe_bounds_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : monoGe (bounds a)

theorem RealAnalysis.monoGe_bounds_of_converges {a : ℕ → ℝ} (h : converges a) : monoGe (bounds a)

@[simp]

theorem RealAnalysis.bounds_neg {a : ℕ → ℝ} : bounds (-a) = bounds a