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

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

Real-variable staging for the Section 5.4 pigeonhole lemma

The final pigeonhole proof needs a small logarithmic estimate for the chosen number of scale steps. This file is reserved for that pure real algebra, separate from the law-facing scalar-chain input.

theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.exp_neg_half_delta_mul_natCeil_two_delta_inv_abs_log_le {delta sigma : ℝ} (hdelta_pos : 0 < delta) (hsigma_pos : 0 < sigma) (hsigma_le_one : sigma ≤ 1) : Real.exp (-(1 / 2 * delta * ↑⌈2 * delta⁻¹ * |Real.log sigma|⌉₊)) ≤ sigma

The logarithmic scale count used in the pigeonhole lemma makes the exponential tail at most sigma.

theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.inv_one_add_delta_le_exp_neg_half {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le : delta ≤ 1 / 2) : (1 + delta)⁻¹ ≤ Real.exp (-(1 / 2 * delta))

The elementary estimate (1 + δ)⁻¹ ≤ exp (-δ / 2) on the range used by the pigeonhole lemma.

theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.inv_one_add_delta_pow_le_exp_neg_half_mul {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le : delta ≤ 1 / 2) (k : ℕ) : (1 + delta)⁻¹ ^ k ≤ Real.exp (-(1 / 2 * delta * ↑k))

Iterated version of inv_one_add_delta_le_exp_neg_half.

theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.inv_one_add_delta_pow_natCeil_two_delta_inv_abs_log_le {delta sigma : ℝ} (hdelta_pos : 0 < delta) (hdelta_le : delta ≤ 1 / 2) (hsigma_pos : 0 < sigma) (hsigma_le_one : sigma ≤ 1) : (1 + delta)⁻¹ ^ ⌈2 * delta⁻¹ * |Real.log sigma|⌉₊ ≤ sigma

The manuscript scale count makes the repeated (1 + δ)⁻¹ loss no larger than σ.