def RealAnalysis.Rment (σ : ℕ → ℕ) : Prop

Equations

• RealAnalysis.Rment σ = Function.Bijective σ

noncomputable def RealAnalysis.rinv (σ : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• RealAnalysis.rinv σ n = Classical.epsilon fun (k : ℕ) => σ k = n

noncomputable def RealAnalysis.mkRmentP (a : ℕ → ℝ) (is : List ℕ) : ℕ

Equations

• RealAnalysis.mkRmentP a is = Nat.find! fun (i : ℕ) => i ∉ is ∧ 0 ≤ a i

noncomputable def RealAnalysis.mkRmentN (a : ℕ → ℝ) (is : List ℕ) : ℕ

Equations

• RealAnalysis.mkRmentN a is = Nat.find! fun (j : ℕ) => j ∉ is ∧ a j < 0

noncomputable def RealAnalysis.mkRmentList1 (a : ℕ → ℝ) (is : List ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentList1 a is = is ++ [RealAnalysis.mkRmentP a is, RealAnalysis.mkRmentN a is]

noncomputable def RealAnalysis.mkRmentSum (a : ℕ → ℝ) (is : List ℕ) : ℝ

Equations

• RealAnalysis.mkRmentSum a is = (List.map a is).sum

def RealAnalysis.mkRmentLeNCnd (a : ℕ → ℝ) (n : ℕ) (is : List ℕ) (N : ℕ) : Prop

Equations

• RealAnalysis.mkRmentLeNCnd a n is N = (0 ≤ a N ∧ ∀ (r : ℕ), N ≤ r → 0 ≤ a r → r ∉ is ∧ a r < 1 / (↑n + 2))

def RealAnalysis.mkRmentGeNCnd (a : ℕ → ℝ) (n : ℕ) (is : List ℕ) (N : ℕ) : Prop

Equations

• RealAnalysis.mkRmentGeNCnd a n is N = (a N < 0 ∧ ∀ (r : ℕ), N ≤ r → a r < 0 → r ∉ is ∧ -1 / (↑n + 2) < a r)

noncomputable def RealAnalysis.mkRmentLeN (a : ℕ → ℝ) (n : ℕ) (is : List ℕ) : ℕ

Equations

• RealAnalysis.mkRmentLeN a n is = Nat.find! (RealAnalysis.mkRmentLeNCnd a n is)

noncomputable def RealAnalysis.mkRmentGeN (a : ℕ → ℝ) (n : ℕ) (is : List ℕ) : ℕ

Equations

• RealAnalysis.mkRmentGeN a n is = Nat.find! (RealAnalysis.mkRmentGeNCnd a n is)

noncomputable def RealAnalysis.mkRmentLeF (a : ℕ → ℝ) (n : ℕ) (is : List ℕ) (k : ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentLeF a n is k = List.filter (fun (x : ℕ) => decide (0 ≤ a x)) (List.map (fun (x : ℕ) => RealAnalysis.mkRmentLeN a n is + x) (List.range k))

noncomputable def RealAnalysis.mkRmentGeF (a : ℕ → ℝ) (n : ℕ) (is : List ℕ) (k : ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentGeF a n is k = List.filter (fun (x : ℕ) => decide (a x < 0)) (List.map (fun (x : ℕ) => RealAnalysis.mkRmentGeN a n is + x) (List.range k))

def RealAnalysis.mkRmentLeKCnd (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) (k : ℕ) : Prop

Equations

• RealAnalysis.mkRmentLeKCnd a L n is k = (L - 1 / (↑n + 2) < RealAnalysis.mkRmentSum a is + (List.map a (RealAnalysis.mkRmentLeF a n is k)).sum)

def RealAnalysis.mkRmentGeKCnd (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) (k : ℕ) : Prop

Equations

• RealAnalysis.mkRmentGeKCnd a L n is k = (RealAnalysis.mkRmentSum a is + (List.map a (RealAnalysis.mkRmentGeF a n is k)).sum < L + 1 / (↑n + 2))

noncomputable def RealAnalysis.mkRmentLeK (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) : ℕ

Equations

• RealAnalysis.mkRmentLeK a L n is = Nat.find! (RealAnalysis.mkRmentLeKCnd a L n is)

noncomputable def RealAnalysis.mkRmentGeK (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) : ℕ

Equations

• RealAnalysis.mkRmentGeK a L n is = Nat.find! (RealAnalysis.mkRmentGeKCnd a L n is)

noncomputable def RealAnalysis.mkRmentLe (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentLe a L n is = RealAnalysis.mkRmentLeF a n is (RealAnalysis.mkRmentLeK a L n is)

noncomputable def RealAnalysis.mkRmentGe (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentGe a L n is = RealAnalysis.mkRmentGeF a n is (RealAnalysis.mkRmentGeK a L n is)

noncomputable def RealAnalysis.mkRmentIte (a : ℕ → ℝ) (L : ℝ) (n : ℕ) (is : List ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentIte a L n is = is ++ if RealAnalysis.mkRmentSum a is ≤ L - 1 / (↑n + 2) then RealAnalysis.mkRmentLe a L n is else if L + 1 / (↑n + 2) ≤ RealAnalysis.mkRmentSum a is then RealAnalysis.mkRmentGe a L n is else []

noncomputable def RealAnalysis.mkRmentList (a : ℕ → ℝ) (L : ℝ) (n : ℕ) : List ℕ

Equations

• RealAnalysis.mkRmentList a L 0 = []
• RealAnalysis.mkRmentList a L n_2.succ = RealAnalysis.mkRmentIte a L n_2 (RealAnalysis.mkRmentList1 a (RealAnalysis.mkRmentList a L n_2))

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

Equations

• RealAnalysis.mkRment a L n = (RealAnalysis.mkRmentList a L (n + 1))[n]!

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

Equations

• RealAnalysis.mkRmentLen a L n = (RealAnalysis.mkRmentList a L n).length

theorem RealAnalysis.rment_eq_iff {σ : ℕ → ℕ} {n m : ℕ} (h : Rment σ) : σ n = σ m ↔ n = m

theorem RealAnalysis.rinv_cancel_left {σ : ℕ → ℕ} {n : ℕ} (h : Rment σ) : rinv σ (σ n) = n

theorem RealAnalysis.rinv_cancel_right {σ : ℕ → ℕ} {n : ℕ} (h : Rment σ) : σ (rinv σ n) = n

theorem RealAnalysis.rment_rinv {σ : ℕ → ℕ} (h : Rment σ) : Rment (rinv σ)

theorem RealAnalysis.tendsTo_rment_of {a : ℕ → ℝ} {σ : ℕ → ℕ} {L : ℝ} (h₁ : Rment σ) (h₂ : tendsTo a L) : tendsTo (fun (x : ℕ) => a (σ x)) L

theorem RealAnalysis.tendsTo_rment_iff {a : ℕ → ℝ} {σ : ℕ → ℕ} {L : ℝ} (h₁ : Rment σ) : tendsTo (fun (x : ℕ) => a (σ x)) L ↔ tendsTo a L

theorem RealAnalysis.converges_rment_of {a : ℕ → ℝ} {σ : ℕ → ℕ} (h₁ : Rment σ) (h₂ : converges a) : converges fun (x : ℕ) => a (σ x)

theorem RealAnalysis.converges_rment_iff {a : ℕ → ℝ} {σ : ℕ → ℕ} (h₁ : Rment σ) : (converges fun (x : ℕ) => a (σ x)) ↔ converges a

@[simp]

theorem RealAnalysis.le_length_mkRmentList {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : n ≤ (mkRmentList a L n).length

@[simp]

theorem RealAnalysis.le_mkRmentLen {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : n ≤ mkRmentLen a L n

theorem RealAnalysis.mkRmentList_prefix {a : ℕ → ℝ} {L : ℝ} {k n : ℕ} (h : k ≤ n) : mkRmentList a L k <+: mkRmentList a L n

theorem RealAnalysis.getElem!_mkRmentList_eq_getElem {a : ℕ → ℝ} {L : ℝ} {n k : ℕ} (h : k < n) : (mkRmentList a L n)[k]! = (mkRmentList a L n)[k]

@[simp]

theorem RealAnalysis.lt_length_mkRmentList_succ {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : n < (mkRmentList a L (n + 1)).length

@[simp]

theorem RealAnalysis.lt_mkRmentLen_succ {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : n < mkRmentLen a L (n + 1)

theorem RealAnalysis.mkRment_eq_getElem {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : mkRment a L n = (mkRmentList a L (n + 1))[n]

theorem RealAnalysis.getElem_mkRmentList_eq_of_lt {a : ℕ → ℝ} {L : ℝ} {n m k : ℕ} (h₁ : k < n) (h₂ : k < m) : (mkRmentList a L n)[k] = (mkRmentList a L m)[k]

theorem RealAnalysis.getElem!_mkRmentList_eq_of_lt {a : ℕ → ℝ} {L : ℝ} {n m k : ℕ} (h₁ : k < n) (h₂ : k < m) : (mkRmentList a L n)[k]! = (mkRmentList a L m)[k]!

theorem RealAnalysis.mkRmentP_spec' {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : (mkRmentP a is ∉ is ∧ 0 ≤ a (mkRmentP a is)) ∧ ∀ (k : ℕ), k ∉ is ∧ 0 ≤ a k → mkRmentP a is ≤ k

theorem RealAnalysis.mkRmentN_spec' {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : (mkRmentN a is ∉ is ∧ a (mkRmentN a is) < 0) ∧ ∀ (k : ℕ), k ∉ is ∧ a k < 0 → mkRmentN a is ≤ k

theorem RealAnalysis.mkRmentP_spec {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : mkRmentP a is ∉ is ∧ 0 ≤ a (mkRmentP a is)

theorem RealAnalysis.mkRmentN_spec {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : mkRmentN a is ∉ is ∧ a (mkRmentN a is) < 0

@[simp]

theorem RealAnalysis.mem_mkRmentList_succ {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : n ∈ mkRmentList a L (n + 1)

theorem RealAnalysis.getElem_mkRmentList_of_le.proof₁ {a : ℕ → ℝ} {L : ℝ} {n₁ n₂ k : ℕ} (h₁ : n₁ ≤ n₂) (h₂ : k < (mkRmentList a L n₁).length) : k < (mkRmentList a L n₂).length

theorem RealAnalysis.getElem_mkRmentList_of_le {a : ℕ → ℝ} {L : ℝ} {n₁ n₂ k : ℕ} {hh : k < (mkRmentList a L n₁).length} (h : n₁ ≤ n₂) : (mkRmentList a L n₁)[k] = (mkRmentList a L n₂)[k]

theorem RealAnalysis.getElem_mkRmentList_eq {a : ℕ → ℝ} {L : ℝ} {n₁ n₂ k : ℕ} {hh₁ : k < (mkRmentList a L n₁).length} {hh₂ : k < (mkRmentList a L n₂).length} : (mkRmentList a L n₁)[k] = (mkRmentList a L n₂)[k]

@[simp]

theorem RealAnalysis.getElem_mkRmentList_eq_iff_true {a : ℕ → ℝ} {L : ℝ} {n₁ n₂ k : ℕ} {hh₁ : k < (mkRmentList a L n₁).length} {hh₂ : k < (mkRmentList a L n₂).length} : (mkRmentList a L n₁)[k] = (mkRmentList a L n₂)[k] ↔ True

@[simp]

theorem RealAnalysis.mkRmentList_zero {a : ℕ → ℝ} {L : ℝ} : mkRmentList a L 0 = []

theorem RealAnalysis.mkRmentP_notMem {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : mkRmentP a is ∉ is

theorem RealAnalysis.mkRmentN_notMem {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : mkRmentN a is ∉ is

theorem RealAnalysis.mkRmentP_nonneg {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : 0 ≤ a (mkRmentP a is)

theorem RealAnalysis.mkRmentN_neg {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : a (mkRmentN a is) < 0

theorem RealAnalysis.mkRmentP_ne_mkRmentN {a : ℕ → ℝ} {is : List ℕ} (H : CondConv a) : mkRmentP a is ≠ mkRmentN a is

@[simp]

theorem RealAnalysis.nodup_mkRmentLe {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} : (mkRmentLe a L n is).Nodup

@[simp]

theorem RealAnalysis.nodup_mkRmentGe {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} : (mkRmentGe a L n is).Nodup

theorem RealAnalysis.mkRmentLeK_spec' {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : mkRmentLeKCnd a L n is (mkRmentLeK a L n is) ∧ ∀ (k : ℕ), mkRmentLeKCnd a L n is k → mkRmentLeK a L n is ≤ k

theorem RealAnalysis.mkRmentGeK_spec' {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : mkRmentGeKCnd a L n is (mkRmentGeK a L n is) ∧ ∀ (k : ℕ), mkRmentGeKCnd a L n is k → mkRmentGeK a L n is ≤ k

theorem RealAnalysis.mkRmentLeK_spec {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : L - 1 / (↑n + 2) < mkRmentSum a is + (List.map a (mkRmentLeF a n is (mkRmentLeK a L n is))).sum

theorem RealAnalysis.mkRmentGeK_spec {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : mkRmentSum a is + (List.map a (mkRmentGeF a n is (mkRmentGeK a L n is))).sum < L + 1 / (↑n + 2)

theorem RealAnalysis.mkRmentLeN_spec' {a : ℕ → ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : mkRmentLeNCnd a n is (mkRmentLeN a n is) ∧ ∀ (k : ℕ), mkRmentLeNCnd a n is k → mkRmentLeN a n is ≤ k

theorem RealAnalysis.mkRmentGeN_spec' {a : ℕ → ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : mkRmentGeNCnd a n is (mkRmentGeN a n is) ∧ ∀ (k : ℕ), mkRmentGeNCnd a n is k → mkRmentGeN a n is ≤ k

theorem RealAnalysis.mkRmentLeN_spec {a : ℕ → ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : 0 ≤ a (mkRmentLeN a n is) ∧ ∀ (r : ℕ), mkRmentLeN a n is ≤ r → 0 ≤ a r → r ∉ is ∧ a r < 1 / (↑n + 2)

theorem RealAnalysis.mkRmentGeN_spec {a : ℕ → ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : a (mkRmentGeN a n is) < 0 ∧ ∀ (r : ℕ), mkRmentGeN a n is ≤ r → a r < 0 → r ∉ is ∧ -1 / (↑n + 2) < a r

theorem RealAnalysis.notMem_mkRmentLe_of_mem {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} {i : ℕ} (H : CondConv a) (h : i ∈ is) : i ∉ mkRmentLe a L n is

theorem RealAnalysis.notMem_mkRmentGe_of_mem {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} {i : ℕ} (H : CondConv a) (h : i ∈ is) : i ∉ mkRmentGe a L n is

theorem RealAnalysis.nodup_mkRmentList {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (H : CondConv a) : (mkRmentList a L n).Nodup

theorem RealAnalysis.mkRment_eq_iff {a : ℕ → ℝ} {L : ℝ} {i j : ℕ} (H : CondConv a) : mkRment a L i = mkRment a L j ↔ i = j

theorem RealAnalysis.rment_mkRment {a : ℕ → ℝ} {L : ℝ} (h : CondConv a) : Rment (mkRment a L)

theorem RealAnalysis.series_mkRment_eq_sum {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : series (fun (i : ℕ) => a (mkRment a L i)) n = (List.map a (List.take n (mkRmentList a L n))).sum

theorem RealAnalysis.take_length_mkRmentList {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} (h : mkRmentList a L n = is) : List.take is.length (mkRmentList a L is.length) = is

@[simp]

theorem RealAnalysis.take_mkRmentLen_mkRmentList {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : List.take (mkRmentLen a L n) (mkRmentList a L (mkRmentLen a L n)) = mkRmentList a L n

@[simp]

theorem RealAnalysis.mkRmentLeF_zero {a : ℕ → ℝ} {n : ℕ} {is : List ℕ} : mkRmentLeF a n is 0 = []

@[simp]

theorem RealAnalysis.mkRmentGeF_zero {a : ℕ → ℝ} {n : ℕ} {is : List ℕ} : mkRmentGeF a n is 0 = []

theorem RealAnalysis.abs_map_sum_mkRmentLe_sub_lt {a : ℕ → ℝ} {L : ℝ} {is : List ℕ} {n : ℕ} (H : CondConv a) (h₁ : mkRmentSum a is ≤ L - (↑n + 2)⁻¹) : |(List.map a is).sum + (List.map a (mkRmentLe a L n is)).sum - L| ≤ (↑n + 2)⁻¹

theorem RealAnalysis.abs_map_sum_mkRmentGe_sub_lt {a : ℕ → ℝ} {L : ℝ} {is : List ℕ} {n : ℕ} (H : CondConv a) (h₁ : L + (↑n + 2)⁻¹ ≤ mkRmentSum a is) : |(List.map a is).sum + (List.map a (mkRmentGe a L n is)).sum - L| ≤ (↑n + 2)⁻¹

theorem RealAnalysis.abs_map_sum_mkRmentIte_sub_lt {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} (H : CondConv a) : |(List.map a (mkRmentIte a L n is)).sum - L| ≤ 1 / (↑n + 2)

theorem RealAnalysis.abs_map_sum_mkRmentList_sub_lt {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (H : CondConv a) (hn : n ≠ 0) : |(List.map a (mkRmentList a L n)).sum - L| ≤ 1 / (↑n + 1)

theorem RealAnalysis.abs_series_mkRment_mkRmentLen_sub_lt {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (H : CondConv a) (hn : n ≠ 0) : |series (fun (x : ℕ) => a (mkRment a L x)) (mkRmentLen a L n) - L| ≤ 1 / (↑n + 1)

theorem RealAnalysis.subseq_exi_ge {σ : ℕ → ℕ} {n : ℕ} (h : Subseq σ) : ∃ (k : ℕ), n ≤ σ k

theorem RealAnalysis.subseq_exi_gt {σ : ℕ → ℕ} {n : ℕ} (h : Subseq σ) : ∃ (k : ℕ), n < σ k

theorem RealAnalysis.subseq_exi_ge_and_between_of_le {σ : ℕ → ℕ} {n i : ℕ} (h₁ : Subseq σ) (h₂ : σ n ≤ i) : ∃ (k : ℕ), n ≤ k ∧ σ k ≤ i ∧ i < σ (k + 1)

@[simp]

theorem RealAnalysis.mkRmentLen_lt_succ {a : ℕ → ℝ} {L : ℝ} {n : ℕ} : mkRmentLen a L n < mkRmentLen a L (n + 1)

@[simp]

theorem RealAnalysis.subseq_mkRmentLen {a : ℕ → ℝ} {L : ℝ} : Subseq (mkRmentLen a L)

@[simp]

theorem RealAnalysis.take_mkRmentLen_mkRmentList_add {a : ℕ → ℝ} {L : ℝ} {n k : ℕ} : List.take (mkRmentLen a L n) (mkRmentList a L (n + k)) = mkRmentList a L n

theorem RealAnalysis.mem_mkRmentList_of_lt {a : ℕ → ℝ} {L : ℝ} {n k : ℕ} (h : k < n) : k ∈ mkRmentList a L n

theorem RealAnalysis.le_mkRmentP_mkRmentList {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (H : CondConv a) : n ≤ mkRmentP a (mkRmentList a L n)

theorem RealAnalysis.le_mkRmentN_mkRmentList {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (H : CondConv a) : n ≤ mkRmentN a (mkRmentList a L n)

theorem RealAnalysis.nonneg_of_mem_mkRmentLe {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} {i : ℕ} (h : i ∈ mkRmentLe a L n is) : 0 ≤ a i

theorem RealAnalysis.neg_of_mem_mkRmentGe {a : ℕ → ℝ} {L : ℝ} {n : ℕ} {is : List ℕ} {i : ℕ} (h : i ∈ mkRmentGe a L n is) : a i < 0

theorem RealAnalysis.abs_series_add_sum_mkRmentList_sub_lt.aux₁ {a : ℕ → ℝ} {L : ℝ} {n N k i j : ℕ} {s₀ s s₁ : ℝ} {is is₁ : List ℕ} {d : ℝ} (H : CondConv a) (h₂ : mkRmentSum a (mkRmentList a L n) = s₀) (h₁ : mkRmentList a L n = is) (_hN : is.length = N) (h₃ : |s₀ - L| ≤ (↑n + 1)⁻¹) (ha : tendsTo a 0) (hi : mkRmentP a is = i) (hj : mkRmentN a is = j) (h₄ : is ++ [i, j] = is₁) (hs : mkRmentSum a is₁ = s) (hd : (↑n + 2)⁻¹ = d) (hs₁ : (List.take k (List.map a (mkRmentLe a L n is₁))).sum = s₁) (H₂ : s ≤ L - d) : |s₁| ≤ 4 * bounds a n + 2 * (↑n + 1)⁻¹

theorem RealAnalysis.abs_series_add_sum_mkRmentList_sub_lt.aux₂ {a : ℕ → ℝ} {L : ℝ} {n N k i j : ℕ} {s₀ s s₁ : ℝ} {is is₁ : List ℕ} {d : ℝ} (H : CondConv a) (h₂ : mkRmentSum a (mkRmentList a L n) = s₀) (h₁ : mkRmentList a L n = is) (_hN : is.length = N) (h₃ : |s₀ - L| ≤ (↑n + 1)⁻¹) (ha : tendsTo a 0) (hi : mkRmentP a is = i) (hj : mkRmentN a is = j) (h₄ : is ++ [i, j] = is₁) (hs : mkRmentSum a is₁ = s) (hd : (↑n + 2)⁻¹ = d) (hs₁ : (List.take k (List.map a (mkRmentGe a L n is₁))).sum = s₁) (H₂ : L + d ≤ s) : |s₁| ≤ 4 * bounds a n + 2 * (↑n + 1)⁻¹

theorem RealAnalysis.abs_series_add_sum_mkRmentList_sub_lt {a : ℕ → ℝ} {L : ℝ} {n N k : ℕ} (H : CondConv a) (hN : mkRmentLen a L n = N) (hn : n ≠ 0) : |series (fun (x : ℕ) => a (mkRment a L x)) N + (List.map a (List.take k (List.drop N (mkRmentList a L (n + 1))))).sum - L| ≤ 8 * bounds a n + 4 * (↑n + 1)⁻¹

theorem RealAnalysis.abs_series_mkRment_sub_lt_of_between {a : ℕ → ℝ} {L : ℝ} {n i : ℕ} (H : CondConv a) (hn : n ≠ 0) (h₁ : mkRmentLen a L n ≤ i) (h₂ : i < mkRmentLen a L (n + 1)) : |series (fun (x : ℕ) => a (mkRment a L x)) i - L| ≤ 8 * bounds a n + 4 * (↑n + 1)⁻¹

theorem RealAnalysis.abs_series_mkRment_sub_lt_of_le {a : ℕ → ℝ} {L : ℝ} {n i : ℕ} (H : CondConv a) (hn : n ≠ 0) (h : mkRmentLen a L n ≤ i) : |series (fun (x : ℕ) => a (mkRment a L x)) i - L| ≤ 8 * bounds a n + 4 * (↑n + 1)⁻¹

theorem RealAnalysis.tendsTo_series_mkRment {a : ℕ → ℝ} {L : ℝ} (H : CondConv a) : tendsTo (series fun (i : ℕ) => a (mkRment a L i)) L

theorem RealAnalysis.exi_rment_tendsTo_of_condConv {a : ℕ → ℝ} {L : ℝ} (H : CondConv a) : ∃ (σ : ℕ → ℕ), Rment σ ∧ tendsTo (series fun (x : ℕ) => a (σ x)) L