RealizationTransfer #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the stationary product-average transfer #
This file proves item of the corrector-limit design: for stationary
square-integrable fields X, Y on the abstract carrier and any triadic
cube Q,
E[ ⨍_Q (realize X) · (realize Y) ] = E[X · Y],
together with the corollaries that hang off it, in particular
E[ ‖realize X‖²_{L²(Q)} ] = E[|X|²].
This is the identity that converts every cube-averaged quantity appearing in
l.approximation.stationary.by.local and l.corrector.limit into a quantity of
the abstract stationary Hilbert space, where
Algsuperdiff/Section3/Provider/Corrector/StationaryCorrector.lean operates.
CoarseGraining does not supply this. Its stationarity transfer
Homogenization.Book.Ch04.integral_eq_of_isTranslationCovariantR_of_stationary
moves a set-indexed observable along an integer translation under
IsStationaryR, which is the wrong shape twice over: it is discrete, and it
moves the set rather than the field inside a spatial average.
The proof is Fubini on μ ⊗ (volume.restrict (cubeSet Q)) — legitimate exactly
because of the joint measurability established in Realization.lean — followed
by the real-shift Koopman transfer integral_comp_const_vadd for each fixed
point of the cube, which makes the inner integral constant in the space
variable.
, the stationary product-average transfer. The expectation of the cube
average of the pointwise product of two realizations equals the expectation of
the product itself, for every triadic cube. In the notation of ABK26,
E[⨍_{cu_K} X · Y] = E[X · Y].
, quadratic form. E[⨍_Q |realize X|²] = E[|X|²].
A realization that is square integrable on a cube is square integrable for the
normalized cube measure, the measure underlying CoarseGraining's cubeLpNorm.