Coarse-graining support: Support.Book.Ch05.Theorems.Section54.Pigeonhole.Assembly

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Assembly staging for the Section 5.4 pigeonhole lemma

The manuscript-facing theorem will live here. Its scalar-chain input is now available from (P4); the remaining work is the finite pigeonhole and telescoping argument over the arithmetic progression of scales.

theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.product_step_le_inv_mul_of_not_good {delta aPrev aNow bPrev bNow : ℝ} (hdelta_pos : 0 < delta) (haNow_nonneg : 0 ≤ aNow) (hbNow_nonneg : 0 ≤ bNow) (ha_mono : aNow ≤ aPrev) (hb_mono : bNow ≤ bPrev) (hbad : ¬(aPrev ≤ (1 + delta) * aNow ∧ bPrev ≤ (1 + delta) * bNow)) : aNow * bNow ≤ (1 + delta)⁻¹ * (aPrev * bPrev)

If one of the two good-scale inequalities fails while both scalar chains are monotone, then the product contracts by (1 + δ)⁻¹.

theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.iterate_le_geometric_of_step {A : ℕ → ℝ} {r : ℝ} (hr_nonneg : 0 ≤ r) (k : ℕ) : (∀ (j : ℕ), 1 ≤ j → j ≤ k → A j ≤ r * A (j - 1)) → A k ≤ r ^ k * A 0

A one-sided finite Gronwall estimate for a sequence whose consecutive steps are bounded by multiplication by r.