def RealAnalysis.series (a : ℕ → ℝ) (n : ℕ) : ℝ

Equations

• RealAnalysis.series a n = ∑ i ∈ Finset.range n, a i

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

Equations

• RealAnalysis.AbsConv a = RealAnalysis.converges (RealAnalysis.series fun (x : ℕ) => |a x|)

theorem RealAnalysis.series_eq {a : ℕ → ℝ} : series a = fun (n : ℕ) => ∑ i ∈ Finset.range n, a i

@[simp]

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

theorem RealAnalysis.series_succ {a : ℕ → ℝ} {n : ℕ} : series a (n + 1) = series a n + a n

@[simp]

theorem RealAnalysis.series_const {x : ℝ} {n : ℕ} : series (fun (x_1 : ℕ) => x) n = ↑n * x

theorem RealAnalysis.tendsTo_zero_of_converges_series {a : ℕ → ℝ} (h : converges (series a)) : tendsTo a 0

@[simp]

theorem RealAnalysis.inv_add_tendsTo_zero {x : ℝ} : tendsTo (fun (n : ℕ) => (↑n + x)⁻¹) 0

theorem RealAnalysis.add_div_add_tendsTo_one_aux₁ {x y : ℝ} (hy : 0 < y) : tendsTo (fun (n : ℕ) => (↑n + x) / (↑n + y)) 1

@[simp]

theorem RealAnalysis.add_div_add_tendsTo_one {x y : ℝ} : tendsTo (fun (n : ℕ) => (↑n + x) / (↑n + y)) 1

@[simp]

theorem RealAnalysis.add_div_tendsTo_one {x : ℝ} : tendsTo (fun (n : ℕ) => (↑n + x) / ↑n) 1

@[simp]

theorem RealAnalysis.div_add_tendsTo_one {x : ℝ} : tendsTo (fun (n : ℕ) => ↑n / (↑n + x)) 1

theorem RealAnalysis.leibniz_sum {n : ℕ} : ∑ i ∈ Finset.range n, 1 / ((↑i + 1) * (↑i + 2)) = ↑n / (↑n + 1)

theorem RealAnalysis.leibniz_sum' {n : ℕ} : ∑ i ∈ Finset.range n, 1 / ((↑i + 1) * (↑i + 2)) = 1 - 1 / (↑n + 1)

theorem RealAnalysis.leibniz_series_tendsTo : tendsTo (series fun (n : ℕ) => 1 / ((↑n + 1) * (↑n + 2))) 1

theorem RealAnalysis.series_le_of_le {a b : ℕ → ℝ} {n : ℕ} (h₁ : ∀ (n : ℕ), a n ≤ b n) : series a n ≤ series b n

theorem RealAnalysis.converges_of_monoLe_and_forall_le_add {a b : ℕ → ℝ} {x : ℝ} (h₁ : converges b) (h₂ : monoLe a) (h₃ : ∀ (n : ℕ), a n ≤ b n + x) : converges a

theorem RealAnalysis.converges_of_monoLe_and_forall_le {a b : ℕ → ℝ} (h₁ : converges b) (h₂ : monoLe a) (h₃ : ∀ (n : ℕ), a n ≤ b n) : converges a

theorem RealAnalysis.series_add {a : ℕ → ℝ} {n k : ℕ} : series a (n + k) = series a n + series (fun (x : ℕ) => a (n + x)) k

theorem RealAnalysis.series_add' {a : ℕ → ℝ} {n k : ℕ} : series a (n + k) = series a k + series (fun (x : ℕ) => a (k + x)) n

theorem RealAnalysis.converges_basel {x : ℝ} : converges (series fun (n : ℕ) => 1 / (↑n + x) ^ 2)

@[simp]

theorem RealAnalysis.subseq_add_right {k : ℕ} : Subseq fun (x : ℕ) => x + k

@[simp]

theorem RealAnalysis.subseq_add_left {k : ℕ} : Subseq fun (x : ℕ) => k + x

@[simp]

theorem RealAnalysis.subseq_mul_right {k : ℕ} (h : k ≠ 0) : Subseq fun (x : ℕ) => x * k

@[simp]

theorem RealAnalysis.subseq_mul_left {k : ℕ} (h : k ≠ 0) : Subseq fun (x : ℕ) => k * x

theorem RealAnalysis.pow_tendsTo_zero_of_pos_and_lt_one {x : ℝ} (h₁ : 0 < x) (h₂ : x < 1) : tendsTo (fun (x_1 : ℕ) => x ^ x_1) 0

theorem RealAnalysis.geom_series_eq {x : ℝ} {n : ℕ} (h : x ≠ 1) : series (fun (x_1 : ℕ) => x ^ x_1) n = (1 - x ^ n) / (1 - x)

