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

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

The concentration step for the first quenched estimate

This file records the part of Corollary c.first.quenched.estimate which is already supplied by the Chapter 4 concentration lemma: a unit-scale Γσ tail for the chosen deterministic block vectors propagates to larger scales around the corresponding annealed response. The remaining Section 5.7 work is to produce that unit-scale tail and the annealed bound for the limiting normalization \overline A.

theorem HCPolySupport.Book.Ch05.Section57.firstQuenchedEstimate_concentrationStep {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (hσ_le_two : σ ≤ 2) : ∃ (C : ℝ), 0 < C ∧ ∀ {Pμ : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure Pμ], Ch04.RestrictionLawCarrier Pμ → Ch04.RestrictionStationaryLaw Pμ → Ch04.RestrictionUnitRangeDependentLaw Pμ → ∀ (P Qv : BlockVec d) {θ : ℝ}, 0 < θ → IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (Ch04.blockJObservableCubeSetBlockVec (originCube d 0) P Qv) θ → ∀ {n m : ℤ}, 0 ≤ n → n < m → ∀ {R : ℝ}, ∫ (b : RegCoeffField d), Ch04.blockJObservableCubeSetBlockVec (originCube d n) P Qv b ∂Pμ ≤ R → IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => Ch04.blockJObservableCubeSetBlockVec (originCube d m) P Qv a - R) (C * 3 ^ (-↑d / 2 * ↑(m - n).toNat) * θ)

Concentration plus deterministic annealed domination, in the form used by the first quenched estimate.

The constant is chosen before the law Pμ, so it is independent of the probability measure.

theorem HCPolySupport.Book.Ch05.Section57.firstQuenchedEstimate_limitNormalized_concentration {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) : ∃ (C : ℝ), 0 < C ∧ ∀ {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hΓ : GammaSigmaCoarseGrainedEllipticity Pμ hPμ hStruct), hΓ.sigma = σ → ∀ (e : FullBlockVec d), (∀ (α : BlockCoord d), |e α| ≤ 1) → ∀ {n m : ℤ}, 0 ≤ n → n < m → ∀ {R : ℝ}, ∫ (b : RegCoeffField d), limitNormalizedBlockJObservable hPμ hStruct (originCube d n) e b ∂Pμ ≤ R → IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma (min σ 2)) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hPμ hStruct (originCube d m) e a - R) (C * 3 ^ (-↑d / 2 * ↑(m - n).toNat) * (thetaAtScale hPμ hStruct 0 * hΓ.thetaHat))

First quenched concentration step for the limiting normalization \overline A: the unit-cube Γσ tail from (P5) propagates from scale n to scale m, centered at any deterministic upper bound for the annealed response at scale n, with the concentration exponent truncated to σ ∧ 2.

The constant is chosen after d, σ and before the law, hence is independent of the probability measure and of the Γσ scale thetaHat.

theorem HCPolySupport.Book.Ch05.Section57.firstQuenchedEstimate_limitNormalized {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (α : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < α ∧ ∀ {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hΓ : GammaSigmaCoarseGrainedEllipticity Pμ hPμ hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ {n m : ℕ}, n < m → have N0 := annealedAlgebraicEntryScale Pμ hΓ.toQuantitativeCoarseGrainedEllipticity Centry; IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma (min σ 2)) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hPμ hStruct (originCube d ↑(N0 + m)) e a - Real.rpow 3 (-α * ↑n)) (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + m) - ↑(N0 + n)).toNat) * hΓ.thetaHat ^ 2)

Corollary c.first.quenched.estimate, in the limiting scalar normalization used by Section 5.7, with the quenched fluctuation controlled in the Γ_{σ ∧ 2} class.

The fluctuation constant, the annealed entry constant, and the algebraic exponent are selected before the law Pμ. The entry scale is the deterministic annealed scale associated to Centry; after that shift, the annealed theorem controls the deterministic centering and the Γσ concentration estimate gives the quenched fluctuation term.

theorem HCPolySupport.Book.Ch05.Section57.firstQuenchedEstimate_limitNormalized_uniformAnnealedExponent {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ), 0 < Cfluct ∧ ∀ {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hΓ : GammaSigmaCoarseGrainedEllipticity Pμ hPμ hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ {n m : ℕ}, n < m → have N0 := annealedAlgebraicEntryScale Pμ hΓ.toQuantitativeCoarseGrainedEllipticity Centry; IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma (min σ 2)) (fun (aω : RegCoeffField d) => limitNormalizedBlockJObservable hPμ hStruct (originCube d ↑(N0 + m)) e aω - Real.rpow 3 (-a * ↑n)) (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + m) - ↑(N0 + n)).toNat) * hΓ.thetaHat ^ 2)

Uniform-in-σ version of firstQuenchedEstimate_limitNormalized.

The annealed entry constant and algebraic exponent are chosen before the finite moment exponent σ. Only the fluctuation constant is selected after σ, reflecting that the concentration step depends on the moment class while the annealed algebraic rate only uses the existence of a finite moment.

theorem HCPolySupport.Book.Ch05.Section57.firstQuenchedEstimate_limitNormalized_uniformAnnealedExponent_noXi {d : ℕ} [NeZero d] (params : GammaCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ), 0 < Cfluct ∧ ∀ {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hΓ : GammaSigmaCoarseGrainedEllipticityNoXi Pμ hPμ hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ {n m : ℕ}, n < m → have N0 := annealedAlgebraicEntryScale Pμ hΓ.withInternalXi.toQuantitativeCoarseGrainedEllipticity Centry; IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma (min σ 2)) (fun (aω : RegCoeffField d) => limitNormalizedBlockJObservable hPμ hStruct (originCube d ↑(N0 + m)) e aω - Real.rpow 3 (-a * ↑n)) (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + m) - ↑(N0 + n)).toNat) * hΓ.thetaHat ^ 2)

Note-facing, xi-free version of firstQuenchedEstimate_limitNormalized_uniformAnnealedExponent.

The proof chooses the finite moment exponent needed by the older annealed API internally from sUpper and sLower; the resulting constants therefore depend only on the displayed Section 5.7 parameters.