FluxCorrectedRepresentative #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The measurable flux-corrected (∞,2) representative #
Algsuperdiff.Section4.Support.ErrorAtoms records the literal flux-corrected
observable fluxCorrectedError — the (∞,2) homogenization error of
a_L − (k_L − k_m)_Q on □_k — and its L ≥ m supremum in [0,∞]. As at
(∞,2) in Section 3, the literal is not measurable by composition.
The proved Section 3 chain (Observable/CutoffCoarseBlockRepresentative.lean,
Observable/CutoffHomogenizationErrorRepresentative.lean) is built for
Cutoff.coefficientCutoff specifically: its a.e.-measurable coarse-block
input comes from Cutoff.coefficientCutoffLaw_lawCarrier, the Chapter 4
RestrictionLawCarrier of the pushforward of the cutoff sample law along
coefficientCutoff. This module re-derives that input at the flux-corrected
field, and reuses everything downstream of it verbatim.
The re-derivation has exactly three ingredients.
- The flux-corrected field is a genuine carrier element and the map into the
carrier is genuinely measurable:
a_L − (k_L − k_m)_QisCutoff.coefficientCutoff M.nu L ωplus the constant carrier fieldconstRegCoeffField (−(k_L − k_m)_Q(ω)), whose sample dependence is measurable bymeasurable_fluxIncrementAverage_entry. BothRegCoeffFieldlanes of the constant summand are handled directly: the pointwise lane is an entry evaluation, and the entry-test lane is(k_L−k_m)_Q(ω)_{ij} ∫ φ. - Every sample of the flux-corrected field is locally a.e.-uniformly
elliptic, because the subtracted matrix is skew (so the symmetric part is
still
ν Id) and its entries are uniformly bounded on each cube. - Hence the pushforward law is a Chapter 4
RestrictionLawCarrier, which supplies CoarseGraining's a.e.-measurable coarse full-block observable.
Nothing else changes: normalizedBlockResponseMaxRepresentativeFunctional, the
compact-sphere identification
normalizedBlockResponseMaxFromFullCoarseBlock_eq_representativeFunctional_of_nonneg
and the geometric scale sum are exponent- and coefficient-agnostic and are used
exactly as proved.
Main definitions #
fluxCorrectedRegField,fluxCorrectedCoeffFamily— the carrier field and its canonical Chapter 2 triadic family.fluxCorrectedErrorRepresentative— the genuine measurable representative.fluxCorrectedErrorObservableSup,fluxCorrectedErrorObservableSqSup— thesup_{L ≥ m}observables ofp.mathcalE.annular.decomp(§B4).
References #
- ABK26,
p.mathcalE.annular.decomp.
The flux-corrected coefficient as a carrier field #
The flux-corrected coefficient a_L − (k_L − k_m)_Q as an element of
CoarseGraining's regular-fields carrier: the cutoff coefficient plus a constant
carrier field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The flux-corrected carrier field is a genuinely measurable function of the cutoff sample.
Local uniform ellipticity of every flux-corrected sample #
The uniform entry envelope of the flux-corrected field on a cube R: the
proved cutoff envelope on R plus the entry mass of the constant shift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The upper ellipticity constant of the flux-corrected field on a cube R.
Equations
Instances For
Every flux-corrected sample lies in CoarseGraining's Chapter 4 local
a.e.-uniform ellipticity carrier: the subtracted matrix is skew, so the
symmetric part is still ν Id, and on each cube the entries are uniformly
bounded.
The canonical Chapter 2 triadic coefficient family of the flux-corrected field. It is CoarseGraining's own dependent family construction at the witness above; no new family is introduced.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The literal flux-corrected error of ErrorAtoms is exactly CoarseGraining's
homogenization error on the canonical family of the flux-corrected field.
The Chapter 4 law carrier of the flux-corrected law #
The pushforward of the cutoff-sample law along the flux-corrected carrier
map is a Chapter 4 RestrictionLawCarrier.
The flux-corrected coarse-block representative #
The literal full coarse block matrix of the flux-corrected coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The common coarse-block representative of the flux-corrected coefficient.
Equations
Instances For
The everywhere-defined normalized response functional of the common flux-corrected coarse-block representative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The literal normalized block-response maximum of the flux-corrected family is the finite-dimensional sphere maximum of its literal full coarse matrix.
At every fixed cube, the flux-corrected coarse-block representative realizes CoarseGraining's literal normalized response maximum almost everywhere.
A single probability-one event identifies the literal normalized maximum with its representative on every triadic cube.
The flux-corrected error representative #
The finite descendant maximum of the flux-corrected coarse-block representatives.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The nonnegative everywhere-defined functional of the flux-corrected error.
Unlike the proved (∞,2) cutoff chain, no A.mk is needed at this layer:
every descendant maximum above is genuinely measurable, so the geometric
scale sum is too.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper-wide assumption 2 ≤ d, stored in the model, supplies the
nonzero-dimension instance required by CoarseGraining's doubled-response A.
The genuine measurable, nonnegative representative of the flux-corrected
(∞,2) error 𝓔_{s,∞,2}(□_k; a_L − (k_L − k_k)_{□_k}, σ_k Id).
Equations
Instances For
The flux-corrected representative is almost everywhere exactly the literal
flux-corrected error of ErrorAtoms.
The public sup_{L ≥ m} observables #
The sup_{L ≥ m} 𝓔_{s,∞,2}(□_m; a_L − (k_L − k_m)_{□_m}, σ_m Id) of
p.mathcalE.annular.decomp, taken in [0,∞] so that no convergence side
condition enters the statement.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The squared supremum sup_{L ≥ m} 𝓔_{s,∞,2}(…)², the left-hand side of the
main display of p.mathcalE.annular.decomp read literally (the square is
inside the supremum, as printed).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A single probability-one event carries the per-L identities
simultaneously, because the index set is countable.