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

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

Quenched homogenization above the quantitative minimal scale

This file applies the deterministic scale compression to the quantitative minimal-scale theorem. The result is still written with the shifted entry scale N0; the final public wrapper only has to choose the admissible exponent alpha and undo the harmless shift.

theorem HCPolySupport.Book.Ch05.Section57.exists_shifted_quenchedLocalizedEstimate_interpolated_expLogSq {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ}, have b := ↑d / 2; 0 < t → t ≤ b → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {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; have η := finiteQuenchedTailExponent d σ t; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ}, X aω ≤ 3 ^ m → n < m → 3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (N0 + m) (N0 + n) e aω ≤ (3 ^ m / X aω) ^ (-αbad)

theorem HCPolySupport.Book.Ch05.Section57.max_sUpper_sLower_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < max params.sUpper params.sLower

The larger regularity exponent in the parameter-only (P4) data is positive.

theorem HCPolySupport.Book.Ch05.Section57.exists_shifted_quenchedLocalizedEstimate_interpolated_expLogSq_parameterAlpha {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (α : ℝ), 0 < Centry ∧ 0 < α ∧ ∀ {t : ℝ}, max params.sUpper params.sLower < t → t ≤ ↑d / 2 → ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {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; have η := finiteQuenchedTailExponent d σ t; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ}, X aω ≤ 3 ^ m → n < m → 3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (N0 + m) (N0 + n) e aω ≤ (3 ^ m / X aω) ^ (-α)

The shifted quenched estimate with a single exponent selected from the moment parameters.

The exponent alpha is chosen before the law. For every decay exponent t > max sUpper sLower with t ≤ d / 2, the stochastic scale has the manuscript exp(C log^2(2 + thetaHat)) size and the interpolated tail exponent finiteQuenchedTailExponent d sigma t.

theorem HCPolySupport.Book.Ch05.Section57.exists_aboveEntry_quenchedLocalizedEstimate_interpolated_expLogSq_parameterAlpha {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (α : ℝ), 0 < Centry ∧ 0 < α ∧ ∀ {t : ℝ}, max params.sUpper params.sLower < t → t ≤ ↑d / 2 → ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {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; have η := finiteQuenchedTailExponent d σ t; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ}, N0 ≤ n → X aω ≤ 3 ^ m → n < m → 3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct m n e aω ≤ (3 ^ m / X aω) ^ (-α)

Absolute-scale version of the shifted quenched estimate, valid once the bottom scale has passed the annealed entry scale.

Compared with exists_shifted_quenchedLocalizedEstimate_interpolated_expLogSq_parameterAlpha, the random scale is multiplied by 3 ^ N0; the deterministic entry-scale compression from EntryScaleCompression keeps the same manuscript exp(C log^2(2 + thetaHat)) envelope.

theorem HCPolySupport.Book.Ch05.Section57.exists_quenchedLocalizedEstimate_interpolated_expLogSq_parameterAlpha {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (α : ℝ), 0 < α ∧ ∀ {t : ℝ}, max params.sUpper params.sLower < t → t ≤ 1 → ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → have η := finiteQuenchedTailExponent d σ t; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ}, X aω ≤ 3 ^ m → n < m → 3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct m n e aω ≤ (3 ^ m / X aω) ^ (-α)

Note-facing quenched homogenization estimate above a random minimal scale.

The exponent alpha is selected before the law and depends only on the dimension and the moment parameters. For each admissible t, the scale constant is selected before the probability law; the stochastic integrability exponent is the corrected finite-sigma exponent finiteQuenchedTailExponent d sigma t.

theorem HCPolySupport.Book.Ch05.Section57.exists_quenchedLocalizedEstimate_interpolated_expLogSq_uniformAnnealedExponent {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (α : ℝ), 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {σ : ℝ}, 0 < σ → ∀ {t : ℝ}, max params.sUpper params.sLower < t → t ≤ 1 → ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → have η := finiteQuenchedTailExponent d σ t; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ}, X aω ≤ 3 ^ m → n < m → 3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct m n e aω ≤ (3 ^ m / X aω) ^ (-α)

Note-facing finite-sigma quenched estimate with the public exponent chosen before sigma.

The annealed entry constant and the final algebraic exponent depend only on the dimension and the deterministic moment parameters. For each finite moment exponent sigma, the fluctuation constants and scale constant may depend on sigma, as in the manuscript.