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

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

Block-response expectations

This file is the public Chapter 4 surface for expectations of the block response observable. The Ch4-facing observable is the manuscript half-sum of one scalar response and one adjointed scalar response, so downstream sections never supply a separate BlockJ = half-sum a.e. bridge.

noncomputable def HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumSet {d : ℕ} (U : Set (Vec d)) (p pStar q qStar : Vec d) : CoeffField d → ℝ

The standard half-sum expression for the block response: one scalar response for a, and one scalar response for the adjointed field.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumCubeSet {d : ℕ} (Q : TriadicCube d) (p pStar q qStar : Vec d) : CoeffField d → ℝ

Cube-set specialization of the standard half-sum expression.

Equations

• HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumCubeSet Q p pStar q qStar = HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumSet (HCPolySupport.cubeSet Q) p pStar q qStar

@[simp]

theorem HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumCubeSet_apply {d : ℕ} (Q : TriadicCube d) (p pStar q qStar : Vec d) (a : CoeffField d) : blockJHalfResponseAdjointSumCubeSet Q p pStar q qStar a = 1 / 2 * ResponseJ (cubeSet Q) (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ (cubeSet Q) (pStar + p) (qStar + q) (adjointCoeffField a)

noncomputable def HCPolySupport.Book.Ch04.blockJObservableCubeSet {d : ℕ} (Q : TriadicCube d) (p pStar q qStar : Vec d) : RegCoeffField d → ℝ

Ch4-facing block response observable on a deterministic triadic cube. It is definitionally the manuscript half-sum expression evaluated on the underlying field of a carrier sample.

Equations

• HCPolySupport.Book.Ch04.blockJObservableCubeSet Q p pStar q qStar a = HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumCubeSet Q p pStar q qStar a.toFun

@[simp]

theorem HCPolySupport.Book.Ch04.blockJObservableCubeSet_apply {d : ℕ} (Q : TriadicCube d) (p pStar q qStar : Vec d) (a : RegCoeffField d) : blockJObservableCubeSet Q p pStar q qStar a = 1 / 2 * restrictionResponseJObservableCubeSet Q (p - pStar) (qStar - q) a + 1 / 2 * restrictionResponseJObservableCubeSet Q (pStar + p) (qStar + q) (adjointReg a)

theorem HCPolySupport.Book.Ch04.blockJObservableCubeSet_eq_half_responseJ_adjoint_sum {d : ℕ} (Q : TriadicCube d) (p pStar q qStar : Vec d) : blockJObservableCubeSet Q p pStar q qStar = fun (a : RegCoeffField d) => blockJHalfResponseAdjointSumCubeSet Q p pStar q qStar a.toFun

The Ch4 block observable is definitionally the standard half-sum on the underlying field.

noncomputable def HCPolySupport.Book.Ch04.expectedBlockJCubeSet {d : ℕ} (P : RestrictionCoeffLaw d) (Q : TriadicCube d) (p pStar q qStar : Vec d) : ℝ

Annealed block response on a deterministic triadic cube.

Equations

• HCPolySupport.Book.Ch04.expectedBlockJCubeSet P Q p pStar q qStar = ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.Book.Ch04.blockJObservableCubeSet Q p pStar q qStar a ∂P

noncomputable def HCPolySupport.Book.Ch04.expectedDescendantsAverageBlockJCubeSet {d : ℕ} (P : RestrictionCoeffLaw d) (Q : TriadicCube d) (j : ℕ) (p pStar q qStar : Vec d) : ℝ

Annealed finite descendant average of block responses.

Equations

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

theorem HCPolySupport.Book.Ch04.integrable_descendantsAverage_blockJObservableCubeSet {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {j : ℕ} {p pStar q qStar : Vec d} (hB : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (blockJObservableCubeSet R p pStar q qStar) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => descendantsAverage Q j fun (R : TriadicCube d) => blockJObservableCubeSet R p pStar q qStar a) P

Finite descendant averages of block responses are integrable if the child block responses are integrable.

theorem HCPolySupport.Book.Ch04.memLp_descendantsAverage_blockJObservableCubeSet {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {j : ℕ} {r : ENNReal} {p pStar q qStar : Vec d} (hB : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (blockJObservableCubeSet R p pStar q qStar) r P) : MeasureTheory.MemLp (fun (a : RegCoeffField d) => descendantsAverage Q j fun (R : TriadicCube d) => blockJObservableCubeSet R p pStar q qStar a) r P

Finite descendant averages of block responses are in L^r if the child block responses are in L^r.

theorem HCPolySupport.Book.Ch04.integral_blockJDescendantAverage_eq_expectedAverage {d : ℕ} {P : RestrictionCoeffLaw d} (Q : TriadicCube d) (j : ℕ) (p pStar q qStar : Vec d) (hB : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (blockJObservableCubeSet R p pStar q qStar) P) : ∫ (a : RegCoeffField d), descendantsAverage Q j fun (R : TriadicCube d) => blockJObservableCubeSet R p pStar q qStar a ∂P = expectedDescendantsAverageBlockJCubeSet P Q j p pStar q qStar

Finite descendant block-response averages commute with expectation, assuming childwise integrability.

theorem HCPolySupport.Book.Ch04.integrable_blockJObservableCubeSet_of_integrable {d : ℕ} {P : RestrictionCoeffLaw d} (hAdj : RestrictionAdjointInvariantLaw P) (Q : TriadicCube d) (p pStar q qStar : Vec d) (hJ : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q (p - pStar) (qStar - q)) P) (hJAdjBase : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q (pStar + p) (qStar + q)) P) : MeasureTheory.Integrable (blockJObservableCubeSet Q p pStar q qStar) P

The Ch4 block response observable is integrable when the two scalar responses in its half-sum representation are integrable. The second scalar response is composed with the carrier adjoint using adjoint-invariance.

theorem HCPolySupport.Book.Ch04.integral_blockJObservableCubeSet_eq_half_expectedResponseJCubeSet_add {d : ℕ} {P : RestrictionCoeffLaw d} (hAdj : RestrictionAdjointInvariantLaw P) (Q : TriadicCube d) (p pStar q qStar : Vec d) (hJ : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q (p - pStar) (qStar - q)) P) (hJAdjBase : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q (pStar + p) (qStar + q)) P) : ∫ (a : RegCoeffField d), blockJObservableCubeSet Q p pStar q qStar a ∂P = 1 / 2 * expectedResponseJCubeSet P Q (p - pStar) (qStar - q) + 1 / 2 * expectedResponseJCubeSet P Q (pStar + p) (qStar + q)

