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

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

Deterministic large-scale thresholds

These elementary real-variable lemmas discharge the side conditions in the concrete bad-scale kernel once the bad scale is chosen above an explicit deterministic threshold.

theorem HCPolySupport.Book.Ch05.Section57.one_le_rpow_three_linear_sub_div_of_log_bound {β O D q : ℝ} (hβ : 0 < β) (hD : 0 < D) (hq : (Real.log D + O * Real.log 3) / (β * Real.log 3) ≤ q) : 1 ≤ 3 ^ (β * q - O) / D

If q is above the logarithmic threshold associated with a denominator D, then the base-three tail parameter is at least one.

theorem HCPolySupport.Book.Ch05.Section57.one_le_rpow_three_linear_sub_nat_div_of_log_bound {β O D : ℝ} {q : ℕ} (hβ : 0 < β) (hD : 0 < D) (hq : (Real.log D + O * Real.log 3) / (β * Real.log 3) ≤ ↑q) : 1 ≤ 3 ^ (β * ↑q - O) / D

Natural-scale version of one_le_rpow_three_linear_sub_div_of_log_bound.

theorem HCPolySupport.Book.Ch05.Section57.one_le_rpow_three_linear_sub_nat_div_of_natCeil_le {β O D : ℝ} {q : ℕ} (hβ : 0 < β) (hD : 0 < D) (hq : ⌈(Real.log D + O * Real.log 3) / (β * Real.log 3)⌉₊ ≤ q) : 1 ≤ 3 ^ (β * ↑q - O) / D

A ceiling threshold is enough to make the base-three tail parameter at least one.

theorem HCPolySupport.Book.Ch05.Section57.large_scale_cutoff_of_div_lt {L δ : ℝ} {q : ℕ} (hδ : 0 < δ) (hq : (L + 1) / δ < ↑q) : L + 1 < δ * ↑q

Once the scale is above the cutoff threshold, the crude-top branch is deterministically empty.

theorem HCPolySupport.Book.Ch05.Section57.large_scale_cutoff_of_natCeil_add_one_le {L δ : ℝ} {q : ℕ} (hδ : 0 < δ) (hq : ⌈(L + 1) / δ + 1⌉₊ ≤ q) : L + 1 < δ * ↑q

Ceiling form of the large-scale cutoff.