PrincipalResponseLoadMeas #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
NOTE: this module is an ordinary Provider helper / conditional A. The binder inventories below are informal descriptions only.
The fresh-shell measurability's load, at the display's own load #
Sources in ABK26:
- The sentence "Therefore, by independence of
bfA_{m-h}andG_{-(h)_{z+cu_n}} P_z(the latter is a function ofk_m - k_{m-h}), increasingMin\eqref{e.cgamma.constraints}if necessary,"; e.lower.bound.principal.one.pre(label);e.Pz.def(label; display), the load itself;e.Gh.def, the doubled shear that gauges it.
What this module supplies #
Measurable[Cutoff.shellIndexSigma (Set.Ioc n m)] W
for W : Cutoff.ShellSeq d -> BlockVec d. It was carried as a binder at an
abstract W by every consumer, including
PrincipalResponseLowerShellMeas.integral_blockQuadratic_shellSplit_eq_of_representative.
This module supplies it at the concrete load the display gauges, i.e. at
G_{-(h)_{z+cu_n}} P_z
= blockMatVecMul (blockGauge (-freshShellCubeAverage R omega n m))
(principalPz sigma omega n m e e' R (wD omega) (wN omega)) ,
named gaugedPrincipalLoadShell below, and then instantiates the hWmeas slot
of the consumer of PrincipalResponseLowerShellMeas at it.
The three legs, and where each one comes from #
The load has three sample-dependent ingredients, and each is reduced here to a
continuous functional of an already-proved measurable L^2 class over the
large cube cu_K:
- the averaged fresh shell
(h)_{z+cu_n} = freshShellCubeAverage R omega n mofe.Gh.def. Reading the directionPi.single j 1and the reciprocal scale-1, the fieldx |-> (k_m - k_n)(x) e_jis literally the negated forcing-streamForcing (-1) omega n m e_jofe.def.w, whoseL^2class is the provedCorrector.freshShellForcingL2; its fresh-block measurability isCorrector.measurable_freshShellForcingL2_shellIndexSigma; - the potential average
(grad w_D)_{z+cu_n}, from the provedCorrector.measurable_shellIndexSigma_freshShellDirichletGradL2; - the flux average
(grad w_N + shom^{-1} h e')_{z+cu_n}, whose integrand is the sum of the Neumann gradient andstreamForcing, hence whoseL^2class is the difference of the proved Neumann gradient class and the proved forcing class, both measurable for the fresh block.
The passage from an L^2 class on openCubeSet Q to the manuscript's cube
average over the localization cube R is cubeAverage_eq_of_coeFn_ae: for a
descendant R of Q, the restricted Lebesgue measure of openCubeSet Q,
further restricted to cubeSet R, is the plain restricted Lebesgue measure of
cubeSet R, so the class integrates against cubeAverage's own
measure and may be replaced by any of its representatives. The remaining
algebra -- blockGauge, matVecMul, inverseSqrtLoad, sqrtLoad and the
constants e, e' -- is finite and continuous.
The matrix side #
hB is discharged here as well, at an arbitrary representative of the matrix,
by transporting
Provider.Annealed.coefficientCutoffLaw_integrable_blockMatEntry_coarseBlockMatrix
across the two carrier changes that PrincipalResponseIndepWire already
performs for the integral. See integrable_blockMatEntry_of_representative.
Carriers, disclosed #
Every declaration below lives on the shell-sequence carrier Cutoff.ShellSeq d, which is the carrier integral_blockQuadratic_shellSplit_eq integrates
over. No extension along Subtype.val is needed for the load:
freshShellCubeAverage, principalPz and Corrector.streamForcing are all
already defined at Cutoff.ShellSeq d, and the corrector families are taken at
that carrier, exactly as the proved measurability lemmas of
Corrector.CorrectorMeasurableGradient take them.
gaugedPrincipalLoadShell_val records that at a genuine cutoff sample the load
below is PrincipalResponseIndepWire.gaugedSwitchLoad at principalPz.
The matrix is not a concrete term of this file either. Both declarations below
that mention it quantify over an arbitrary
B : Cutoff.ShellSeq d -> BlockMat d carrying the binder
∀ᵐ w ∂(Cutoff.cutoffSampleLaw M).toMeasure,
B w.val = PrincipalResponseIndepWire.switchCubeMatrix M L R w
produced by
PrincipalResponseLowerShellMeas.exists_measurable_representative_switchCubeMatrix,
and both are invariant under that almost-everywhere identification: B is read
only under an integral or an integrability statement. No value of B off the
lower-tail-good carrier is named, asserted or used anywhere below.
What this module does NOT supply #
It does not supply hW of
PrincipalResponseLowerShellMeas.integral_blockQuadratic_shellSplit_eq_of_representative:
the consuming statement below carries it as a binder, visible in its own
signature. hW is the second-moment integrability of the gauged load, i.e.
the standing moment content of e.nablaw.in.L.eight (label) together with a
fourth moment of the averaged fresh shell; no bound on either is asserted or
used anywhere below. Two ingredients that a later discharge of hW would need
are absent from this repository as of writing: any norm or moment estimate for
cubeAverageMat/cubeAverageVec, and any unconditional MemLp for the
corrector gradients on Cutoff.ShellSeq d.
hB is supplied, by integrable_blockMatEntry_of_representative below,
and that supply is free of good events and of any structural-law or (P4)
hypothesis; the one proposition it does carry is the representative binder
hBrep described under "Carriers, disclosed".
It does not supply hBmeas either: like the representative binder itself,
hBmeas is carried as a binder by the consumer below, and at this matrix it is
available from
PrincipalResponseLowerShellMeas.exists_measurable_representative_switchCubeMatrix.
It does not remove the independence binder hindep: that binder still stands on
ApproximateRecurrence.PrincipalResponseBudgetWire
exists_smallCoupling_principalEnergy_bound_of_centering
and on its predecessors, untouched by anything here.
It asserts nothing about the correctors beyond the two weak-solution properties
its binders name, and it constructs no measurable selection: the corrector
families wD, wN are arbitrary, exactly as in
Corrector.CorrectorMeasurableGradient.
Main results #
The public surface is the five declarations listed below, together with the two
component measurability legs of the Step-5 basket and their plain-measurability
corollaries (see the paragraph after the list); the remaining nine declarations
are private. The window-average bridge, the class-to-cube-average reduction,
the flux-average leg and the principalPz step stay private, because each is
consumed only by a later declaration in this file.
gaugedPrincipalLoadShell-- the load itself; it occurs in the two statements below, so it must be public.gaugedPrincipalLoadShell_val-- the bridge toPrincipalResponseIndepWire.gaugedSwitchLoad, hence toPrincipalResponseSwitchActualPerCube.switchCubeQuad. A consumer that starts from the display's per-cube quadratic form onCutoff.CutoffSample dneeds exactly this identity to reach the shell-carrier statement below.measurable_shellIndexSigma_gaugedPrincipalLoadShell-- thehWmeasinput.integrable_blockMatEntry_of_representative-- thehBinput of the same factorization, at any representative of the matrix. A consumer that instantiatesPrincipalResponseLowerShellMeas.integral_blockQuadratic_shellSplit_eq_of_representativeat any other load needs this one by name; it is therefore public rather than private.integral_blockQuadratic_shellSplit_eq_gaugedPrincipalLoadShell-- the consumer, withhWits only remaining integrability input.
Two of the component legs are also public, because the Step-5 basket of
Closure.Step5Basket needs them by name for its hmeasX, hmeasS, hAmem and
hvmem binders and there is no other route to them:
measurable_shellIndexSigma_freshShellCubeAverageand its full-sigma-algebra corollarymeasurable_freshShellCubeAverage;measurable_shellIndexSigma_cubeAverageVec_freshShellDirichletGradand its full-sigma-algebra corollarymeasurable_cubeAverageVec_freshShellDirichletGrad.
Publicizing changes no statement: the two shellIndexSigma legs are byte-stable
apart from the dropped private keyword, and the two corollaries are their
images under Cutoff.shellIndexSigma_le_borel.
References #
- ABK26, (the sentence and its parenthetical);
e.lower.bound.principal.one.pre(label);e.Pz.def(label);e.Gh.def;e.def.w.
Generic measurability bookkeeping #
From an L^2 class on the large cube to a cube average on a descendant #
Leg 1: the averaged fresh shell of e.Gh.def #
The averaged fresh shell (h)_{z+cu_n} is a measurable function of the
fresh shells (n, m] alone.
This is's parenthetical for the gauge factor of e.Gh.def. Conditional on the
single binder hR: the localization cube R is any descendant of the large
cube Q. No corrector and no solution property enters.
The averaged fresh shell is measurable for the full sigma-algebra. The
fresh-shell sigma-field is coarser than the ambient one
(Cutoff.shellIndexSigma_le_borel), so the statement above is the stronger one
and this is its plain-measurability corollary.
Leg 2: the potential average of e.Pz.def #
The potential average (grad w_D)_{z+cu_n} of e.Pz.def is a
measurable function of the fresh shells (n, m] alone.
Conditional on its binders hR (geometric membership of the localization cube)
and hwD (the zero-trace Dirichlet weak-solution property of e.def.w). The
corrector family is otherwise arbitrary: no measurability, continuity or
selection property is assumed, exactly as in
Corrector.measurable_shellIndexSigma_freshShellDirichletGradL2.
The potential average is measurable for the full sigma-algebra. The
plain-measurability corollary of the statement above, by
Cutoff.shellIndexSigma_le_borel.
Leg 3: the flux average of e.Pz.def #
The load P_z of e.Pz.def #
Internal. The localized principal load P_z of e.Pz.def is a
measurable function of the fresh shells (n, m] alone.
Conditional on its binders hR, hwD and hwN.
The gauged load G_{-(h)_{z+cu_n}} P_z #
The gauged load G_{-(h)_{z+cu_n}} P_z, at the shell-sequence carrier and at
the manuscript's own centering constant freshShellCubeAverage.
This is a definition and carries no propositional binder: wD and wN enter as
bare families, with no solution, measurability or selection property required of
them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At a genuine cutoff sample the load above is
PrincipalResponseIndepWire.gaugedSwitchLoad applied to principalPz, i.e. the
very load PrincipalResponseSwitchActualPerCube.switchCubeQuad conjugates.
This identity carries no propositional binder -- it is rfl, the two sides
being the same term read at the two carriers.
The hWmeas input of integral_blockQuadratic_shellSplit_eq, at the exact
gauged load.
The load G_{-(h)_{z+cu_n}} P_z is a measurable function of the fresh shells
(n, m] alone. This is the literal content of the parenthetical "the latter is
a function of k_m - k_{m-h}".
: this statement holds only under the propositions supplied by its binders, which are exactly three:
hR, the geometric membership of the localization cubeRin the depth-jdgrid below the large cubeQ;hwD, the zero-trace Dirichlet weak-solution property ofe.def.wfor the familywD;hwN, the mean-zero Neumann weak-solution property ofe.def.wfor the familywN.
hwD and hwN are the defining property of the correctors, not extra
assumptions about them: they are what e.def.w says, and at a concrete
consumer they are discharged by the produced-existence route of
Corrector.FreshShellExistence. Nothing is assumed about measurability,
continuity or selection of either family. This is a provider A, not a
source-facing frozen declaration.
The entrywise integrability of the coarse matrix #
The hB input of integral_blockQuadratic_shellSplit_eq, at the exact
matrix, in representative form. Every entry of any representative B of
PrincipalResponseIndepWire.switchCubeMatrix is integrable on the
shell-sequence carrier.
Integrability is invariant under the almost-everywhere identification the
binder hBrep supplies, so the statement is available at every representative
that
PrincipalResponseLowerShellMeas.exists_measurable_representative_switchCubeMatrix
can produce, and no value of B off the lower-tail-good carrier is read: the
transport only ever evaluates B on Subtype.val images, and only under an
integrability statement.
The route is the carrier transport of PrincipalResponseIndepWire
integral_blockMatEntry_switchCubeMatrix_eq run on integrability instead of on
the integral: push M.P.toMeasure back to the cutoff-sample law along
Subtype.val, replace B by switchCubeMatrix using hBrep, push forward
along Cutoff.coefficientCutoff to RegCoeffField d, and land on
Provider.Annealed.coefficientCutoffLaw_integrable_blockMatEntry_coarseBlockMatrix.
That last input is itself free of good events, of (P4) records and of any
structural-law hypothesis: it rests only on the deterministic coercivity nu
through the two cutoff moment lemmas of Cutoff. and Cutoff.
: this statement holds only under the propositions supplied by its binders,
here exactly the representative binder hBrep. In particular it carries no
ellipticity event and no good event. It is a provider A, not a source-facing
frozen declaration.
The consumer #
The independence factorization at the exact load, at any representative of the exact matrix.
Relative to PrincipalResponseLowerShellMeas
integral_blockQuadratic_shellSplit_eq_of_representative, two further inputs
are gone:
hWmeasis now the theoremmeasurable_shellIndexSigma_gaugedPrincipalLoadShellabove, at the concrete gauged loadG_{-(h)_{z+cu_n}} P_z, and in its place stand only the two weak-solution properties ofe.def.wthat the corrector displays already carry. The geometric membershiphRthat the load's cube average needs is the samehRthe annealed identification already needed, so no geometric binder is added;hB, the entrywise integrability of the coarse matrix, isintegrable_blockMatEntry_of_representativeabove, applied at the same representative binderhBrepthis statement already carries, so it too adds no binder.
The matrix stays abstract: B and its two properties hBmeas and hBrep are
binders here, exactly as in the direct predecessor of this statement in
PrincipalResponseLowerShellMeas, and at the display's own matrix both are
produced together by
PrincipalResponseLowerShellMeas.exists_measurable_representative_switchCubeMatrix
under the geometric inclusion cubeSet R ⊆ U. No value of B off the
lower-tail-good carrier is read.
Exactly one integrability input remains a binder here, and it is still open:
hW, the second-moment integrability of the gauged load. The independence
binder hindep of the downstream budget wire is likewise untouched, upstream of
this file.
: this statement holds only under the propositions supplied by its binders. It is a provider A, not a source-facing frozen declaration.