Coarse-graining support: Support.Book.Ch04.Theorems.StationaryExpectations

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

Stationary response expectations

This file is the public Chapter 4 surface for the stationarity step used by the expectation/moment arguments: at nonnegative scales, deterministic child cubes are integer translates of the origin cube at the same scale, so stationarity identifies their annealed response expectations.

The statements are phrased directly in terms of the clean response expectation objects from Expectations.lean.

theorem HCPolySupport.Book.Ch04.responseJCubeSet_translation_covariant {d : ℕ} (p q : Vec d) : IsTranslationCovariant fun (U : Set (Vec d)) (a : CoeffField d) => ResponseJ U p q a

Scalar response is translation-covariant as a set-indexed coefficient-field observable.

theorem HCPolySupport.Book.Ch04.coarseBlockMatrix_entry_translation_covariant {d : ℕ} (α β : BlockCoord d) : IsTranslationCovariant fun (U : Set (Vec d)) (a : CoeffField d) => blockMatEntry (coarseBlockMatrix U a) α β

Coarse block matrix entries are translation-covariant as set-indexed coefficient-field observables.

noncomputable def HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (m : ℤ) : BlockMat d

Scalar block diagonal center used to normalize full-block fluctuations at a structural-law scale. The lower-right block is the inverse starred scalar.

Equations

• HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct m = HCPolySupport.Book.Ch02.blockDiag (hP.barSigmaAtScale hStruct m • 1) ((hP.barSigmaStarAtScale hStruct m)⁻¹ • 1)

noncomputable def HCPolySupport.Book.Ch04.scalarFullBlockInvSqrtDiag {d : ℕ} (b c : ℝ) : BlockCoord d → ℝ

Diagonal full-block normalization associated with scalar blocks b,c.

Equations

• HCPolySupport.Book.Ch04.scalarFullBlockInvSqrtDiag b c (Sum.inl val) = (√b)⁻¹
• HCPolySupport.Book.Ch04.scalarFullBlockInvSqrtDiag b c (Sum.inr val) = √c

noncomputable def HCPolySupport.Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSq {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (m : ℤ) (U : Set (Vec d)) (a : CoeffField d) : ℝ

Manuscript normalized full-block fluctuation observable at center scale m, written for an arbitrary deterministic set. The norm is the Euclidean operator norm of the associated full block matrix.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (m : ℤ) (R : TriadicCube d) (a : RegCoeffField d) : ℝ

Manuscript normalized full-block fluctuation observable on a triadic cube. The norm is the Euclidean operator norm, not the Frobenius norm.

Equations

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

theorem HCPolySupport.Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSq_translation_covariant {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (m : ℤ) : IsTranslationCovariant fun (U : Set (Vec d)) (a : CoeffField d) => fullBlockNormalizedFluctuationOperatorNormSq hP hStruct m U a

The normalized full-block fluctuation observable is translation-covariant in its deterministic set argument.

theorem HCPolySupport.Book.Ch04.translateReg_toFun {d : ℕ} (z : Fin d → ℤ) (a : RegCoeffField d) : (translateReg (intVecToRealVec z) a).toFun = translateByInt z a.toFun

Carrier bridge for integer translation: precomposition on the carrier projects to the raw integer translation (rfl).

theorem HCPolySupport.Book.Ch04.integral_comp_toFun_translation_transfer_of_restrictionStationaryLaw {d : ℕ} {P : RestrictionCoeffLaw d} {X : Set (Vec d) → CoeffField d → ℝ} (hstat : RestrictionStationaryLaw P) {U : Set (Vec d)} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => X U a.toFun) P) (hcov : IsTranslationCovariant X) (z : Fin d → ℤ) : ∫ (a : RegCoeffField d), X (translateSet (intVecToRealVec z) U) a.toFun ∂P = ∫ (a : RegCoeffField d), X U a.toFun ∂P

Translation transfer under a restriction-stationary carrier law for a raw translation-covariant observable composed with toFun integrates equally on translated sets under a stationary carrier law. Uses IsStationaryR.integral_comp_translateReg and the translateReg/translateByInt bridge.

def HCPolySupport.Book.Ch04.IsRestrictionTranslationCovariant {β : Type u_1} {d : ℕ} (X : Set (Vec d) → RegCoeffField d → β) : Prop

Restriction translation covariance: a set-indexed carrier observable commutes with spatial integer translation via the carrier translation translateReg.

Equations

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

