Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib.

theorem LongTails.OracleTemplate.GeneralizedAccelerated.exp_sub_one_le_mul_exp (d : ℝ) : Real.exp d - 1 ≤ d * Real.exp d

theorem LongTails.OracleTemplate.GeneralizedAccelerated.nat_cube_le_exp_two (q : ℕ) : ↑q ^ 3 ≤ 48 * 2 ^ q

theorem LongTails.OracleTemplate.GeneralizedAccelerated.logarithmic_charge_cube {u d : ℝ} (hu : 0 < u) (hd : 0 < d) (q : ℕ) (h : 2 ^ q ≤ 64 * √u * (Real.exp d - 1)) : max 0 (↑q - 4 * d) ^ 3 ≤ 262144 * u * d ^ 2

theorem LongTails.OracleTemplate.GeneralizedAccelerated.ordered_log_telescope {ι : Type u_1} (s : Finset ι) (time : ι → ℕ) (w : ι → ℝ) (B : ℝ) (hinj : Set.InjOn time ↑s) : ∑ i ∈ s, (Real.log (B + ∑ j ∈ s with time j ≤ time i, w j) - Real.log (B + ∑ j ∈ s with time j < time i, w j)) = Real.log (B + ∑ i ∈ s, w i) - Real.log B

theorem LongTails.OracleTemplate.GeneralizedAccelerated.ordered_log_increments {ι : Type u_1} (s : Finset ι) (time : ι → ℕ) (w : ι → ℝ) {B : ℝ} (hB : 0 < B) (hw : ∀ i ∈ s, 0 < w i) (hinj : Set.InjOn time ↑s) : ∑ i ∈ s, Real.log (1 + w i / (B + ∑ j ∈ s with time j < time i, w j)) = Real.log ((B + ∑ i ∈ s, w i) / B)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.high_count_self_normalized {ι : Type u_1} (s : Finset ι) (time : ι → ℕ) (A G : ι → ℝ) (q : ι → ℕ) {A0 Afinal H : ℝ} (hA0 : 0 < A0) (hAF : A0 ≤ Afinal) (hA : ∀ i ∈ s, A0 ≤ A i) (hG : ∀ i ∈ s, 0 < G i) (hH : 0 ≤ H) (hinj : Set.InjOn time ↑s) (henergy : ∑ i ∈ s, A i * G i ≤ H) (hweights : ∑ i ∈ s, 2 ^ q i / √(G i) ≤ 32 * √Afinal) (hprefix : ∀ i ∈ s, ∑ j ∈ s with time j < time i, 2 ^ q j / √(G j) ≤ 32 * √(A i)) : have D := Real.log (2 * Afinal / A0); ∑ i ∈ s, ↑(q i) ≤ 4 * D + 64 * (H * D ^ 2) ^ (1 / 3)