LocalizationFluctuationDuality #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The duality leg of Step 2 at the genuine localization carriers #
Source display in ABK26: the first display of Step 2 of
l.approximate.recurrence.formula,
fint_{z+cu_n} tilde S_z . bfA_m tilde S_z
= fint_{z+cu_n} bfF_z . bfA_m tilde S_z
<= [ bfAhom^{1/2} bfF_z ]_{H^1} [ bfAhom^{-1/2} bfA_m tilde S_z ]_{H^{-1}} .
What this module does #
It composes, at the manuscript's own carriers,
- the gauge-conjugated duality bound of
CoarseEllipticity.abs_cubeAverage_blockVecDot_le_besovDualityConst(the inequality's companion),
obtaining hquad of
Variational.PerCubeFluctuationArithmetic.perCube_fluct_le at the localization
cell:
2 * doubledMuValue (cubeDomain R) a T <= besovDualityConst R s * (Bu * Bg) .
The volumeAverage (openCubeSet R) of the Chapter-2 pairing and the
cubeAverage R of the Besov layer are identified by
volumeAverage_openCubeSet_eq_cubeAverage; the cube boundary is Lebesgue null.
The mean-zeroness premises of the duality are discharged internally from
cubeAverageVec_localizationFz_{potential,flux}, i.e. from the structure of
e.Fz.def itself.
Binders #
hsub is the descendant geometry; hwN is the defining property of
w_{N,e'}^{(K)}; hT names tilde S_z. The remaining hypotheses -- the
exponent window hs, the gauge positivity hsig0, the four L^2 memberships,
the two cube integrabilities of the corrector fields, the two integrabilities
of the gauged pairing integrands, the sign of Bg and the four seminorm
envelopes -- are conditional A obligations of this module, discharged by the
caller at its carrier. They are not premises of the pinned source statement.
Scope #
No anchor, frozen theorem or external input is consumed, and there is no
sorry.
The two averages agree #
The Chapter-2 domain average over the open cube is the Besov layer's cube average: the cube boundary is Lebesgue null.
The duality leg #
** at the genuine localization carriers.**
fint_R tilde S_z . bfA_m tilde S_z <= besovDualityConst R s * ( Bu * Bg )
with Bu any envelope of the finite-depth negative q = 2 Besov seminorms of
bfAhom^{-1/2} bfA_m tilde S_z and Bg any envelope of the finite-depth
positive ones of bfAhom^{1/2} bfF_z.
This is the hquad leg of
Variational.PerCubeFluctuationArithmetic.perCube_fluct_le, with E the
Chapter-2 doubledMuValue of tilde S_z and the manuscript's generic C
pinned.
as described in the module docstring.