theorem HCPolySupport.Book.Ch04.isRestrictionTranslationCovariant_comp_toFun {β : Type u_1} {d : ℕ} {X : Set (Vec d) → CoeffField d → β} (hX : IsTranslationCovariant X) : IsRestrictionTranslationCovariant fun (U : Set (Vec d)) (a : RegCoeffField d) => X U a.toFun

A raw translation-covariant observable, precomposed with toFun, is restriction translation covariant.

theorem HCPolySupport.Book.Ch04.comp_translateReg_eq_of_isRestrictionTranslationCovariant {β : Type u_1} {d : ℕ} {X : Set (Vec d) → RegCoeffField d → β} (hX : IsRestrictionTranslationCovariant X) (U : Set (Vec d)) (z : Fin d → ℤ) : X (translateSet (intVecToRealVec z) U) = X U ∘ translateReg (intVecToRealVec z)

Restriction-carrier analogue of comp_translateByInt_eq_of_isTranslationCovariant.

theorem HCPolySupport.Book.Ch04.map_eq_map_translateReg_of_isRestrictionTranslationCovariant {β : Type u_1} [MeasurableSpace β] {d : ℕ} {P : RestrictionCoeffLaw d} {X : Set (Vec d) → RegCoeffField d → β} (hP : RestrictionStationaryLaw P) {U : Set (Vec d)} (hX_meas : Measurable (X U)) (hX_cov : IsRestrictionTranslationCovariant X) (z : Fin d → ℤ) : MeasureTheory.Measure.map (X (translateSet (intVecToRealVec z) U)) P = MeasureTheory.Measure.map (X U) P

Restriction-carrier analogue of map_eq_map_translateByInt_of_isTranslationCovariant.

theorem HCPolySupport.Book.Ch04.map_eq_map_translateReg_of_isRestrictionTranslationCovariant_aemeasurable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {P : RestrictionCoeffLaw d} {X : Set (Vec d) → RegCoeffField d → β} (hP : RestrictionStationaryLaw P) {U : Set (Vec d)} (hX_aemeas : AEMeasurable (X U) P) (hX_cov : IsRestrictionTranslationCovariant X) (z : Fin d → ℤ) : MeasureTheory.Measure.map (X (translateSet (intVecToRealVec z) U)) P = MeasureTheory.Measure.map (X U) P

A.e.-measurable carrier analogue of map_eq_map_translateByInt_of_isTranslationCovariant_aemeasurable.

theorem HCPolySupport.Book.Ch04.integral_eq_of_isRestrictionTranslationCovariant_of_stationary {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {d : ℕ} {P : RestrictionCoeffLaw d} {X : Set (Vec d) → RegCoeffField d → E} (hP : RestrictionStationaryLaw P) {U : Set (Vec d)} (hX_meas : Measurable (X U)) (hX_cov : IsRestrictionTranslationCovariant X) (z : Fin d → ℤ) : ∫ (a : RegCoeffField d), X (translateSet (intVecToRealVec z) U) a ∂P = ∫ (a : RegCoeffField d), X U a ∂P

Carrier analogue of integral_eq_of_isTranslationCovariant_of_isStationary.

theorem HCPolySupport.Book.Ch04.integral_eq_of_isRestrictionTranslationCovariant_of_stationary_aestronglyMeasurable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {d : ℕ} {P : RestrictionCoeffLaw d} {X : Set (Vec d) → RegCoeffField d → E} (hP : RestrictionStationaryLaw P) {U : Set (Vec d)} (hX_aemeas : MeasureTheory.AEStronglyMeasurable (X U) P) (hX_cov : IsRestrictionTranslationCovariant X) (z : Fin d → ℤ) : ∫ (a : RegCoeffField d), X (translateSet (intVecToRealVec z) U) a ∂P = ∫ (a : RegCoeffField d), X U a ∂P

A.e.-strongly-measurable carrier analogue of integral_eq_of_isTranslationCovariant_of_isStationary_aestronglyMeasurable.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.expectedResponseJCubeSet_eq_originCube_of_stationary {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) (p q : Vec d) : expectedResponseJCubeSet P R p q = expectedResponseJCubeSet P (originCube d R.scale) p q

Under stationarity, the annealed response on a nonnegative-scale cube is the annealed response on the origin cube at the same scale.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integral_coarseBlockMatrix_entry_cubeSet_eq_originCube_of_stationary {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) (α β : BlockCoord d) : ∫ (a : RegCoeffField d), blockMatEntry (coarseBlockMatrix (cubeSet R) a.toFun) α β ∂P = ∫ (a : RegCoeffField d), blockMatEntry (coarseBlockMatrix (cubeSet (originCube d R.scale)) a.toFun) α β ∂P

Under stationarity, every coarse block matrix entry on a nonnegative-scale cube has the same expectation as the corresponding origin-cube entry.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.expectedResponseJCubeSet_eq_originCube_of_mem_descendantsAtScale_originCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (p q : Vec d) : expectedResponseJCubeSet P R p q = expectedResponseJCubeSet P (originCube d n) p q

Under stationarity, a child cube of an origin cube has the same annealed response as the origin cube at the child scale.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integral_coarseBlockEntry_eq_origin_on_originDescendant {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (α β : BlockCoord d) : ∫ (a : RegCoeffField d), blockMatEntry (coarseBlockMatrix (cubeSet R) a.toFun) α β ∂P = ∫ (a : RegCoeffField d), blockMatEntry (coarseBlockMatrix (cubeSet (originCube d n)) a.toFun) α β ∂P

Under stationarity, every coarse block matrix entry on a child cube of an origin cube has the same expectation as the corresponding origin-cube entry at the child scale.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.fluctuationOperatorNormSq_integral_eq_origin_of_stationarity {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (hStruct : RestrictionStructuralLaw P) (center : ℤ) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) (hOrigin : MeasureTheory.Integrable (fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d R.scale)) P) : ∫ (a : RegCoeffField d), fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R a ∂P = ∫ (a : RegCoeffField d), fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d R.scale) a ∂P

