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

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

Localized block-response maxima

This file packages the finite maximum over subcubes appearing in Theorem t.homogenization.quenched. The maximum is first defined for a fixed full-block vector e; the finite-basis reduction for the maximum over unit vectors is kept as a later deterministic step.

noncomputable def HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (m n : ℕ) (e : FullBlockVec d) : RegCoeffField d → ℝ

The finite maximum of the limiting-normalized block response over all scale-n descendants of the scale-m origin cube.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section57.descendantsAtScale_originCube_nat_nonempty {d m n : ℕ} (hnm : n ≤ m) : (descendantsAtScale (originCube d ↑m) ↑n).Nonempty

theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_le_localizedLimitNormalizedJMax {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) {m n : ℕ} (e : FullBlockVec d) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d ↑m) ↑n) (a : RegCoeffField d) : limitNormalizedBlockJObservable hP hStruct R e a ≤ localizedLimitNormalizedJMax hP hStruct m n e a

noncomputable def HCPolySupport.Book.Ch05.Section57.discountedLocalizedLimitNormalizedJMax {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (t : ℝ) (m n : ℕ) (e : FullBlockVec d) : RegCoeffField d → ℝ

Discounted localized response, the left side of the bad-event predicate.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section57.aemeasurable_limitNormalizedBlockJObservable {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (Q : TriadicCube d) (e : FullBlockVec d) : AEMeasurable (limitNormalizedBlockJObservable hP hStruct Q e) Pμ

theorem HCPolySupport.Book.Ch05.Section57.map_limitNormalizedBlockJObservable_eq_origin_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {m n : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (e : FullBlockVec d) : MeasureTheory.Measure.map (limitNormalizedBlockJObservable hP hStruct R e) Pμ = MeasureTheory.Measure.map (limitNormalizedBlockJObservable hP hStruct (originCube d n) e) Pμ

theorem HCPolySupport.Book.Ch05.Section57.isBigOWith_limitNormalizedBlockJObservable_sub_const_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A c : ℝ} {m n : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (e : FullBlockVec d) (hOrigin : IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hP hStruct (originCube d n) e a - c) A) : IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hP hStruct R e a - c) A

theorem HCPolySupport.Book.Ch05.Section57.isBigO_limitNormalizedBlockJObservable_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A : ℝ} {m n : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (e : FullBlockVec d) (hOrigin : IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (limitNormalizedBlockJObservable hP hStruct (originCube d n) e) A) : IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (limitNormalizedBlockJObservable hP hStruct R e) A

theorem HCPolySupport.Book.Ch05.Section57.isBigO_limitNormalizedBlockJObservable_originCube_of_scaleZero {d : ℕ} [NeZero d] {σ : ℝ} (_hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {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), (∀ (α : BlockCoord d), |e α| ≤ 1) → ∀ {n : ℕ}, IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (limitNormalizedBlockJObservable hPμ hStruct (originCube d ↑n) e) (C * hΓ.thetaHat ^ 2)

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_sub_const_le_sup_sub {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) {m n : ℕ} (e : FullBlockVec d) (c : ℝ) (a : RegCoeffField d) : have D := descendantsAtScale (originCube d ↑m) ↑n; ∀ (hD : D.Nonempty), localizedLimitNormalizedJMax hP hStruct m n e a - c ≤ D.sup' hD fun (R : TriadicCube d) => limitNormalizedBlockJObservable hP hStruct R e a - c

theorem HCPolySupport.Book.Ch05.Section57.descendantsAtScale_originCube_nat_card_two_le {d : ℕ} [NeZero d] {m n : ℕ} (hnm : n < m) : 2 ≤ (descendantsAtScale (originCube d ↑m) ↑n).card

theorem HCPolySupport.Book.Ch05.Section57.isBigO_localizedLimitNormalizedJMax {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {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 → ∀ {m n : ℕ}, n < m → have D := descendantsAtScale (originCube d ↑m) ↑n; IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (localizedLimitNormalizedJMax hPμ hStruct m n e) ((3 * Real.log ↑D.card) ^ σ⁻¹ * (C * hΓ.thetaHat ^ 2))

theorem HCPolySupport.Book.Ch05.Section57.isBigOWith_localizedLimitNormalizedJMax_sub_const {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A c : ℝ} (hσ : 0 < σ) {m n : ℕ} (hnm : n < m) (e : FullBlockVec d) (hOrigin : IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hP hStruct (originCube d ↑n) e a - c) A) : IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => localizedLimitNormalizedJMax hP hStruct m n e a - c) ((3 * Real.log ↑(descendantsAtScale (originCube d ↑m) ↑n).card) ^ σ⁻¹ * A)

theorem HCPolySupport.Book.Ch05.Section57.localizedFirstQuenchedEstimate_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 → n < m → have N0 := annealedAlgebraicEntryScale Pμ hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma (min σ 2)) (fun (a : RegCoeffField d) => localizedLimitNormalizedJMax hPμ hStruct (N0 + m) (N0 + n) e a - Real.rpow 3 (-α * ↑ℓ)) ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2))

Localized version of Corollary c.first.quenched.estimate for a fixed unit vector. The finite maximum over descendants costs only the standard (log #D)^{1/(σ∧2)} factor.

theorem HCPolySupport.Book.Ch05.Section57.localizedFirstQuenchedEstimate_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 → n < m → have N0 := annealedAlgebraicEntryScale Pμ hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma (min σ 2)) (fun (aω : RegCoeffField d) => localizedLimitNormalizedJMax hPμ hStruct (N0 + m) (N0 + n) e aω - Real.rpow 3 (-a * ↑ℓ)) ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2))

Uniform-in-σ version of localizedFirstQuenchedEstimate_limitNormalized.

The entry constant and annealed algebraic exponent are fixed before the finite moment exponent; the localized fluctuation constant remains allowed to depend on σ.