Coarse-graining support: Support.Book.Ch05.Theorems.Section51.EntryScale

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

Entry-scale arithmetic for Theorem t.annealed.convergence

The lemmas in this file are pure scale bookkeeping: they show that the manuscript two-ceiling scale with a sufficiently large universal constant dominates the fixed perturbative entry, shifted-moment tail, and algebraic burn-in scales.

theorem HCPolySupport.Book.Ch05.Section51.widetildeThetaAtScale_nonneg {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℤ) : 0 ≤ widetildeThetaAtScale P m hP4

theorem HCPolySupport.Book.Ch05.Section51.log_two_add_ge_half {T : ℝ} (hT : 0 ≤ T) : 1 / 2 ≤ Real.log (2 + T)

theorem HCPolySupport.Book.Ch05.Section51.log_two_add_nonneg {T : ℝ} (hT : 0 ≤ T) : 0 ≤ Real.log (2 + T)

theorem HCPolySupport.Book.Ch05.Section51.natCeil_le_add_one {x : ℝ} (hx : 0 ≤ x) : ↑⌈x⌉₊ ≤ x + 1

theorem HCPolySupport.Book.Ch05.Section51.natCeil_add_nat_le_natCeil_mul_logSq {A C T : ℝ} {R : ℕ} (hT : 0 ≤ T) (hA : 0 ≤ A) (hC : A + 4 * (↑R + 1) ≤ C) : ⌈A * Real.log (2 + T) ^ 2⌉₊ + R ≤ ⌈C * Real.log (2 + T) ^ 2⌉₊

theorem HCPolySupport.Book.Ch05.Section51.natCeil_two_log_terms_le_natCeil_large_log {Acoef Aarg Bcoef Barg C xi T : ℝ} (hT : 0 ≤ T) (hxi : 1 ≤ xi) (hAcoef : 0 ≤ Acoef) (hAarg : 0 ≤ Aarg) (hBcoef : 0 ≤ Bcoef) (hBarg : 0 ≤ Barg) (hAarg_le_C : Aarg ≤ C) (hBarg_le_C : Barg ≤ C) (hsum_le_C : Acoef + Bcoef + 4 ≤ C) : ⌈Acoef * xi * Real.log (2 + Aarg * xi * T)⌉₊ + ⌈Bcoef * Real.log (2 + Barg * T)⌉₊ ≤ ⌈C * xi * Real.log (2 + C * xi * T)⌉₊