Abstract real lemmas for the flip-flop #

abs_log_one_add_le: |x| ≤ 1/2 → |log (1+x)| ≤ 2|x|;
const_mul_inv_rpow_le_one: K Λ^{-s} ≤ 1 once Λ ≥ K^{1/s};
flipflop_unroll: the alternating telescoping with a tail-summable error sequence.

theorem AVenhance.Infra.FullTheorem.FlipFlop.const_mul_inv_rpow_le_one {K s Λ : ℝ} (hK : 0 < K) (hs : 0 < s) (hΛ0 : 0 < Λ) (hΛ : K ^ (1 / s) ≤ Λ) :

K * Λ⁻¹ ^ s ≤ 1

theorem AVenhance.Infra.FullTheorem.FlipFlop.flipflop_unroll (u e : ℕ → ℝ) (L B T : ℝ) (M : ℕ) (hB : 0 ≤ B) (htail : ∀ (m n : ℕ), ∑ k ∈ Finset.range n, e (m + k) ≤ T * e m) (htop : |u (M - 1) - L| ≤ B * e (M - 1)) (hstep : ∀ (n : ℕ), 1 ≤ n → n + 1 ≤ M - 1 → |u n + u (n + 1)| ≤ B * e n) (m : ℕ) :

1 ≤ m → m ≤ M - 1 → |u m - (-1) ^ (M - 1 - m) * L| ≤ B * T * e m

Alternating telescoping.

Documentation