noncomputable def RealAnalysis.altInv (n : ℕ) : ℝ

Equations

• RealAnalysis.altInv n = (-1) ^ n * (↑n + 1)⁻¹

@[simp]

theorem RealAnalysis.altInv_zero : altInv 0 = 1

@[simp]

theorem RealAnalysis.altInv_one : altInv 1 = -2⁻¹

theorem RealAnalysis.tendsTo_zero_iff_abs_tendsTo {a : ℕ → ℝ} : tendsTo a 0 ↔ tendsTo |a| 0

@[simp]

theorem RealAnalysis.abs_altInv {n : ℕ} : |altInv n| = (↑n + 1)⁻¹

@[simp]

theorem RealAnalysis.altInv_tendsTo_zero : tendsTo altInv 0

@[simp]

theorem RealAnalysis.converges_altInv : converges altInv

@[simp]

theorem RealAnalysis.converges_series_altInv : converges (series altInv)

theorem RealAnalysis.converges_series_fn_mul_two_of_nonneg {a : ℕ → ℝ} {L : ℝ} (h₁ : ∀ (n : ℕ), 0 ≤ a n) (h₂ : tendsTo (series a) L) : converges (series fun (x : ℕ) => a (x * 2))

theorem RealAnalysis.converges_series_fn_mul_two_add_one_of_nonneg {a : ℕ → ℝ} {L : ℝ} (h₁ : ∀ (n : ℕ), 0 ≤ a n) (h₂ : tendsTo (series a) L) : converges (series fun (x : ℕ) => a (x * 2 + 1))

theorem RealAnalysis.tendsTo_of_bounded_top {a : ℕ → ℝ} {L : ℝ} (h₂ : ∀ (n : ℕ), a n ≤ L) (h₃ : ∀ (ε : ℝ), 0 < ε → eventually fun (n : ℕ) => L - ε < a n) : tendsTo a L

theorem RealAnalysis.tendsTo_of_bounded_bottom {a : ℕ → ℝ} {L : ℝ} (h₂ : ∀ (n : ℕ), L ≤ a n) (h₃ : ∀ (ε : ℝ), 0 < ε → eventually fun (n : ℕ) => a n < L + ε) : tendsTo a L

theorem RealAnalysis.tendsTo_iff_bounded_top {a : ℕ → ℝ} {L : ℝ} (h : ∀ (n : ℕ), a n ≤ L) : tendsTo a L ↔ ∀ (ε : ℝ), 0 < ε → eventually fun (n : ℕ) => L - ε < a n

theorem RealAnalysis.tendsTo_iff_bounded_bottom {a : ℕ → ℝ} {L : ℝ} (h : ∀ (n : ℕ), L ≤ a n) : tendsTo a L ↔ ∀ (ε : ℝ), 0 < ε → eventually fun (n : ℕ) => a n < L + ε

theorem RealAnalysis.tendsTo_series_fn_add {a : ℕ → ℝ} {L : ℝ} (h₂ : tendsTo (series a) L) : tendsTo (series fun (n : ℕ) => a (n * 2) + a (n * 2 + 1)) L

theorem RealAnalysis.exi_tendsTo_series_fn_add_of_nonneg {a : ℕ → ℝ} {L : ℝ} (h₂ : tendsTo (series a) L) (h₁ : ∀ (n : ℕ), 0 ≤ a n) : ∃ (L₁ : ℝ) (L₂ : ℝ), L₁ + L₂ = L ∧ tendsTo (series fun (x : ℕ) => a (x * 2)) L₁ ∧ tendsTo (series fun (x : ℕ) => a (x * 2 + 1)) L₂

theorem RealAnalysis.series_smul {a : ℕ → ℝ} {x : ℝ} : (series fun (x_1 : ℕ) => a x_1 * x) = fun (n : ℕ) => series a n * x

theorem RealAnalysis.series_sdiv {a : ℕ → ℝ} {x : ℝ} : (series fun (x_1 : ℕ) => a x_1 / x) = fun (n : ℕ) => series a n / x

theorem RealAnalysis.tendsTo_smul {a : ℕ → ℝ} {L x : ℝ} (h : tendsTo a L) : tendsTo (fun (x_1 : ℕ) => a x_1 * x) (L * x)

theorem RealAnalysis.tendsTo_sdiv {a : ℕ → ℝ} {L x : ℝ} (h : tendsTo a L) : tendsTo (fun (x_1 : ℕ) => a x_1 / x) (L / x)

theorem RealAnalysis.exi_tendsTo_le_of_monoLe_and_forall_le {a b : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo b L) (h₂ : monoLe a) (h₃ : ∀ (n : ℕ), a n ≤ b n) : ∃ M ≤ L, tendsTo a M

theorem RealAnalysis.series_fn_add {a b : ℕ → ℝ} : series (a + b) = series a + series b

@[simp]

theorem RealAnalysis.series_one {a : ℕ → ℝ} : series a 1 = a 0

theorem RealAnalysis.exi_series_tendsTo_lt_of_forall_lt {a b : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo (series b) L) (h₂ : ∀ (n : ℕ), 0 ≤ b n) (h₃ : ∀ (n : ℕ), 0 ≤ a n) (h₄ : ∀ (n : ℕ), a n < b n) : ∃ M < L, tendsTo (series a) M

@[simp]

theorem RealAnalysis.not_converges_series_inv : ¬converges (series fun (n : ℕ) => (↑n + 1)⁻¹)

@[simp]

theorem RealAnalysis.not_absConv_altInv : ¬AbsConv altInv

@[simp]

theorem RealAnalysis.condConv_altInv : CondConv altInv