ErrorAtoms #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Section 4 homogenization-error atoms #

The Section 4 good events and the annular decomposition (d.good.event.for.lambda; p.mathcalE.annular.decomp) read the homogenization-error functional at two exponent pairs and at two coefficient shapes that Section 3 does not already carry:

the (2,2) atoms 𝓔_{s,2,2}(z+□_n; a_{n−2}, σ_{n−2} Id) of 𝒢₂, and
the (∞,2) functionals of the flux-corrected coefficient a_L − (k_L − k_m)_{□_m} appearing on the left of e.mathcalE.annular.decomp.

Both are built from exactly the proved carriers: the frozen general-exponent functional Algsuperdiff.Frozen.Section24.unitCubeHomogenizationError (which is already quantified over p q : MultiscaleExponent), the triadic change of variables Algsuperdiff.Section3.Observable.unitRescaledCoeffOn, the coefficient cutoff Cutoff.coefficientCutoff M.nu L, and the running diffusivity Annealed.sigmaBar M k (already a PositiveScalar).

Translation convention #

Every declaration here is stated at the origin cube □_n, matching the Section 3 raw-observable discipline. The manuscript's translated atom at z + □_n is rendered by translating the sample, never the cube. Consumers therefore write

  annularErrorAtom M n s ∘ Cutoff.translateCutoffSample z

for the atom at z + □_n. The same convention applies to fluxCorrectedError. No identity between the translated rendering and a moved cube is asserted here; that is provider content.

Main definitions #

homogenizationErrorAtScale22 — the (2,2) sibling of Observable.homogenizationErrorAtScale.
cutoffHomogenizationErrorRaw22 — the (2,2) sibling of Observable.cutoffHomogenizationErrorRaw.
annularErrorAtom — the 𝒢₂ atom 𝓔_{s,2,2}(□_n; a_{n−2}, σ_{n−2} Id).
fluxIncrementAverage — the constant matrix (k_L − k_m)_Q.
fluxCorrectedCoeffOn — the coefficient a_L − (k_L − k_m)_Q on Q.
fluxCorrectedError — the (∞,2) functional of the flux-corrected coefficient, in [0,∞].

Measurability #

The literal 𝓔 observables are deliberately not claimed measurable here, and the omission mirrors the proved Section 3 layer exactly. The (∞,2) literal Observable.cutoffHomogenizationErrorRaw carries no genuine measurability theorem: Section 3 obtains a measurable observable by defining Observable.cutoffHomogenizationError to be the selected representative Observable.cutoffHomogenizationErrorRepresentative and recording its a.e. identity with the literal (Observable.cutoffHomogenizationErrorRaw_ae_eq_representative). The corresponding (2,2) representative — and the representative for the flux-corrected coefficient, whose constant shift is itself sample-dependent — are provider constructions and are not built in this support layer.

What is proved genuinely measurable here is fluxIncrementAverage: each of its entries is a Carathéodory cube integral of the stream increment, jointly measurable in (ω, x) by continuity in the point and measurability in the sample.

References #

ABK26, d.mathcal.E, (2.28); d.good.event.for.lambda; p.mathcalE.annular.decomp.

ErrorAtoms #

Section 4 homogenization-error atoms #

Translation convention #

Main definitions #

Measurability #

References #

The (2,2) homogenization error at one triadic scale #

The literal (2,2) cutoff observable #

The 𝒢₂ annular atom #

The cube-averaged flux increment (k_L − k_m)_Q #

Genuine measurability of the averaged flux increment #

The flux-corrected coefficient a_L − (k_L − k_m)_Q #

The flux-corrected (∞,2) error and its L ≥ m supremum #

The `(2,2)` homogenization error at one triadic scale #

The literal `(2,2)` cutoff observable #

The `𝒢₂` annular atom #

The cube-averaged flux increment `(k_L − k_m)_Q` #

The flux-corrected coefficient `a_L − (k_L − k_m)_Q` #

The flux-corrected `(∞,2)` error and its `L ≥ m` supremum #