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

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

The crude top bad-scale component

In the top complementary range, the selected-scale inequality bounds n by a deterministic logarithmic offset. Since this branch also has q ≤ n, it is empty above the corresponding deterministic threshold.

theorem HCPolySupport.Book.Ch05.Section57.selectedBadPairScale_cast_le_logOffset {K a t α : ℝ} (ha : 0 < a) {q m n : ℕ} : have x := α * ↑(m - q) - t * ↑(m - n); have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); ↑(selectedBadPairScale K a t α q m n) ≤ L + max (x / a) 0 + 1

The selected bad-pair scale is bounded by the logarithmic offset plus the positive part of the exponent correction. This deterministic cutoff estimate is loss-free; it is kept with the crude-top branch rather than with the old kernel bounds.

theorem HCPolySupport.Book.Ch05.Section57.crudeTopBadScaleEvent_eq_empty_of_large {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (hαt : α < t) (hαa : α < a) (hq_large : have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); L + 1 < (1 - α / a) * ↑q) : crudeTopBadScaleEvent H K a t α q = ∅

theorem HCPolySupport.Book.Ch05.Section57.measureReal_crudeTopBadScaleEvent_eq_zero_of_large {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (hαt : α < t) (hαa : α < a) (hq_large : have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); L + 1 < (1 - α / a) * ↑q) : μ.real (crudeTopBadScaleEvent H K a t α q) = 0