@[reducible, inline]

noncomputable abbrev halvingCount (a : ℕ → ℝ) (m : ℕ) : ℕ

Helper for Lemma 11.7: the number of halving steps among the first m transitions.

@[reducible, inline]

noncomputable abbrev strictHalfRatioCount (a : ℕ → ℝ) (m : ℕ) : ℕ

Helper for Lemma 11.7: the number of strict-half-ratio steps among the first m transitions.

theorem quadratic_step_recurrence_antitone {a : ℕ → ℝ} {γ : ↑PosReal} (hstep : ∀ (k : ℕ), a k - a (k + 1) ≥ 1 / ↑γ * a (k + 1) ^ 2) : Antitone a

Helper for Lemma 11.7: the quadratic recurrence makes the sequence antitone.

theorem reciprocal_increment_ge_one_div_two_gamma_of_strict_half_ratio {a : ℕ → ℝ} {γ : ↑PosReal} (hstep : ∀ (k : ℕ), a k - a (k + 1) ≥ 1 / ↑γ * a (k + 1) ^ 2) (k : ℕ) (hak : 0 < a k) (hak_succ : 0 < a (k + 1)) (hhalf : a k / 2 < a (k + 1)) : 1 / (2 * ↑γ) ≤ 1 / a (k + 1) - 1 / a k

Helper for Lemma 11.7: a strict-half-ratio step yields a uniform reciprocal increment.

theorem geometric_prefix_bound_of_halving_count {a : ℕ → ℝ} {γ : ↑PosReal} (hstep : ∀ (k : ℕ), a k - a (k + 1) ≥ 1 / ↑γ * a (k + 1) ^ 2) (m : ℕ) : a m ≤ (1 / 2) ^ halvingCount a m * a 0

Helper for Lemma 11.7: every halving step contributes one factor 1 / 2 to the prefix bound.

theorem reciprocal_prefix_bound_of_strict_half_ratio_count {a : ℕ → ℝ} {γ : ↑PosReal} (hstep : ∀ (k : ℕ), a k - a (k + 1) ≥ 1 / ↑γ * a (k + 1) ^ 2) (m : ℕ) (hm_pos : 0 < a m) : ↑(strictHalfRatioCount a m) / (2 * ↑γ) ≤ 1 / a m - 1 / a 0

Helper for Lemma 11.7: every strict-half-ratio step contributes one reciprocal increment of size at least 1 / (2γ).

theorem geometric_term_le_epsilon_of_log_bound {a0 : ℝ} (ha0 : 0 < a0) (ε : ↑PosReal) {m : ℕ} (hlog : 2 / Real.log 2 * (Real.log a0 + Real.log (1 / ↑ε)) ≤ ↑m) : (1 / 2) ^ (↑m / 2) * a0 ≤ ↑ε

Helper for Lemma 11.7: the logarithmic lower bound on the iteration count forces the geometric term below ε.

theorem nonnegative_sequence_le_max_geometric_or_sublinear_of_quadratic_step_recurrence {a : ℕ → ℝ} {γ : ↑PosReal} (ha_nonneg : ∀ (k : ℕ), 0 ≤ a k) (hstep : ∀ (k : ℕ), a k - a (k + 1) ≥ 1 / ↑γ * a (k + 1) ^ 2) {n : ℕ} (hn : 2 ≤ n) : a n ≤ max ((1 / 2) ^ (↑(n - 1) / 2) * a 0) (4 * ↑γ / ↑(n - 1))

Lemma 11.7 (1): if a nonnegative scalar sequence satisfies a k - a (k + 1) ≥ (1 / γ) * a (k + 1)^2 for every k and some positive γ, then for every n ≥ 2 one has a n ≤ max {((1 / 2)^((n - 1) / 2)) * a 0, 4γ / (n - 1)}.

theorem nonnegative_sequence_le_epsilon_of_quadratic_step_recurrence {a : ℕ → ℝ} {γ : ↑PosReal} (ha_nonneg : ∀ (k : ℕ), 0 ≤ a k) (hstep : ∀ (k : ℕ), a k - a (k + 1) ≥ 1 / ↑γ * a (k + 1) ^ 2) (ε : ↑PosReal) {n : ℕ} (hn : max (2 / Real.log 2 * (Real.log (a 0) + Real.log (1 / ↑ε))) (4 * ↑γ / ↑ε) + 1 ≤ ↑n) : a n ≤ ↑ε

Lemma 11.7 (2): if ε > 0 and n ≥ max {(2 / log 2) * (log (a 0) + log (1 / ε)), 4γ / ε} + 1, then the same recurrence implies a n ≤ ε.