Coarse-graining support: Support.Book.Ch04.Theorems.CoarseObservables #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Coarse-observable measurability from Mu #
This file is the public Chapter 4 handoff for the finite algebraic
consequences of RestrictionLawCarrier.aemeasurable_Mu_cubeSet.
The surface is deliberately law-facing and definition-facing: downstream code
gets measurability of Mu, the coarse block matrices, and response/block
quantities through manuscript identities. There are no provider structures and
no section-local wrapper tracks here.
Finite descendant averages preserve a.e.-measurability.
A locally a.e.-elliptic field has a deterministic coarse block matrix on
each triadic open cube, with the a.e. coefficient representative handled by the
Chapter 2 doubled-Mu theory.
The public cube-set coarse block matrix agrees with the Chapter 2 coarse block matrix built from the canonical a.e.-elliptic coefficient representative on the cube.
A law carrier almost surely supplies deterministic coarse block matrix existence on every fixed triadic open cube.
Origin-cube specialization of
RestrictionLawCarrier.ae_exists_coarseBlockMatrix_openCubeSet.
The lower-right coarse entry σ_*⁻¹(U; a)ᵢⱼ is a.e.-measurable on a
deterministic triadic cube.
The upper-left coarse entry b(U; a)ᵢⱼ is a.e.-measurable on a
deterministic triadic cube.
Law-relative local-test representative for an upper-left coarse block
entry on a fixed triadic cube. The representative is constructed from the
canonical Mu representatives and agrees a.e. with the raw coarse entry.
Law-relative local-test representative for a lower-right coarse block
entry on a fixed triadic cube. The representative is constructed from the
canonical Mu representatives and agrees a.e. with the raw coarse entry.
The upper-right mixed coarse entry is a.e.-measurable on a deterministic triadic cube.
The lower-left mixed coarse entry is a.e.-measurable on a deterministic triadic cube.
The full unfolded coarse block matrix is a.e.-measurable.
The upper-left block b(U; a) is a.e.-measurable as a matrix-valued
observable.
The upper-right block of the doubled coarse matrix is a.e.-measurable.
The lower-left block of the doubled coarse matrix is a.e.-measurable.
The lower-right block σ_*⁻¹(U; a) is a.e.-measurable as a matrix-valued
observable.
The mixed observable σ_*⁻¹(U; a)κ(U; a), represented as the negative
lower-left block, is a.e.-measurable as a matrix-valued observable.
The full unfolded starred inverse coarse block matrix is a.e.-measurable.
Finite descendant averages of Mu over child cubes are a.e.-measurable.
Finite descendant averages of upper-left coarse entries are a.e.-measurable.
Finite descendant averages of upper-right coarse entries are a.e.-measurable.
Finite descendant averages of lower-left coarse entries are a.e.-measurable.
Finite descendant averages of lower-right coarse entries are a.e.-measurable.
Compose an a.e.-measurable observable with adjointing the coefficient field when the law is adjoint-invariant.
The adjointed Mu observable is a.e.-measurable under an adjoint-invariant
law.
ResponseJ is a.e.-measurable whenever the manuscript identity expressing
it as Mu(U; (-p,q)) - p·q holds almost surely.
Under a law carrier, the deterministic Chapter 2 identity
ResponseJ = Mu(-p,q) - p·q holds almost surely on each deterministic
triadic cube.
The scalar response observable is a.e.-measurable under a law carrier.
Finite descendant averages of ResponseJ are a.e.-measurable whenever each
child response is almost surely identified with the corresponding Mu
observable.
Finite descendant averages of scalar response observables are a.e.-measurable under a law carrier.
The adjointed ResponseJ observable is a.e.-measurable whenever the
manuscript identity expressing it through adjointed Mu holds almost surely.