abstract real lemmas for the main-theorem assembly Pure real-variable statements used by the

assembly: the telescoping lower bound s_n ≥ (1 - ∑ e_i) s_j, the geometric tail estimate, and the passage from a lower bound along a sequence tending to 0⁺ to a lower bound for the limsup.

theorem AVenhance.Infra.Section5.RelativeError.telescope_lower {s e : ℕ → ℝ} {j N : ℕ} (hs : 0 ≤ s j) (he0 : ∀ (i : ℕ), j ≤ i → i < N → 0 ≤ e i) (he1 : ∀ (i : ℕ), j ≤ i → i < N → e i ≤ 1) (hstep : ∀ (i : ℕ), j ≤ i → i < N → (1 - e i) * s i ≤ s (i + 1)) (n : ℕ) (hn : j + n ≤ N) : (1 - ∑ i ∈ Finset.range n, e (j + i)) * s j ≤ s (j + n)

Telescoping lower bound from s_{i+1} ≥ (1 - e_i) s_i for j ≤ i < N, with 0 ≤ e_i ≤ 1 there: the product is bounded below by 1 - ∑ e_i.

theorem AVenhance.Infra.Section5.RelativeError.geom_tail_le {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ < 1) (j n : ℕ) : ∑ i ∈ Finset.range n, ρ ^ (j + i) ≤ ρ ^ j / (1 - ρ)

Geometric tail: ∑_{i<n} ρ^{j+i} ≤ ρ^j/(1-ρ).

theorem AVenhance.Infra.Section5.RelativeError.weighted_geom_tail_le {C ρ : ℝ} (hC : 0 ≤ C) (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ 1 / 2) (hCρ : C * ρ ≤ 1 / 4) {j : ℕ} (hj : 1 ≤ j) (n : ℕ) : C * ∑ i ∈ Finset.range n, ρ ^ (j + i) ≤ 1 / 2

Smallness of the weighted geometric tail starting at index j ≥ 1.

theorem AVenhance.Infra.Section5.RelativeError.eventually_mul_rpow_le {x : ℕ → ℝ} (hx : Filter.Tendsto x Filter.atTop (nhds 0)) {e : ℝ} (he : 0 < e) (A : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (m : ℕ) in Filter.atTop, A * x m ^ e ≤ δ

If x_m → 0 through positive reals and e > 0 then A x_m^e is eventually below any positive bound.

theorem AVenhance.Infra.Section5.RelativeError.tendsto_rpow_nhdsGT {x : ℕ → ℝ} (hx0 : ∀ (m : ℕ), 0 < x m) (hx : Filter.Tendsto x Filter.atTop (nhds 0)) {s : ℝ} (hs : 0 < s) : Filter.Tendsto (fun (m : ℕ) => x m ^ s) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

A positive sequence tending to 0 has positive powers tending to 0⁺.

theorem AVenhance.Infra.Section5.RelativeError.le_limsup_of_seq {F : ℝ → ℝ} {κ : ℕ → ℝ} (hκ : Filter.Tendsto κ Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) {B U : ℝ} (hU : ∀ᶠ (k : ℝ) in nhdsWithin 0 (Set.Ioi 0), F k ≤ U) (hlow : ∀ᶠ (m : ℕ) in Filter.atTop, B ≤ F (κ m)) : B ≤ Filter.limsup F (nhdsWithin 0 (Set.Ioi 0))

A lower bound along a sequence tending to 0⁺ passes to the limsup at 0⁺, given an upper bound for the function near 0⁺.