Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.PartitionAverage

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

Local-representative bridge for partition averages

This file builds the Section 5.4-local bridge needed to feed the normalized full-block fluctuation observable into the Chapter 4 partition-average theorems. The bridge is internal to the variance-bound slice: it proves the locality/measurability facts from existing Ch4 entrywise local representatives, without adding proof objects to the public Section 5.4 theorem.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFullBlockCLMLinearMap {d : ℕ} (D : FullBlockMat d) : FullBlockMat d →ₗ[ℝ] EuclideanSpace ℝ (BlockCoord d) →L[ℝ] EuclideanSpace ℝ (BlockCoord d)

The linear map sending a full-block matrix M to the Euclidean operator of D * M * D.

Equations

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

def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFullBlockMatLinearMap {d : ℕ} (D : FullBlockMat d) : FullBlockMat d →ₗ[ℝ] FullBlockMat d

The linear map sending a full-block matrix M to the normalized matrix D * M * D.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFullBlockMatLinearMap D = mulRightLinearMap (HCPolySupport.BlockCoord d) ℝ D ∘ₗ mulLeftLinearMap (HCPolySupport.BlockCoord d) ℝ D

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54_annealedMomentRoot_abs_le_of_ae_abs_le_nonneg {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ξ : ℕ} {X Y : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (_hY_nonneg : ∀ (a : RegCoeffField d), 0 ≤ Y a) (hXY : (fun (a : RegCoeffField d) => |X a|) ≤ᵐ[P] Y) (hX_abs_pow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a| ^ ξ) P) (hY_pow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Y a ^ ξ) P) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => |X a|) ≤ Ch04.annealedMomentRoot P ξ Y

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54_integrable_abs_pow_of_ae_abs_le_nonneg {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ξ : ℕ} {X Y : RegCoeffField d → ℝ} (hX_meas : AEMeasurable X P) (hY_nonneg : ∀ᵐ (a : RegCoeffField d) ∂P, 0 ≤ Y a) (hXY : (fun (a : RegCoeffField d) => |X a|) ≤ᵐ[P] Y) (hY_pow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Y a ^ ξ) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a| ^ ξ) P

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54_annealedMomentRoot_abs_sub_integral_le_two_mul {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {ξ : ℕ} {X : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hX_meas : AEMeasurable X P) (hX_abs_pow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a| ^ ξ) P) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => |X a - ∫ (b : RegCoeffField d), X b ∂P|) ≤ 2 * Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => |X a|

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54_annealedMomentRoot_add_le {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ξ : ℕ} {X Y : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hX_nonneg : ∀ (a : RegCoeffField d), 0 ≤ X a) (hY_nonneg : ∀ (a : RegCoeffField d), 0 ≤ Y a) (hX_meas : AEMeasurable X P) (hY_meas : AEMeasurable Y P) (hX_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => X a ^ ξ) P) (hY_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Y a ^ ξ) P) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => X a + Y a) ≤ Ch04.annealedMomentRoot P ξ X + Ch04.annealedMomentRoot P ξ Y

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54_centeredOrigin_momentRoot_le_factor_sum_of_abs_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {C : ℝ} (hC_nonneg : 0 ≤ C) {X : RegCoeffField d → ℝ} (hX_meas : AEMeasurable X P) (hX_abs_le : (fun (a : RegCoeffField d) => |X a|) ≤ᵐ[P] fun (a : RegCoeffField d) => C * (Ch04.LambdaSqCoeffField (originCube d 0) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a + (Ch04.lambdaSqCoeffField (originCube d 0) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹)) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a - ∫ (b : RegCoeffField d), X b ∂P| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |X a - ∫ (b : RegCoeffField d), X b ∂P|) ≤ 2 * C * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.exists_localRandomVariable_ae_eq_fluctuationOperatorNormSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) : ∃ (Y : RegCoeffField d → ℝ), Ch04.IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center (cubeSet Q) a.toFun) =ᵐ[P] Y

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.exists_isRestrictionLocalRandomVariable_ae_eq_fullBlockNormalizedQuadraticObservable_cubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) : ∃ (Y : RegCoeffField d → ℝ), Ch04.IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => normalizedQuadraticObservable hP hStruct center q (cubeSet Q) a.toFun) =ᵐ[P] Y

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedFluctuationOperatorNormSq_descendants_localRep {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (n : ℤ) (R : TriadicCube d) : R ∈ descendantsAtScale Q n → ∃ (Y : RegCoeffField d → ℝ), Ch04.IsRestrictionLocalRandomVariable (cubeSet R) ⋯ Y ∧ (fun (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center (cubeSet R) a.toFun) =ᵐ[P] Y

Descendant-family local representatives for the normalized full-block fluctuation observable. This is the local-representative hypothesis needed by the a.e.-local Ch4 partition-average theorem.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_descendants_localRep {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) (n : ℤ) (R : TriadicCube d) : R ∈ descendantsAtScale Q n → ∃ (Y : RegCoeffField d → ℝ), Ch04.IsRestrictionLocalRandomVariable (cubeSet R) ⋯ Y ∧ (fun (a : RegCoeffField d) => normalizedQuadraticObservable hP hStruct center q (cubeSet R) a.toFun) =ᵐ[P] Y

Descendant-family local representatives for normalized quadratic probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.centeredDescendantAverageMomentRoot_le_of_unitRangeLaw_of_localRepresentatives {d : ℕ} {n m : ℤ} {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {p : ℕ} {K : ℝ} (hP : Ch04.RestrictionLawCarrier P) (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : Ch04.RestrictionStationaryLaw P) (hPdep : Ch04.RestrictionUnitRangeDependentLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_localRep : ∀ R ∈ descendantsAtScale (originCube d m) n, ∃ (Y : RegCoeffField d → ℝ), Ch04.IsRestrictionLocalRandomVariable (cubeSet R) ⋯ Y ∧ X (cubeSet R) =ᵐ[P] Y) (hX_cov : Ch04.IsRestrictionTranslationCovariant X) (hX0_aemeas : AEMeasurable (X (cubeSet (originCube d n))) P) (hX_desc_aemeas : ∀ R ∈ descendantsAtScale (originCube d m) n, AEMeasurable (X (cubeSet R)) P) (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (hX0Lp_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P n X a| ^ p) P) (hX0Lp : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredOriginObservable P n X a| ^ p ∂P) ^ (1 / ↑p) ≤ K) : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P n m X a| ^ p ∂P) ^ (1 / ↑p) ≤ (↑(descendantsAtScale (originCube d m) n).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d n p * ↑(descendantsAtScale (originCube d m) n).card ^ (1 / ↑p) * K + Ch04.rosenthalDescendantsAtScaleSqrtConst d n p * √↑(descendantsAtScale (originCube d m) n).card * K)

Origin-cube partition-average moment estimate with a.e.-local descendant representatives. This is the Section 5.4-local bridge from the exact-local Ch4 Rosenthal theorem to the totalized coarse-block observables used in Ch5.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedFluctuationOperatorNormSq_restrictionCenteredDescendantAverage_pow_rpow_inv_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {center n m : ℤ} {K : ℝ} (hn : 0 ≤ n) (hnm : n ≤ m) (hK_nonneg : 0 ≤ K) (hOriginMoment_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P n (fun (U : Set (Vec d)) (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center U a.toFun) a| ^ hP4.xi) P) (hOriginMoment : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredOriginObservable P n (fun (U : Set (Vec d)) (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center U a.toFun) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ K) : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P n m (fun (U : Set (Vec d)) (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center U a.toFun) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ (↑(descendantsAtScale (originCube d m) n).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d n hP4.xi * ↑(descendantsAtScale (originCube d m) n).card ^ (1 / ↑hP4.xi) * K + Ch04.rosenthalDescendantsAtScaleSqrtConst d n hP4.xi * √↑(descendantsAtScale (originCube d m) n).card * K)

Rosenthal/partition-average estimate for the normalized full-block fluctuation observable, assuming only the origin-scale moment root that the good-scale scalar estimates will provide.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_restrictionCenteredDescendantAverage_pow_rpow_inv_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {center n m : ℤ} {K : ℝ} (q : FullBlockVec d) (hn : 0 ≤ n) (hnm : n ≤ m) (hK_nonneg : 0 ≤ K) (hOriginMoment_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P n (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ hP4.xi) P) (hOriginMoment : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredOriginObservable P n (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ K) : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P n m (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ (↑(descendantsAtScale (originCube d m) n).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d n hP4.xi * ↑(descendantsAtScale (originCube d m) n).card ^ (1 / ↑hP4.xi) * K + Ch04.rosenthalDescendantsAtScaleSqrtConst d n hP4.xi * √↑(descendantsAtScale (originCube d m) n).card * K)

Rosenthal/partition-average estimate for a normalized quadratic probe, assuming the origin-scale moment root supplied by the good-scale scalar estimate.