DoubledPairingResponse #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Poincare leg of Step 2 at a doubled response field #
Source displays in ABK26: Step 2 of l.approximate.recurrence.formula,
- The doubled coarse-grained Poincare inequality
e.CG.Poincare.doubled.varsofr.cg.poincare.doubled.variables, which bounds theH^{-1}-side seminorm ofbfAhom^{-1/2} bfA_m tilde S_zlinearly in|| bfA_m^{1/2} tilde S_z ||; - The ellipticity display, whose gauged sum is reached here through
sqrt_mul_add_inv_sqrt_mul_sq_le_two_mul.
What this module supplies #
DoubledCoarsePoincare.lean states the Poincare inequality for the explicit
fields doubledStateField / doubledFluxField of a primal/adjoint cube-solution
pair. The Step-2 consumer instead holds an abstract doubled response field T
-- the tilde S_z produced by LocalizationRecurrenceMesh -- and needs the
finite-depth negative q = 2 seminorms of the two components of
bfAhom^{-1/2} bfA_m T, which is the shape in which
LocalizationFluctuationDuality.two_mul_doubledMuValue_le_besovDualityConst_localizationFz
consumes them.
Three things bridge the gap.
Ch02.doubledResponseTheory ... |>.response_space_by_solutionsturnsIsDoubledResponseFieldinto a solution pair(v, v^*)withT = doubledFieldOfSolutionsalmost everywhere (e.findSfull).- The a.e.-congruence kit below transports the negative seminorms and the
mu-value across that null set. CoarseGraining carries only the pointwisecubeAverage_congr_on_cubeSet; the a.e. version is proved here by unfolding the depth averages -- each depth-jterm is adescendantsAverageof cube averages, and a.e. equality on the parent restricts to every descendant. - The
BddAbovekit discharges the boundedness premises ofBlockBesovPositive.cubeBesovNegativeVectorPartialSeminormTwo_*_le_blockNegativeBesovTwofrom the sameMemVectorL2and truncation data thatDoubledCoarsePoincare.leanalready uses.
doubledPoincareEllipticityFactor is the display's own factor, and
doubledPoincareEllipticityFactor_sq_le records the arithmetic link in the
gauged form 2 (sigma_0^{-1} Lambda + sigma_0 lambda^{-1}) that the
ellipticity display consumes.
Binders #
0 < s < 1 is the exponent window of the CoarseGraining coarse Poincare
package (the manuscript names s = 1 and discards to s = gamma); 0 < sigma_0 is the source's own positivity of the scalar sigma_0 of
e.form.of.A.naught; [NeZero d] is typing, dischargeable from the standing
d >= 2. No smallness, moment, measurability or integrability proposition
occurs, and no proposition about the coefficient family beyond its own
CoeffOn data is assumed.
Scope #
No anchor, frozen theorem or external input is consumed, and there is no
sorry.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2;r.cg.poincare.doubled.variables;e.findSfull;e.bfA.magic.swapping.
The a.e.-congruence kit for the negative seminorms #
The cube average sees the function only a.e. on the cube.
The vector cube average sees the field only a.e. on the cube.
A.e. equality on a cube restricts to every subcube.
The closed and open cube carry the same restricted Lebesgue measure.
The depth-j negative block average is an a.e. functional.
The depth-j negative seminorm is an a.e. functional.
The missing a.e.-congruence. The finite-depth negative q = 2 seminorm
sees the field only a.e. on the cube. This is what transports the Poincare
bound of DoubledCoarsePoincare.lean, stated for the explicit solution field, to
the abstract response field that agrees with it off a null set.
The boundedness kit #
Boundedness of the finite-depth negative seminorms of a scaled sum.
Boundedness of the finite-depth negative seminorms of a scaled difference.
The first component of the flux carrier is bounded in the seminorm scale.
The second component of the flux carrier is bounded in the seminorm scale.
The mu-value and the flux carrier across the null set #
The mu-value sees the doubled field only a.e. on the domain.
e.bfA.magic.swapping across the null set. For a doubled field agreeing
a.e. with the field of a solution pair, the gauged bfA-image is a.e. the
display's own flux carrier.
The Poincare ellipticity factor, in square-root form #
The lower factor lambda_{s,q}^{-1/2} as a square root.
The upper factor Lambda_{s,q}^{1/2} as a square root.
The ellipticity factor of e.CG.Poincare.doubled.vars at q = 2, in the
gauge of e.form.of.A.naught.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The arithmetic link. The square of the display's ellipticity factor is 32 c_{s,2}^{-1} times the gauged ellipticity sum sigma_0^{-1} Lambda_{s,2} + sigma_0 lambda_{s,2}^{-1}.
The Poincare leg at a doubled response field #
e.CG.Poincare.doubled.vars at an abstract doubled response field.
For T a doubled response field of a on the cube R, every finite-depth
negative q = 2 seminorm of either component of bfAhom^{-1/2} bfA T is at most
the display's ellipticity factor times || bfA^{1/2} T ||_{L^2(R)}, and the
mu-value of T is nonnegative.
This is the hpoin/hsq pair of
Variational.PerCubeFluctuationArithmetic.perCube_fluct_le, with
blockE = sqrt (2 mu).
on the exponent window, the gauge positivity and [NeZero d] only; see the
module docstring's binder census.