CutoffCoarseBlockRepresentative #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Canonical measurable coarse-block representatives for cutoff coefficients #
The literal Chapter-2 homogenization error contains a maximum over all doubled unit directions. Consequently its measurable realization must start with one common representative of the entire finite coarse block matrix on each cube, not with independently chosen representatives for individual directions.
This file supplies that common representative. It is A.mk of
CoarseGraining's a.e.-measurable coarse full-block observable and comes with
the explicit almost-everywhere identification to the raw coarse matrix. The
final homogenization-error representative will be its finite-dimensional
continuous functional once that functional's equality with CoarseGraining's
literal sphere maximum has been proved.
The literal full coarse block matrix of the actual cutoff coefficient. This is kept separate from its representative so that their a.e. identification is explicit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The raw cutoff full coarse block is a.e.-measurable under the genuine canonical cutoff-sample law.
The common coarse-block representative on actual cutoff samples. It is the
canonical A.mk of the literal full block, hence it retains a single common
a.e. event for every matrix entry and every direction.
Equations
- Algsuperdiff.Section3.Observable.cutoffCoarseFullBlockRepresentative M coefficientScale Q = AEMeasurable.mk (Algsuperdiff.Section3.Observable.cutoffCoarseFullBlockRaw M coefficientScale Q) ⋯
Instances For
The cutoff coarse-block representative is measurable on the genuine canonical cutoff-sample probability space.
The cutoff representative is a.e. equal to the literal full coarse block matrix of the actual coefficient cutoff. This is the explicit bridge that a future error provider must consume before replacing CoarseGraining's literal error by a measurable finite-dimensional functional.
Evaluate the common full coarse-block representative in the public doubled block-response quadratic form. This is the finite-dimensional observable from which both the sphere maximum in the homogenization error and the directional Section 3.5 response are formed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fixed-load evaluation of the common representative is measurable.
One common a.e. event identifies all doubled block responses at a fixed
cube with evaluations of the one full-matrix representative. The universal
quantifiers over P and Qv are inside the event: this is deliberately
stronger than a family of direction-indexed a.e. equalities, and prevents an
uncountable union of exceptional sets in the later sphere maximum.
The finite-dimensional unit-sphere maximum associated to a full coarse block.
This is deliberately the same maximum domain as CoarseGraining's literal
normalizedBlockResponseMax: the doubled Euclidean normalization is written
with fullBlockVecNormSq, rather than replacing it by a convenient norm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The compact Euclidean unit sphere used to parameterize the literal
fullBlockVecNormSq = 1 directions. We use the Euclidean carrier only for
topology; fullBlockVecOfUnitSphere below returns CoarseGraining's exact
function-valued direction.
Equations
Instances For
Convert a compact Euclidean-sphere direction into CoarseGraining's literal doubled vector carrier.
Equations
Instances For
The Euclidean sphere parameterization has exactly CoarseGraining's squared-norm normalization, not an equivalent or rescaled substitute.
The joint finite-dimensional quadratic response on the exact compact direction sphere.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The continuous-map packaging of the finite-dimensional quadratic response as a function of a compact direction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The compact-direction response map is continuous in the finite coarse matrix. Consequently its norm is an everywhere measurable scalar functional even off the physical locally elliptic support.
The globally continuous, hence everywhere measurable, finite-dimensional candidate for the normalized block-response maximum. Its equality with the literal supremum is asserted only on the locally elliptic physical event.
Equations
Instances For
The matrix functional used for a measurable error representative is continuous on every full coarse block matrix.
Turn an exactly normalized CoarseGraining full block vector back into the compact Euclidean sphere used by the continuous representative.
Equations
Instances For
On any full coarse matrix whose normalized quadratic response is nonnegative on
the literal unit sphere, the norm of the continuous compact representative is
exactly CoarseGraining's sSup expression. The nonnegativity premise is
deliberately explicit: arbitrary values of an A.mk representative need not be
physical off its probability-one event.
On every cutoff sample, the literal normalized block-response maximum is the finite-dimensional sphere maximum of the literal full coarse matrix. The proof first changes only the compatible coefficient representative, then uses the single locally elliptic field to identify every direction at once.