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

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

Expectations and finite response moments

This file is the public Chapter 4 surface for taking expectations of the scalar response observables already exposed in CoarseObservables.

The surface is intentionally small: it names the observable, its expectation, the centered observable used in the manuscript, and the finite descendant average expectation theorem. Integrability remains an explicit theorem hypothesis; there is no extra moment carrier or section-local wrapper track.

theorem HCPolySupport.Book.Ch04.integral_vecDot_matVecMul_eq_entrywise_integral {d : ℕ} {P : RestrictionCoeffLaw d} {M : RegCoeffField d → Mat d} (hM : ∀ (i j : Fin d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => M a i j) P) (x y : Vec d) : ∫ (a : RegCoeffField d), vecDot x (matVecMul (M a) y) ∂P = vecDot x (matVecMul (fun (i j : Fin d) => ∫ (a : RegCoeffField d), M a i j ∂P) y)

Finite-dimensional matrix quadratic forms commute with entrywise expectation under entrywise integrability.

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

Scalar response observable on a deterministic triadic cube.

Equations

• HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet Q p q a = HCPolySupport.ResponseJ (HCPolySupport.cubeSet Q) p q a.toFun

@[simp]

theorem HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet_apply {d : ℕ} (Q : TriadicCube d) (p q : Vec d) (a : RegCoeffField d) : restrictionResponseJObservableCubeSet Q p q a = ResponseJ (cubeSet Q) p q a.toFun

theorem HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet_nonneg {d : ℕ} (Q : TriadicCube d) (p q : Vec d) (a : RegCoeffField d) : 0 ≤ restrictionResponseJObservableCubeSet Q p q a

The scalar response observable is pointwise nonnegative.

theorem HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet_ae_eq_quadratic_coarseBlockMatrix_of_lawCarrier {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : (fun (a : RegCoeffField d) => restrictionResponseJObservableCubeSet Q p q a) =ᵐ[P] fun (a : RegCoeffField d) => 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight q) - vecDot p q - vecDot q (matVecMul (coarseBlockMatrix (cubeSet Q) a.toFun).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft p)

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_restrictionResponseJObservableCubeSet_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube Q) P) : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q p q) P

Full coarse-block integrability makes the scalar response integrable.

The law carrier supplies the a.s. elliptic support and the deterministic ResponseJ = Mu(-p,q) - p·q identity; the only remaining analytic input is integrability of the finite-dimensional coarse block.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integral_restrictionResponseJObservableCubeSet_eq_quadratic_annealedBlockMatrix {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube Q) P) : ∫ (a : RegCoeffField d), restrictionResponseJObservableCubeSet Q p q a ∂P = 1 / 2 * vecDot q (matVecMul (annealedBlockMatrix P (cubeSet Q)).lowerRight q) - vecDot p q - vecDot q (matVecMul (annealedBlockMatrix P (cubeSet Q)).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (annealedBlockMatrix P (cubeSet Q)).upperLeft p)

Expected scalar response expressed through the annealed coarse block matrix, with the stochastic hypotheses packaged in RestrictionLawCarrier.

This is the note-facing Chapter 4 source identity: Ch5 should call this rather than passing deterministic coarse-data witnesses.

noncomputable def HCPolySupport.Book.Ch04.restrictionCenteredResponseJObservableCubeSet {d : ℕ} (Q : TriadicCube d) (p q p0 q0 : Vec d) : RegCoeffField d → ℝ

Centered scalar response observable on a deterministic triadic cube.

Equations

• HCPolySupport.Book.Ch04.restrictionCenteredResponseJObservableCubeSet Q p q p0 q0 a = HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet Q p q a - 1 / 2 * HCPolySupport.vecDot p0 q0

@[simp]

theorem HCPolySupport.Book.Ch04.restrictionCenteredResponseJObservableCubeSet_apply {d : ℕ} (Q : TriadicCube d) (p q p0 q0 : Vec d) (a : RegCoeffField d) : restrictionCenteredResponseJObservableCubeSet Q p q p0 q0 a = restrictionResponseJObservableCubeSet Q p q a - 1 / 2 * vecDot p0 q0

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

Annealed scalar response on a deterministic triadic cube.

Equations

• HCPolySupport.Book.Ch04.expectedResponseJCubeSet P Q p q = ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet Q p q a ∂P

theorem HCPolySupport.Book.Ch04.integral_restrictionResponseJObservableCubeSet_eq_quadratic_annealedBlockMatrix {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (Q : TriadicCube d) (p q : Vec d) (hData : ∀ᵐ (a : RegCoeffField d) ∂P, OpenCubeDeterministicCoarseData Q a.toFun) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube Q) P) : ∫ (a : RegCoeffField d), restrictionResponseJObservableCubeSet Q p q a ∂P = 1 / 2 * vecDot q (matVecMul (annealedBlockMatrix P (cubeSet Q)).lowerRight q) - vecDot p q - vecDot q (matVecMul (annealedBlockMatrix P (cubeSet Q)).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (annealedBlockMatrix P (cubeSet Q)).upperLeft p)

Expected scalar response expressed through the annealed coarse block matrix.

