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

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

Entry-scale compression for the quenched theorem

The shifted minimal-scale theorem controls the random scale measured from the annealed entry scale. This file supplies the deterministic estimate needed to put the absolute factor 3 ^ N0 back into the manuscript envelope exp(C log^2(2 + thetaHat)).

theorem HCPolySupport.Book.Ch05.Section57.log_two_add_le_const_mul_log_two_add_of_le_const_mul_sq {A T θ : ℝ} (hA : 0 ≤ A) (hT : 0 ≤ T) (hθ : 0 ≤ θ) (hT_le : T ≤ A * θ ^ 2) : Real.log (2 + T) ≤ (2 + 2 * max 0 (Real.log (2 + A))) * Real.log (2 + θ)

theorem HCPolySupport.Book.Ch05.Section57.exists_entryScale_le_natCeil_logSq {d : ℕ} [NeZero d] {σ Centry : ℝ} (hσ : 0 < σ) (hCentry : 0 < Centry) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (CentryScale : ℝ), 0 < CentryScale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; N0 ≤ ⌈CentryScale * Real.log (2 + hΓ.thetaHat) ^ 2⌉₊

The annealed algebraic entry scale is bounded by a single manuscript ceil(C log^2(2 + thetaHat)) scale.

The constant is selected before the law; it depends only on the finite sigma, the parameter-only (P4) data, and the entry constant used to define N0.

theorem HCPolySupport.Book.Ch05.Section57.exists_entryScale_pow_three_le_exp_logSq {d : ℕ} [NeZero d] {σ Centry : ℝ} (hσ : 0 < σ) (hCentry : 0 < Centry) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (CentryScale : ℝ), 0 < CentryScale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; 3 ^ N0 ≤ Real.exp (CentryScale * Real.log (2 + hΓ.thetaHat) ^ 2)

The absolute annealed entry factor is absorbed by the manuscript exp(C log^2(2 + thetaHat)) envelope.

The constant is selected before the law; it depends only on the finite sigma, the parameter-only (P4) data, and the entry constant used to define N0.