LocalizationFluctuationJointBackground #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
hcomp and the measurability half of hbg, from one class hypothesis #
ABK26, l.approximate.recurrence.formula, Step 2.
What this module does #
LocalizationFluctuationMuMeasCell.integrable_meshFluctuationCellIntegrand'
carries two hypotheses whose content is measurability in the sample:
hcomp, for every test fieldYon the cell, ofomega |-> mu(a_omega; background_omega + Y);- the measurability half of
hbg, i.e. the same statement atY = 0.
This module reduces both, simultaneously and for every Y at once, to the
single statement
omega |-> [ background_omega ] is measurable into L^2(cell; R^{2d}) ,
i.e. to measurability of the background field's L^2 class. Adding a fixed
test field is a translation of the L^2 carrier, hence continuous, so the class
of background + Y is measurable as soon as the class of background is; and
LocalizationFluctuationJointField.measurable_doubledMuValue_meshCellCoeff_of_measurable_class
then converts a measurable class into a measurable energy.
The remaining obligation, stated exactly #
After this module the whole hcomp/hbg-measurability front is the single
proposition
Measurable (fun omega : CutoffSample d =>
toHilbertBlockL2OfBlockField
(memBlockL2_blockField (hpot omega) (hflux omega)))
at F = meshCellBackground M n h Kc e e' wD wN R. Its two legs are the
constant load P_z (whose sample measurability is proved at
PrincipalResponseLoadMeas.measurable_shellIndexSigma_principalPz) and
bfF_z, whose legs are the corrector gradients, proved as L^2 classes on
the localization cube cu_K at
Corrector.measurable_freshShell{Dirichlet,Neumann}GradL2. The one piece of
plumbing still missing between the two is the restriction of an L^2 class
from the localization cube to the mesoscopic cell, which
Corrector.CorrectorMeasurableGradient explicitly records as not built.
Binders #
Beyond the typing binders: [NeZero d]; the vector-L^2 membership of the two
legs of the background at every sample (a typing property of the corrector
data); and the class measurability. No integrability, no estimate, no
smallness, and no selection of any minimizer occurs.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formula, Step 2,e.Pz.def,e.Fz.def.
The class map is additive #
Adding a fixed test field translates the L^2 class of the background by a
constant, hence preserves measurability of the class.
The reduction of hcomp and of the measurability half of hbg #
The hcomp/hbg measurability front, reduced to one class hypothesis.
At every fixed competitor Y --- in particular at Y = 0, which is hbg ---
the doubled energy value of the shifted background is measurable in the sample,
given only that the background's own L^2 class is.
on hpot, hflux (typing), hYpot, hYflux (typing of the competitor) and
hclass. No estimate, no integrability and no selection.
hcomp of
LocalizationFluctuationMuMeasCell.integrable_meshFluctuationCellIntegrand', in
its own binder shape. Every test field on the cell is admissible at once.
The measurability half of hbg: the background energy itself.