The Ch4 block-response expectation is the half-sum of ordinary response expectations under adjoint-invariance.

theorem HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumSet_translation_covariant {d : ℕ} (p pStar q qStar : Vec d) : IsTranslationCovariant fun (U : Set (Vec d)) => blockJHalfResponseAdjointSumSet U p pStar q qStar

The Ch4 block response half-sum is translation-covariant as a set-indexed coefficient-field observable.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_blockJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hAdj : RestrictionAdjointInvariantLaw P) (Q : TriadicCube d) (p pStar q qStar : Vec d) : AEMeasurable (blockJObservableCubeSet Q p pStar q qStar) P

The Ch4 block response observable is a.e.-measurable under a law carrier and adjoint-invariant law.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_blockJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hAdj : RestrictionAdjointInvariantLaw P) (Q : TriadicCube d) (p pStar q qStar : Vec d) : MeasureTheory.AEStronglyMeasurable (blockJObservableCubeSet Q p pStar q qStar) P

The Ch4 block response observable is a.e.-strongly-measurable under a law carrier and adjoint-invariant law.

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

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

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

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

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.expectedDescendantsAverageBlockJCubeSet_eq_originCube_of_stationary {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (hAdj : RestrictionAdjointInvariantLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (p pStar q qStar : Vec d) : expectedDescendantsAverageBlockJCubeSet P (originCube d m) (m - n).toNat p pStar q qStar = expectedBlockJCubeSet P (originCube d n) p pStar q qStar

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

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

Under stationarity and childwise integrability, the expectation of the descendant-average block response observable is the annealed block response on the origin cube at the child scale.