Under stationarity, the normalized full-block fluctuation on a nonnegative-scale cube has the same expectation as the corresponding origin-cube fluctuation. The norm is the Euclidean operator norm of the full block matrix.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_fullBlockNormalizedFluctuationOperatorNormSqAtScale_of_stationary {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (hStruct : RestrictionStructuralLaw P) (center : ℤ) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) (hOrigin : MeasureTheory.Integrable (fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d R.scale)) P) : MeasureTheory.Integrable (fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R) P

Under stationarity, integrability of the origin-cube normalized full-block fluctuation transfers to every same-scale cube.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.fluctuationOperatorNormSq_integrable_on_originDescendants {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (hStruct : RestrictionStructuralLaw P) (center : ℤ) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (hOrigin : MeasureTheory.Integrable (fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d n)) P) : MeasureTheory.Integrable (fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R) P

Under stationarity, integrability of the origin-cube normalized full-block fluctuation at the child scale transfers to descendants of a larger origin cube.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integral_descendantMean_fullBlockFluctuationNormSq_eq_cube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (hStruct : RestrictionStructuralLaw P) (center : ℤ) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (hOrigin : MeasureTheory.Integrable (fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d n)) P) : ∫ (a : RegCoeffField d), descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R a ∂P = ∫ (a : RegCoeffField d), fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d n) a ∂P

Under stationarity, the expectation of a descendant average of normalized full-block fluctuation observables is the corresponding origin-cube expectation at the descendant scale. The observable uses the Euclidean operator norm of the full block matrix.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_coarseFullBlockMatrixAtCube_of_mem_descendantsAtScale_originCube {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (hOrigin : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube R) P

Full coarse-block integrability transfers from the origin cube at scale n to every scale-n descendant of the origin cube at a larger scale. This is the stationarity source theorem for the descendant integrability hypotheses in annealed subadditivity.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.expectedDescendantsAverageResponseJCubeSet_eq_originCube_of_stationary {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (p q : Vec d) : expectedDescendantsAverageResponseJCubeSet P (originCube d m) (m - n).toNat p q = expectedResponseJCubeSet P (originCube d n) p q

Under stationarity, the finite descendant average of child annealed responses equals the annealed response on the origin cube at the child scale.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integral_responseJDescendantAverage_eq_origin_of_stationarity {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (p q : Vec d) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a ∂P = expectedResponseJCubeSet P (originCube d n) p q

Under stationarity, the expectation of the finite descendant average of response observables is the annealed response on the origin cube at the child scale.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integral_weightedResponseJAverages_eq_weightAverage_mul_cubeAverage {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (weight : TriadicCube d → ℝ) (p q : Vec d) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => weight R * restrictionResponseJObservableCubeSet R p q a ∂P = descendantsAverage (originCube d m) (m - n).toNat weight * expectedResponseJCubeSet P (originCube d n) p q

Weighted finite descendant response averages reduce to the average of the deterministic weights times the origin-cube expectation under stationarity.

This is the source theorem for the cancellation step in Section 5.3: Ch5 supplies the cutoff weights and the scalar identity saying their finite descendant average is zero.