Geometric summability of the construction scales (the use of e.minsep in the §2 limit argument).

theorem AVenhance.Infra.Construction.LimitSeries.epsilon_pos_for_ingredients {β : ℝ} (I : Ingredients β) (m : ℕ) : 0 < epsilon β I.Λ m

theorem AVenhance.Infra.Construction.epsilon_step_le {β : ℝ} (I : Ingredients β) (m : ℕ) : epsilon β I.Λ (m + 1) ≤ epsilon β I.Λ m / ↑I.Λ

e.minsep: one step of the scale sequence contracts by Λ.

theorem AVenhance.Infra.Construction.epsilon_rpow_step_le {β s : ℝ} (I : Ingredients β) (hs : 0 < s) (m : ℕ) : epsilon β I.Λ (m + 1) ^ s ≤ epsilon β I.Λ m ^ s * ↑I.Λ ^ (-s)

The scale powers contract geometrically for every positive real exponent.

theorem AVenhance.Infra.Construction.epsilon_rpow_le_geom {β s : ℝ} (I : Ingredients β) (hs : 0 < s) (m k : ℕ) : epsilon β I.Λ (m + k) ^ s ≤ epsilon β I.Λ m ^ s * (↑I.Λ ^ (-s)) ^ k

Repeated e.minsep, in a form ready for comparison with a geometric series.

theorem AVenhance.Infra.Construction.LimitSeries.sum_geom_le {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (n : ℕ) : ∑ k ∈ Finset.range n, q ^ k ≤ 1 / (1 - q)

theorem AVenhance.Infra.Construction.epsilon_rpow_sum_bound {β s : ℝ} (I : Ingredients β) (hs : 0 < s) (m n : ℕ) : ∑ k ∈ Finset.range n, epsilon β I.Λ (m + k) ^ s ≤ epsilon β I.Λ m ^ s / (1 - ↑I.Λ ^ (-s))

The source's e.minsep series estimate, with the tail based at an arbitrary scale. In particular, taking m = 1 gives Σ_{j=1}^N ε_j^s ≤ ε_1^s/(1-Λ^{-s}).

theorem AVenhance.Infra.Construction.inverse_lambda_rpow_lt_one {β s : ℝ} (I : Ingredients β) (hs : 0 < s) : ↑I.Λ ^ (-s) < 1

theorem AVenhance.Infra.Construction.epsilon_rpow_antitone {β s : ℝ} (I : Ingredients β) (hs : 0 < s) {m n : ℕ} (hmn : m ≤ n) : epsilon β I.Λ n ^ s ≤ epsilon β I.Λ m ^ s

Positive powers of the scales decrease with the index.

theorem AVenhance.Infra.Construction.epsilon_rpow_tendsto_zero {β s : ℝ} (I : Ingredients β) (hs : 0 < s) : Filter.Tendsto (fun (m : ℕ) => epsilon β I.Λ m ^ s) Filter.atTop (nhds 0)

The scales and all their positive real powers tend to zero.