theorem RealAnalysis.geom_series_eq_ext {x : ℝ} (h : x ≠ 1) : (series fun (x_1 : ℕ) => x ^ x_1) = fun (n : ℕ) => (1 - x ^ n) / (1 - x)

theorem RealAnalysis.geom_series_tendsTo {x : ℝ} (h₁ : 0 < x) (h₂ : x < 1) : tendsTo (series fun (x_1 : ℕ) => x ^ x_1) (1 / (1 - x))

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

theorem RealAnalysis.tendsTo_zero_of_abs_tendsTo {a : ℕ → ℝ} (h : tendsTo (fun (x : ℕ) => |a x|) 0) : tendsTo a 0

theorem RealAnalysis.abs_tendsTo_zero_iff {a : ℕ → ℝ} : tendsTo (fun (x : ℕ) => |a x|) 0 ↔ tendsTo a 0

theorem RealAnalysis.le_limit_of_monoLe' {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h₁ : monoLe a) (h₂ : tendsTo a L) : a n ≤ L

theorem RealAnalysis.limit_le_of_monoGe' {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h₁ : monoGe a) (h₂ : tendsTo a L) : L ≤ a n

theorem RealAnalysis.le_limit_of_monoLe {a : ℕ → ℝ} {L : ℝ} (h₁ : monoLe a) (h₂ : tendsTo a L) (n : ℕ) : a n ≤ L

theorem RealAnalysis.limit_le_of_monoGe {a : ℕ → ℝ} {L : ℝ} (h₁ : monoGe a) (h₂ : tendsTo a L) (n : ℕ) : L ≤ a n

@[simp]

theorem RealAnalysis.monoLe_series_abs {a : ℕ → ℝ} : monoLe (series fun (x : ℕ) => |a x|)

@[simp]

theorem RealAnalysis.monoLe_series_abs' {a : ℕ → ℝ} : monoLe (series |a|)

theorem RealAnalysis.abs_series_le_series_abs {a : ℕ → ℝ} {n : ℕ} : |series a n| ≤ series (fun (x : ℕ) => |a x|) n

theorem RealAnalysis.converges_series_of_absConv {a : ℕ → ℝ} (h : AbsConv a) : converges (series a)

theorem RealAnalysis.series_sub_series_of_le {a : ℕ → ℝ} {n m : ℕ} (h : n ≤ m) : series a m - series a n = ∑ i ∈ Finset.Ico n m, a i

theorem RealAnalysis.sum_range_mul_two_alternating {a : ℕ → ℝ} {m : ℕ} : ∑ k ∈ Finset.range (m * 2), (-1) ^ k * a k = ∑ k ∈ Finset.range m, (a (k * 2) - a (k * 2 + 1))

theorem RealAnalysis.subseq_lt_of_lt {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : i < j) : σ i < σ j

theorem RealAnalysis.subseq_le_of_le {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : i ≤ j) : σ i ≤ σ j

theorem RealAnalysis.subseq_eq_of_eq {σ : ℕ → ℕ} {i j : ℕ} (h₂ : i = j) : σ i = σ j

theorem RealAnalysis.eq_of_subseq_eq {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : σ i = σ j) : i = j

theorem RealAnalysis.subseq_eq_iff {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) : σ i = σ j ↔ i = j

theorem RealAnalysis.lt_of_subseq_lt {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : σ i < σ j) : i < j

theorem RealAnalysis.subseq_lt_iff {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) : σ i < σ j ↔ i < j

theorem RealAnalysis.le_of_subseq_le {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : σ i ≤ σ j) : i ≤ j

theorem RealAnalysis.subseq_le_iff {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) : σ i ≤ σ j ↔ i ≤ j

theorem RealAnalysis.subseq_ne_of_ne {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : i ≠ j) : σ i ≠ σ j

theorem RealAnalysis.ne_of_subseq_ne {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) (h₂ : σ i ≠ σ j) : i ≠ j

theorem RealAnalysis.subseq_ne_iff {σ : ℕ → ℕ} {i j : ℕ} (h₁ : Subseq σ) : σ i ≠ σ j ↔ i ≠ j

theorem RealAnalysis.monoLe_subseq {a : ℕ → ℝ} {σ : ℕ → ℕ} (h₁ : monoLe a) (h₂ : Subseq σ) : monoLe fun (x : ℕ) => a (σ x)

theorem RealAnalysis.monoGe_subseq {a : ℕ → ℝ} {σ : ℕ → ℕ} (h₁ : monoGe a) (h₂ : Subseq σ) : monoGe fun (x : ℕ) => a (σ x)

