LocalizationFluctuationBackgroundClass #

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

The Step-2 background's `L^2` class is measurable in the sample #

ABK26, l.approximate.recurrence.formula, Step 2, e.Pz.def, e.Fz.def, the background display.

The obligation this module discharges #

LocalizationFluctuationJointBackground reduced the whole hcomp/hbg measurability front of LocalizationFluctuationMuMeasCell.integrable_meshFluctuationCellIntegrand' to the single proposition

  omega |->  [ meshCellBackground M n h Kc e e' wD wN R omega ]

is measurable into L^2(z + cu_n; R^{2d}). This module proves it.

Method: the cube average cancels #

The Step-2 background is P_z + bfF_z, and both summands carry the cube average (grad w)_{z+cu_n}: P_z with a + sign (e.Pz.def) and bfF_z with a - sign (e.Fz.def). In the sum the average cancels, and PrincipalResponsePz.principalPz_add_principalFz records exactly that:

  P_z + bfF_z(x) = bfAhom^{-1/2} ( e' + grad w_D(x); e + grad w_N(x) + shom^{-1} h e' ) .

So the background is LocalizationActualBackground.localizationBackground, which does not depend on the localization cube at all, and no measurability of any cube average is needed.

The class of that field is then built on the localization cube cu_K, where the proved measurability lives, and restricted to the mesoscopic cell:

principalLoad_add splits off the constant bfAhom^{-1/2}(e'; e), whose class is the continuous linear blockVecToHilbertBlockL2Const (LocalizationFluctuationJointComponents.toHilbertBlockL2OfBlockField_const), and adding it back translates the class by that constant, which preserves measurability (LocalizationFluctuationJointBackground.measurable_toHilbertBlockL2OfBlockField_add_const);
what is left is the doubled class of the pair of scaled corrector gradients, assembled by LocalizationFluctuationJointComponents.measurable_toHilbertBlockL2OfComponents from its two vector legs;
each leg is a fixed scalar multiple of a proved measurable class: Corrector.measurable_freshShellDirichletGradL2 for the potential leg, and the difference grad w_N - (-streamForcing) of Corrector.measurable_freshShellNeumannGradL2 and Corrector.measurable_freshShellForcingL2 for the flux leg;
the passage from cu_K to z + cu_n is LocalizationFluctuationJointRestrict.measurable_toHilbertBlockL2OfBlockField_of_subset;
the sample carrier changes from ShellSeq d to CutoffSample d along measurable_subtype_coe.

No measurable selection occurs: the corrector families wD, wN are arbitrary families of weak solutions of e.def.w, exactly as in Corrector.CorrectorMeasurableGradient, and only their gradient classes are read.

Main results #

toHilbertBlockL2OfBlockField_congr, toHilbertVectorL2OfVecField_grad, toHilbertVectorL2OfVecField_const_smul --- the class-algebra bookkeeping.
memVectorL2_meshCellBackground_potential, ..._flux --- the two typing properties, so that a consumer never has to produce them by hand.
measurable_toHilbertBlockL2OfBlockField_meshCellBackground --- the class measurability itself, the exact statement LocalizationFluctuationJointBackground asks for.
measurable_doubledMuValue_meshCellBackground (the measurability half of hbg) and aemeasurable_doubledMuValue_meshCellBackground_add_testField (hcomp), both in the binder shape LocalizationFluctuationMuMeasCell.integrable_meshFluctuationCellIntegrand' consumes.

Binders #

Beyond the typing binders: [NeZero d]; the two MeasurableSpace/BorelSpace pairs on the doubled L^2 carriers (which every consumer in this cone carries, HilbertBlockL2 having no global Borel instance); the geometric membership of the cell in the mesh below the localization cube; and the two weak-solution properties of e.def.w for the corrector families. No integrability, no estimate, no smallness, no ellipticity and no selection 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 background display, e.def.w.

LocalizationFluctuationBackgroundClass #

The Step-2 background's L^2 class is measurable in the sample #

The obligation this module discharges #

Method: the cube average cancels #

Main results #

Binders #

Scope #

References #

Class-algebra bookkeeping #

The two legs of the background, as measurable classes on the large cube #

The background is cube-average free #

The typing properties of the background on a cell #

The background's class on the localization cube #

The class on a mesoscopic cell #

The two consumers #

The Step-2 background's `L^2` class is measurable in the sample #