Coarse-graining support: Support.Book.Ch05.Theorems.Section57.DeterministicThresholds

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

Deterministic threshold algebra for bad scales

This file records the real-variable estimates used when choosing the intermediate scale ℓ in the proof of Theorem t.homogenization.quenched.

theorem HCPolySupport.Book.Ch05.Section57.prefactor_rpow_three_neg_le_half_rpow_of_log_gap {K a x : ℝ} {ℓ : ℕ} (ha : 0 < a) (hgap : (a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3) ≤ ↑ℓ) : K * Real.rpow 3 (-a * ↑ℓ) ≤ 1 / 2 * Real.rpow 3 (-x)

A logarithmic gap for ℓ makes the deterministic centered contribution fit into half of the bad-event threshold.

The intended substitution is x = α (m - N) - t (m - n), so that the right side is one half of the post-discount threshold.

theorem HCPolySupport.Book.Ch05.Section57.prefactor_rpow_three_neg_le_half_rpow_of_natCeil_log_gap {K a x : ℝ} (ha : 0 < a) : have ℓ := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; K * Real.rpow 3 (-a * ↑ℓ) ≤ 1 / 2 * Real.rpow 3 (-x)

Ceiling form of prefactor_rpow_three_neg_le_half_rpow_of_log_gap.

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_discount_mul_postThreshold {t α : ℝ} {m n N : ℕ} : Real.rpow 3 (-t * ↑(m - n)) * Real.rpow 3 (-(α * ↑(m - N) - t * ↑(m - n))) = Real.rpow 3 (-α * ↑(m - N))

The post-discount threshold identity used in the fixed-pair bad-event estimate.