PrincipalResponseSwitchActualShell #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the centered fresh shell h - (h)_{z+cu_n} at the frozen W^{2,∞} carrier #
Source displays in ABK26:
l.approximate.recurrence.formula(label), Step 3;- the gauge-switch chain of Step 3, whose first line conjugates by the doubled
shear of
e.Gh.defand replacesa_mbya_m - (h)_{z+cu_n}; e.good.local.events(label; display);- the fresh shell
h := k_m - k_{m-h}named.
What this module supplies #
ApproximateRecurrence.PrincipalResponseSwitchTransport transports the
gauge-switch chain to the manuscript's cube z + cu_n, but every one of its
statements carries the centered shell h - (h)_{z+cu_n} as an abstract
Algsuperdiff.Frozen.Section24.UnitCubeSkewW2Infinity d argument hfield
together with two binders about it:
hshift, the pointwise field decomposition at the rescaled unit cube;hgrad, the discounted gradient gate.
No constructor for that centered object existed in this repository: the proved
Provider.BadEvents.incrementUnitCube₂ is the uncentered rescaled increment,
and the proved identification of the rescaled coefficient fields
(Provider.BadEvents.unitRescaledCutoffCoeff_toCoeffField_ae_eq) is an
almost-everywhere statement, while hshift is quantified over every point.
This module builds the constructor and produces both binders.
The construction #
The frozen carrier UnitCubeSkewW2Infinity d stores a value field together
with separately stored first and second derivative fields, and every
structural obligation on the value field (MemLp ∞, skewness, and
HasWeakPartialDerivOn) is an almost-everywhere or distributional statement on
the open unit cube. Consequently the value field may be replaced by any
almost-everywhere equal field without touching the derivative data. That is
unitCubeSkewW2InfinityOfAEEq.
The centered shell is then built in two steps.
subConstShellsubtracts a constant antisymmetric matrix from a shell field. A shell field is a triple (value, first derivative, second derivative) with the twoHasFDerivAtlinks and pointwise antisymmetry; subtracting a constant changes only the value, so the derivative data -- and thereforecubeOscGauge,unitCubeDerivNorm,unitCubeSecondDerivNormandUnitCubeSkewW2Infinity.gradientW1Infinity-- are unchanged definitionally.centeredShellUnitCubereplaces the value field ofcubeUnitCube Q (subConstShell hbar _ (shellIncrement omega lowScale highScale))by the literal difference
of the two rescaled coefficient objects. The replacement is legitimate because the two fields agree almost everywhere on the open unit cube, by the provedx |-> a_hi^resc(x) - a_lo^resc(x) - hbarunitRescaledCutoffCoeff_toCoeffField_ae_eqat both scales together withshellIncrement_apply_eq_cutoff_sub.
Because the value field is now literally that difference, the binder hshift
becomes finite algebra on the coefficient carrier: perturbCoeffOn adds
t • h to the base field pointwise, so at t = 1 the required identity is
a_lo + (a_hi - a_lo - hbar) = a_hi - hbar.
What is produced here, and what is not #
Produced, unconditionally:
centeredShellUnitCube_shift-- the binderhshiftof every statement ofPrincipalResponseSwitchTransport, for every point;centeredShellUnitCube_gradientW1Infinity-- the binderhgrad's carrier identification: the centered shell's gradient gauge is the uncentered rescaled increment's, byrfl.
Produced, almost surely on the cutoff sample law:
responseSensitivityConst_mul_gradientW1Infinity_centeredShell_le_ae-- the binderhgraditself, atDelta = 3^{-(1/4)(m-h-n)_+}, from membership inProvider.BadEvents.goodLocalEventalone. It is the provedresponseSensitivityConst_mul_gradientW1Infinity_le_of_mem_goodLocalEvent_aewith itshcenteredbinder discharged by therflidentification above.
NOT produced here: the shell-size binder hshell, which is the subject of
PrincipalResponseSwitchActualShellSize.
Carriers #
- The localization cube is a free
TriadicCube d; the manuscript's `n = m - h- 16 ceil|log_3 gamma|
(e.recurrence.params`, label) is never hard-coded.
- 16 ceil|log_3 gamma|
- The two scales are free integers
lowScale <= highScale; in Step 3 they arem - handm. - The constant
hbaris a free antisymmetricMat d. The manuscript's own(h)_{z+cu_n}isApproximateRecurrence.freshShellCubeAverage, whose antisymmetry is the provedfreshShellCubeAverage_skew; the specialization iscenteredFreshShellUnitCube. cstardoes not occur in this module.
Weak partial derivatives are insensitive to the representative #
Homogenization.HasWeakPartialDerivOn U i u g is a family of integral
identities in u, so it only sees u through its class modulo null sets of
volume.restrict U. CoarseGraining exports the EqOn version of this fact
privately in two files; the almost-everywhere version is proved here, in
portable style.
Weak partial derivatives are unchanged when the function is modified on a null set of the restricted volume measure.
Unconditional: no caller-supplied proposition enters.
Replacing the value field of a frozen unit-cube W^{2,∞} object #
Representative change at the frozen W^{2,∞} carrier. Given a frozen
unit-cube object h and any coefficient field w that agrees with the value
field of h almost everywhere on the open unit cube, this is the frozen object
whose value field is literally w and whose first and second derivative
fields are those of h.
Every structural field of UnitCubeSkewW2Infinity that mentions the value is
an almost-everywhere or distributional statement on the open unit cube
(MemLp ∞, the skewness of the symmetric part, and HasWeakPartialDerivOn),
so all of them transfer.
: this statement holds only under the proposition supplied by its binder hw,
the almost-everywhere agreement of the two value fields. It is a provider A,
not a source-facing frozen declaration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The representative change does not move the value gauge either: the frozen
w1Infinity reads the value field only through an essential supremum.
Subtracting a constant antisymmetric matrix from a shell field #
The constant shift of a shell field. A shell field is a triple (value,
first derivative, second derivative) subject to two HasFDerivAt links and pointwise
antisymmetry; subtracting a constant antisymmetric matrix changes only the
value, and preserves all three conditions.
: this statement holds only under the proposition supplied by its binder hc,
the antisymmetry of the constant. It is a provider A, not a source-facing
frozen declaration.
Equations
- Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.subConstShell c hc g = ⟨((↑g).1 - ContinuousMap.const (HCPolySupport.Vec d) c, (↑g).2), ⋯⟩
Instances For
The constant shift is invisible to the manuscript's oscillation gauge
3^{2j} ||grad h||_{W^{1,infinity}(z+square_j)}, which reads derivatives only.
The centered fresh shell at the rescaled unit cube #
The rescaled centered shell as a shell field: h - hbar transported to
the unit cube by the manuscript's map y |-> z + 3^j y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The almost-everywhere identification of the rescaled coefficient-field difference with the rescaled centered shell, on the open unit cube.
This is the two-scale form of the proved
Provider.BadEvents.unitRescaledCutoffCoeff_toCoeffField_ae_eq: the constant
nu I of a_m = nu I + k_m cancels in the difference, leaving the literal
increment k_{highScale} - k_{lowScale}.
: this statement holds only under the proposition supplied by its binder hle,
the manuscript's m - h <= m. It is a provider A, not a source-facing frozen
declaration.
The centered fresh shell h - hbar at the frozen W^{2,∞} carrier.
Its value field is literally the difference of the two rescaled coefficient
objects of PrincipalResponseSwitchTransport, shifted by hbar; its stored
derivative fields are those of the rescaled literal increment. The first
property makes hshift a pointwise identity; the second makes the frozen
gradient gauge equal to that of the uncentered increment.
: this statement holds only under the propositions supplied by its binders --
hskew (antisymmetry of the centering constant) and hle (m - h <= m). It
is a provider A, not a source-facing frozen declaration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first caller binder: hshift #
The binder hshift of PrincipalResponseSwitchTransport, produced.
The manuscript's own field decomposition at the rescaled unit-cube carrier,
a_{m-h}(z + 3^n .) + (h - (h)_{z+cu_n}) = a_m(z + 3^n .) - (h)_{z+cu_n} ,
holds at every point, not merely almost everywhere: perturbCoeffOn adds
t . h to the base coefficient field pointwise, and the centered shell's value
field is by construction the literal difference of the two rescaled coefficient
objects.
Unconditional beyond the binders of centeredShellUnitCube: no further
caller-supplied proposition enters.
The second caller binder: hgrad #
Centering by a constant preserves the gradient gauge. The centered
shell's frozen gradientW1Infinity is that of the uncentered rescaled
increment k_{highScale} - k_{lowScale}.
Both the constant shift and the representative change leave the stored first
and second derivative fields untouched, and gradientW1Infinity reads nothing
else, so the identification is definitional.
Unconditional beyond the binders of centeredShellUnitCube.
The binder hgrad of PrincipalResponseSwitchTransport, produced.
Almost surely on the cutoff sample law, membership in the manuscript's own
event cQ(n, m-h, z) -- here goodLocalEvent M Ccg Q lowScale at the
localization cube Q of scale n and the coarse scale lowScale = m-h --
already gives the discounted gradient gate for the centered shell:
C_sens ||grad (h - (h)_{z+cu_n})|| <= 3^{-(1/4)(m-h-n)_+} lambda_{3/8,2}(z+cu_n; a_{m-h}) .
This is the proved
responseSensitivityConst_mul_gradientW1Infinity_le_of_mem_goodLocalEvent_ae
of PrincipalResponseSwitchTransport with its remaining binder hcentered
discharged by centeredShellUnitCube_gradientW1Infinity.
: this statement holds only under the propositions supplied by its binders --
hle (m - h <= m) and hskew -- and the membership hypothesis carried
inside the almost-sure conclusion.
The manuscript's own centering constant #
The centered fresh shell at the manuscript's own constant (h)_{z+cu_n} = freshShellCubeAverage, whose antisymmetry is the proved
freshShellCubeAverage_skew.
: this statement holds only under the proposition supplied by its binder hle.
It is a provider A, not a source-facing frozen declaration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binder hshift at the manuscript's own centering constant.
The binder hgrad at the manuscript's own centering constant.