The only stochastic hypotheses are the deterministic coarse-data identity almost surely and integrability of the full coarse block. Scalarization is not used here; Ch5 gets its scalar formula by specializing this source identity.

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

Annealed finite descendant average of scalar responses.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.tauResponseJCubeSet {d : ℕ} (P : RestrictionCoeffLaw d) (Qchild Qparent : TriadicCube d) (p q : Vec d) : ℝ

Difference of two annealed scalar responses, the basic τ-type quantity.

Equations

• HCPolySupport.Book.Ch04.tauResponseJCubeSet P Qchild Qparent p q = HCPolySupport.Book.Ch04.expectedResponseJCubeSet P Qchild p q - HCPolySupport.Book.Ch04.expectedResponseJCubeSet P Qparent p q

theorem HCPolySupport.Book.Ch04.integrable_descendantsAverage {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {j : ℕ} {F : TriadicCube d → RegCoeffField d → ℝ} (hF : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (F R) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => descendantsAverage Q j fun (R : TriadicCube d) => F R a) P

Finite descendant averages preserve integrability.

theorem HCPolySupport.Book.Ch04.integral_descendantsAverage_eq_descendantsAverage_integral {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {j : ℕ} {F : TriadicCube d → RegCoeffField d → ℝ} (hF : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (F R) P) : ∫ (a : RegCoeffField d), descendantsAverage Q j fun (R : TriadicCube d) => F R a ∂P = descendantsAverage Q j fun (R : TriadicCube d) => ∫ (a : RegCoeffField d), F R a ∂P

Finite descendant averages commute with expectation under childwise integrability.

theorem HCPolySupport.Book.Ch04.memLp_descendantsAverage {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {j : ℕ} {r : ENNReal} {F : TriadicCube d → RegCoeffField d → ℝ} (hF : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (F R) r P) : MeasureTheory.MemLp (fun (a : RegCoeffField d) => descendantsAverage Q j fun (R : TriadicCube d) => F R a) r P

Finite descendant averages preserve MemLp.

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

Finite descendant averages of response observables are integrable if the child responses are integrable.

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

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

theorem HCPolySupport.Book.Ch04.integrable_restrictionCenteredResponseJObservableCubeSet {d : ℕ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsFiniteMeasure P] (Q : TriadicCube d) (p q p0 q0 : Vec d) (hJ : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q p q) P) : MeasureTheory.Integrable (restrictionCenteredResponseJObservableCubeSet Q p q p0 q0) P

Centering by a deterministic scalar preserves integrability.

theorem HCPolySupport.Book.Ch04.memLp_restrictionCenteredResponseJObservableCubeSet {d : ℕ} {P : RestrictionCoeffLaw d} {r : ENNReal} [MeasureTheory.IsFiniteMeasure P] (Q : TriadicCube d) (p q p0 q0 : Vec d) (hJ : MeasureTheory.MemLp (restrictionResponseJObservableCubeSet Q p q) r P) : MeasureTheory.MemLp (restrictionCenteredResponseJObservableCubeSet Q p q p0 q0) r P

Centering by a deterministic scalar preserves MemLp under a finite measure.

theorem HCPolySupport.Book.Ch04.integral_centeredResponseJ_eq_expectedResponseJ_sub_halfDot {d : ℕ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (Q : TriadicCube d) (p q p0 q0 : Vec d) (hJ : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet Q p q) P) : ∫ (a : RegCoeffField d), restrictionCenteredResponseJObservableCubeSet Q p q p0 q0 a ∂P = expectedResponseJCubeSet P Q p q - 1 / 2 * vecDot p0 q0

The integral of the centered response is the annealed response minus the deterministic centering scalar.

theorem HCPolySupport.Book.Ch04.integral_descendantResponseJAverages_eq_expectedResponseJAverages {d : ℕ} {P : RestrictionCoeffLaw d} (Q : TriadicCube d) (j : ℕ) (p q : Vec d) (hJ : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), descendantsAverage Q j fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a ∂P = expectedDescendantsAverageResponseJCubeSet P Q j p q

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

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_restrictionResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : AEMeasurable (restrictionResponseJObservableCubeSet Q p q) P

The named response observable is a.e.-measurable under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_restrictionResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : MeasureTheory.AEStronglyMeasurable (restrictionResponseJObservableCubeSet Q p q) P

The named response observable is a.e.-strongly-measurable under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_restrictionCenteredResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q p0 q0 : Vec d) : AEMeasurable (restrictionCenteredResponseJObservableCubeSet Q p q p0 q0) P

Centered response observables are a.e.-measurable under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_restrictionCenteredResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q p0 q0 : Vec d) : MeasureTheory.AEStronglyMeasurable (restrictionCenteredResponseJObservableCubeSet Q p q p0 q0) P

Centered response observables are a.e.-strongly-measurable under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_descendantsAverage_restrictionResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => descendantsAverage Q j fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a) P

Finite descendant averages of the named response observables are a.e.-measurable under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_descendantsAverage_restrictionResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => descendantsAverage Q j fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a) P

Finite descendant averages of the named response observables are a.e.-strongly-measurable under a law carrier.