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

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

Quenched homogenization at the uniform endpoint

This file assembles the Γ∞ endpoint bad-scale proof into the shifted quenched estimate with stochastic integrability exponent d.

theorem HCPolySupport.Book.Ch05.Section57.rpow_neg_div_mono_of_le {A X Y α : ℝ} (hA : 0 < A) (hX : 0 < X) (hY : 0 < Y) (hXY : X ≤ Y) (hα : 0 < α) : (A / X) ^ (-α) ≤ (A / Y) ^ (-α)

If the normalizing random scale is enlarged, the negative-power right hand side in the quenched estimate becomes larger.

theorem HCPolySupport.Book.Ch05.Section57.discount_mul_rpow_eq_div_rpow_neg {D t α : ℝ} {m n : ℕ} (hD : 0 < D) (hα : 0 < α) : 3 ^ (-t * ↑(m - n)) * D ^ α = (3 ^ (t / α * ↑(m - n)) / D) ^ (-α)

Algebraic form of a discounted deterministic bound.

theorem HCPolySupport.Book.Ch05.Section57.small_bottom_deterministic_estimate {J D X t α : ℝ} {m n N0 : ℕ} (hD : 1 ≤ D) (hJ : J ≤ D ^ α) (hXlower : 3 ^ N0 * D ≤ X) (hXupper : X ≤ 3 ^ m) (hnN0 : n < N0) (_hnm : n < m) (hα : 0 < α) (hαt : α < t) : 3 ^ (-t * ↑(m - n)) * J ≤ (3 ^ m / X) ^ (-α)

Deterministic control of the finite band below the entry scale. The factor 3 ^ N0 * D built into X pays for all bottoms n < N0.

theorem HCPolySupport.Book.Ch05.Section57.exists_shifted_quenchedLocalizedEstimate_uniformEndpoint_expLogSq {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ}, have b := ↑d / 2; 0 < t → 0 ≤ αbad → αbad < t → αbad < b → αbad * (1 + b / a) < b → αbad < a → t ≤ b → ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → have N0 := annealedAlgebraicEntryScale P hInf.toQuantitativeCoarseGrainedEllipticity Centry; have η := ↑d; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hInf.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.exists_shifted_quenchedLocalizedEstimate_uniformEndpoint_expLogSq_parameterAlpha {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (α : ℝ), 0 < Centry ∧ 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {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) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → have N0 := annealedAlgebraicEntryScale P hInf.toQuantitativeCoarseGrainedEllipticity Centry; have η := ↑d; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hInf.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ω) ^ (-α)

theorem HCPolySupport.Book.Ch05.Section57.exists_aboveEntry_quenchedLocalizedEstimate_uniformEndpoint_expLogSq_parameterAlpha {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (α : ℝ), 0 < Centry ∧ 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {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) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → have N0 := annealedAlgebraicEntryScale P hInf.toQuantitativeCoarseGrainedEllipticity Centry; have η := ↑d; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hInf.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ω) ^ (-α)

theorem HCPolySupport.Book.Ch05.Section57.exists_quenchedLocalizedEstimate_uniformEndpoint_expLogSq_parameterAlpha {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (α : ℝ), 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {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) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → have η := ↑d; ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hInf.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 at the uniform ellipticity endpoint.

The stochastic scale has Γ_d integrability. The constant Cscale is chosen before the law; the law only contributes the endpoint datum thetaHat.