StationaryStrip #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: stationary transfer on arbitrary sets and the boundary-strip fraction #
The proof of part (i) of l.approximation.stationary.by.local needs two
ingredients beyond the cube-average transfer of
Algsuperdiff/Section3/Provider/Corrector/RealizationTransfer.lean:
- the stationary transfer over an arbitrary measurable set of finite volume,
E[∫_S g(x + ω) dx] = |S| E[g], which is what turns the first error termE[‖(η_{K,L} - 1) p‖²_{L²(cu_K)}]into(|Σ_{K,L}|/|cu_K|) E[|p|²]; and - the geometric half of
e.boundary.strip.volume: the set where CoarseGraining's cutoffHomogenization.QuantitativeCubeCutoff Q ρ₁ ρ₂is allowed to differ from1has volume fraction at most1 - ρ₁ ^ d ≤ d (1 - ρ₁).
The scalar Bernoulli core of the second item is
Algsuperdiff/Section3/Provider/Corrector/BoundaryStrip.lean; here it is
combined with CoarseGraining's exact boundary-layer volume
Homogenization.volume_cubeBoundaryLayer_toReal_of_nonneg_le_half.
Joint integrability of (ω, x) ↦ g (x +ᵥ ω) over the product of the sample
space with a set of finite volume. This is the Fubini hypothesis behind the
set-indexed stationary transfer.
Set-indexed stationary transfer. For a stationary integrable observable
g and a measurable set S of finite volume, E[∫_S g(x + ω) dx] = |S| · E[g]. Taking S a triadic cube recovers; taking S the boundary strip of
the paper's cutoff is what produces e.boundary.strip.volume.
Integrability in the sample of the set integral of a stationary observable.
The set-indexed transfer for the squared norm of the realization of a
square-integrable stationary field:
E[∫_S |(realize X) (x)|² dx] = |S| E[|X|²].
Integrability in the sample of the set integral of the squared norm of a realization.
Per-sample square integrability on an arbitrary set. For almost every
sample the spatial realization of a stationary L² field is square integrable
on any measurable set of finite volume. This is the general-set companion of
Algsuperdiff.Section3.Provider.Corrector.ae_memHilbertVectorL2_realize.
A concentric closed subcube of ratio ρ contains the inward shrinking of
the half-open cube by the absolute amount (1 - ρ) / 2.
The set on which a concentric cutoff of inner ratio ρ may differ from 1
inside a triadic cube is contained in the boundary layer of thickness
(1 - ρ) / 2.
A concentric closed subcube of ratio ρ < 1 sits inside the open cube;
this is what makes the cutoff product compactly supported in cu_K.
e.boundary.strip.volume, geometric half. The volume of the set where a
concentric cutoff of inner ratio ρ ∈ [0, 1] may differ from 1 inside a
triadic cube is at most (1 - ρ ^ d) times the volume of the cube.