theorem RealAnalysis.monoLt_subseq {a : ℕ → ℝ} {σ : ℕ → ℕ} (h₁ : monoLt a) (h₂ : Subseq σ) : monoLt fun (x : ℕ) => a (σ x)

theorem RealAnalysis.monoGt_subseq {a : ℕ → ℝ} {σ : ℕ → ℕ} (h₁ : monoGt a) (h₂ : Subseq σ) : monoGt fun (x : ℕ) => a (σ x)

theorem RealAnalysis.limit_eq_of_sub_tendsTo_zero {a b : ℕ → ℝ} {L M : ℝ} (h₁ : tendsTo a L) (h₂ : tendsTo b M) (h₃ : tendsTo (a - b) 0) : L = M

theorem RealAnalysis.converges_series_alternating_of_monoGe.aux₁ {a : ℕ → ℝ} {n : ℕ} (h₁ : monoGe a) (h₂ : tendsTo a 0) : 0 ≤ a n

theorem RealAnalysis.converges_series_alternating_of_monoGe.aux₂ {a : ℕ → ℝ} {n : ℕ} {f : ℕ → ℕ} (h₁ : monoGe a) : 0 ≤ ∑ k ∈ Finset.range n, (a (f k) - a (f k + 1))

theorem RealAnalysis.converges_series_alternating_of_monoGe.aux₃ {a : ℕ → ℝ} {n : ℕ} (h₁ : monoGe a) (h₂ : tendsTo a 0) : 0 ≤ ∑ k ∈ Finset.range n, (-1) ^ k * a k

theorem RealAnalysis.converges_series_alternating_of_monoGe.aux₄ {a : ℕ → ℝ} {n : ℕ} (h₁ : monoGe a) (h₂ : tendsTo a 0) : ∑ k ∈ Finset.range n, (-1) ^ k * a k ≤ a 0

theorem RealAnalysis.converges_series_alternating_of_monoGe {a : ℕ → ℝ} (h₁ : monoGe a) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

@[simp]

theorem RealAnalysis.neg_series' {a : ℕ → ℝ} : -series a = series (-a)

@[simp]

theorem RealAnalysis.neg_series {a : ℕ → ℝ} {n : ℕ} : -series a n = series (-a) n

theorem RealAnalysis.converges_series_alternating_of_monoLe {a : ℕ → ℝ} (h₁ : monoLe a) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

theorem RealAnalysis.converges_series_alternating_of_monoGt {a : ℕ → ℝ} (h₁ : monoGt a) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

theorem RealAnalysis.converges_series_alternating_of_monoLt {a : ℕ → ℝ} (h₁ : monoLt a) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

theorem RealAnalysis.series_drop_eq {a : ℕ → ℝ} {N : ℕ} : (series fun (x : ℕ) => a (N + x)) = fun (n : ℕ) => series a (N + n) - series a N

theorem RealAnalysis.series_drop_tendsTo_of {a : ℕ → ℝ} {L : ℝ} {N : ℕ} (h : tendsTo (series a) L) : tendsTo (series fun (x : ℕ) => a (N + x)) (L - series a N)

theorem RealAnalysis.series_drop_tendsTo_iff {a : ℕ → ℝ} {L : ℝ} {N : ℕ} : tendsTo (series fun (x : ℕ) => a (N + x)) L ↔ tendsTo (series a) (L + series a N)

theorem RealAnalysis.converges_series_drop_iff {a : ℕ → ℝ} {N : ℕ} : converges (series fun (x : ℕ) => a (N + x)) ↔ converges (series a)

theorem RealAnalysis.converges_series_alternating_of_monoLe_drop {a : ℕ → ℝ} {N : ℕ} (h₁ : monoLe fun (x : ℕ) => a (N + x)) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

theorem RealAnalysis.converges_series_alternating_of_monoGe_drop {a : ℕ → ℝ} {N : ℕ} (h₁ : monoGe fun (x : ℕ) => a (N + x)) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

theorem RealAnalysis.converges_series_alternating_of_monoLt_drop {a : ℕ → ℝ} {N : ℕ} (h₁ : monoLt fun (x : ℕ) => a (N + x)) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

theorem RealAnalysis.converges_series_alternating_of_monoGt_drop {a : ℕ → ℝ} {N : ℕ} (h₁ : monoGt fun (x : ℕ) => a (N + x)) (h₂ : tendsTo a 0) : converges (series fun (n : ℕ) => (-1) ^ n * a n)

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

theorem RealAnalysis.tendsTo_odd_of {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : tendsTo (fun (x : ℕ) => a (x * 2 + 1)) L