GammaTenAssemblySide #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The analytic side conditions of the per-cube fluctuation bound #
ABK26, Step 2 of l.approximate.recurrence.formula, at the carrier of
e.lower.bound.localization.terms.
The gap this module fills #
LocalizationFluctuationPerCube.perCube_localizationFluctuation_le is stated
with eight analytic side conditions --- the six L^2 memberships hwDmem,
hwNmem, hY1, hY2, h, h at the normalized cube measure, and the two
spatial integrabilities hInt1, hInt2 of the gauged pairing integrands ---
which its own docstring records as "conditional A obligations of this module,
discharged by the caller at its carrier". This module discharges all eight,
once and for all, at the carriers a consumer of Step 2 reads them at.
Nothing here is a source display: every statement below is a transport between
two spellings of L^2 on one triadic cube, an application of the block
ellipticity bound of Section24.Sensitivity.Provider.Path.Densities, or a
Cauchy--Schwarz.
What is proved #
memLp_two_normalizedCubeMeasure_of_memVectorL2--- the transport, and the exact converse of CoarseGraining'smemVectorL2_cubeSet_of_memLp_normalizedCubeMeasure: the normalized cube measure is a finite scalar multiple ofvolume.restrict (cubeSet R), and the cube boundary is Lebesgue null, so the three spellingsMemVectorL2 (openCubeSet R),MemVectorL2 (cubeSet R)andMemLp _ 2 (normalizedCubeMeasure R)agree. Every membership below is produced in theMemVectorL2spelling and pushed through it.memLp_two_gradH10_normalizedCubeMeasure_of_subset---hwDmem, from CoarseGraining'sH1Function.grad_memVectorL2restricted to the cell.memLp_two_neumannFluxField_normalizedCubeMeasure---hwNmem; the stream forcing is continuous, hence in everyL^pof a bounded cube.memLp_two_localizationFz_fst/..._snd---h,h, from the provedLocalizationActualBackground.memVectorL2_localizationFz_{potential,flux}.memLp_two_blockMatVecMul_blockMatrixField_fst/..._snd---hY1,hY2. This is theCoeffOn.Lam-boundedness step:bfA(a)has a.e. bounded blocks becauseais uniformly elliptic (lam <= . <= Lam), so it maps vectorL^2to vectorL^2. The work is CoarseGraining-side and was already carried out inSection24.Sensitivity.Provider.Path.Densities.memVectorL2_blockMatrixField_{fst,snd}; what is added here is only the transport of the carrier.memVectorL2_potential_of_isDoubledResponseField/..._flux--- the twoL^2legs of a response field, i.e. the projections ofIsDoubledResponseField = IsDoubledAmbientField ∧ (Euler--Lagrange)(Homogenization.Book.Ch02.DoubledResponse). These are what a caller has about the fieldtilde S_zthat the split produces.memVectorL2_cubeFluctuationVecandintegrableOn_gaugedPairing_fst/..._snd---hInt1,hInt2: the gauged block image isL^2, the gauged fluctuation ofbfF_zisL^2(a constant is subtracted from anL^2field on a finite-measure set), and Cauchy--Schwarz pairs them.
The eight are consumed together, in the order and shape
perCube_localizationFluctuation_le reads them, by
Closure.GammaTenAssemblyCell.
Binders #
The geometry hsub : openCubeSet R ⊆ openCubeSet Q (which is what makes the
correctors of the localization cube Q readable on the cell R) and, for the
two hY statements and the two integrabilities, the two L^2 legs of the
response field. No estimate, no smallness, no moment and no measurability in
the sample occurs: everything below is spatial, at one fixed sample point.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.Pz.def,e.Fz.def.
The two carrier transports #
The transport of item 1: vector L^2 on the cell becomes L^2 of the
normalized cube measure.
This is the converse of CoarseGraining's
memVectorL2_cubeSet_of_memLp_normalizedCubeMeasure.
The two L^2 legs of a response field #
The potential leg of a doubled response field is vector L^2: it is the
first projection of IsDoubledAmbientField.
The flux leg of a doubled response field is vector L^2.
hwDmem and hwNmem #
hwDmem. The gradient of an H^1_0(cu_K) corrector is L^2 of the
normalized measure of every cell of cu_K.
hwNmem. The flux leg field grad w_N + shom^{-1} h e' of e.Pz.def
is L^2 of the normalized measure of every cell: the gradient by
H1Function.grad_memVectorL2, the stream forcing because it is continuous.
h and h #
hF1. The potential leg of bfF_z is L^2 of the normalized measure of the
cell.
hF2. The flux leg of bfF_z is L^2 of the normalized measure of the
cell.
hY1 and hY2: the CoeffOn.Lam-boundedness step #
hY1. The potential component of bfA(a) T is L^2 of the normalized
cube measure whenever both legs of T are vector L^2.
The content is the uniform ellipticity of a (lam <= . <= Lam), which bounds
the four blocks of blockMatrixField a a.e.; that step is CoarseGraining-side,
proved as
Section24.Sensitivity.Provider.Path.memVectorL2_blockMatrixField_fst.
hY2. The flux component of bfA(a) T is L^2 of the normalized cube
measure whenever both legs of T are vector L^2.
hInt1 and hInt2: Cauchy--Schwarz of two L^2 fields #
The cube fluctuation of a vector-L^2 field is vector L^2: a constant is
subtracted, and the cell has finite measure.
hInt1. The potential-leg gauged pairing integrand is integrable on the
cell: both factors are vector L^2 there.
hInt2. The flux-leg gauged pairing integrand is integrable on the cell.