SensitivityBridges #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The bridge layer of the Section 3.6 sensitivity injection #
It contains no estimate of the manuscript: every declaration below is either an exact identity, an exact normalization, a carrier transport, or a monotone comparison already proved elsewhere in the repository and re-read at the shape the injection needs.
The seams #
** The zeroth-order unit-cube bridge.** IncrementBridge.lean supplies
gradientW1Infinity_shellFieldUnitCube_le, the first-order half of the
frozen Section 2.4 gate. The zeroth-order half -- the one the frozen
remainder's h.w1Infinity term needs -- existed only as a private
declaration,
Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.w1Infinity_shellFieldUnitCube_le
at Provider/Diffusivity/ApproximateRecurrence/PrincipalResponseCentre.lean,
and private in Lean 4 is file-scoped: the name is genuinely unreachable from
any other module (machine-checked: importing that module and referring to the
name fails with unknown identifier). It is therefore re-proved here, in
public form, by exactly the route the private uses -- both components of
UnitCubeSkewW2Infinity.w1Infinity are eLpNorm ... ∞ on the literal open
unit cube, so pointwise bounds transfer -- together with the raw-norm corollary
that mirrors gradientW1Infinity_shellFieldUnitCube_le.
** The zeroth-order twin of the two-index bridge.** ABK26's
e.good.local.events gauge is measured on the rescaled unit cube; the proved
gradientW1Infinity_incrementUnitCube₂_le
(Provider/BadEvents/IncrementGaugeTwoIndex.lean) reads the first-order gate
through cubeOscGauge. Its zeroth-order twin is supplied here. The rescale
weights are exact and are the ones the manuscript's volume-normalized norms
carry (ABK26): for the map y |-> z + 3^l y,
‖rescaled‖_{L∞(square_0)} = ‖·‖_{L∞(z+square_l)} (weight 1),
‖∇ rescaled‖_{L∞(square_0)} = 3^l ‖∇·‖_{L∞(z+square_l)} (weight 3^l),
so w1Infinity of the rescaled increment is max { 3^l ‖∇(k_L-k_n)‖_{L∞(z+square_l)}, ‖k_L-k_n‖_{L∞(z+square_l)} }. Both sides are
carried here at the proved stream-level norms Stream.localCubeDerivNorm and
Cutoff.localCubeControl, and then at the two carriers the wave chain uses,
Stream.streamIncrementLinftyNorm and Stream.cubeSupBound.
** The rescale and gauge companions.** The response at the localization cube
is the response at the unit cube of the rescaled and translated data. The
translate half is the proved ResponseTransport.lean seam
(responseJ_cutoffFamily_eq_originCube_translate); the dilation half is
Ch02.responseJ_dilate at Ch02.TriadicCoeffFamily.isDilation_dilate. Their
composition proves exactly on BadEvents.unitRescaledCutoffCoeff, the carrier
at which the frozen responseJ_sensitivity and the proved lambda-transfer
are both stated. The 3^{4l} is the fingerprint of these weights and is
exhibited here: with the volume-normalized norm
‖f‖_{W^{2,∞}(z+square_l)} = max { ‖∇²f‖_∞, 3^{-l}‖∇f‖_∞, 3^{-2l}‖f‖_∞ },
both frozen gate quantities of the rescaled increment are below
3^{2l} ‖k_L-k_n‖_{W^{2,∞}(z+square_l)}, hence both squares -- the two terms
of the frozen remainder -- are below
3^{4l} ‖k_L-k_n‖²_{W^{2,∞}(z+square_l)}.
A qualification on the norm. ABK26 does not print a W^{2,p} definition:
the symbol ‖·‖_{W^{2,∞}} is used but never defined. The convention adopted
here is the one the wave lane states, in the equivalent 3^{2l}-normalized
form max{‖f‖_∞, 3^l‖∇f‖_∞, 3^{2l}‖∇²f‖_∞}; see the fidelity-convention block
of Provider/MultiscaleEstimate/WaveSizesZeroth.lean.
(b) The 1/8 -> 3/8 gauge conversion. The good event's ellipticity clause is
lambda_{1/8,2}(z+square_l; a_n) (GoodLocalEvents.lean carries it as the
binder hlam); the frozen sensitivity engine gates and prices at
lambda_{3/8,2} of the rescaled unit-cube field. The forward comparison is
proved as BadEvents.lambdaSq_le_unitCubeLambda_unitRescaledCutoffCoeff
(Provider/BadEvents/LambdaTransfer.lean), proved from
e.ellipticities.monotone.ordered (ABK26) in the Section-3 face
Provider/ErrorComparison/ExponentMonotonicity.lean (lambdaSq_mono_of_lt).
What the pricing step consumes is the reciprocal direction: the frozen
remainder's weights lambda_{3/8,2}^{-1} and lambda_{3/8,2}^{-2} must be
replaced by the event's own lambda_{1/8,2}^{-1}. That is supplied here, at
the literal observable and in the squared form the second remainder term
carries.
Main definitions #
Main results #
w1Infinity_shellFieldUnitCube_le,w1Infinity_shellFieldUnitCube_le_max.max_unitCubeValueNorm_cube,w1Infinity_cubeUnitCube_le,w1Infinity_incrementUnitCube₂_le.- (fingerprint)
underlineW2Gauge_nonneg,gradientW1Infinity_cubeUnitCube_le_underlineW2Gauge,w1Infinity_cubeUnitCube_le_underlineW2Gauge,gradientW1Infinity_sq_incrementUnitCube₂_le,w1Infinity_sq_incrementUnitCube₂_le. responseJ_cutoffFamily_eq_unitRescaledCutoffCoeff(an orientation face of the provedMultiscale.responseJ_unitRescaledCutoffCoeff).inv_unitCubeLambda_unitRescaledCutoffCoeff_le_inv_lambdaSq,inv_unitCubeLambda_le_inv_lambdaSq_oneEighth,inv_unitCubeLambda_sq_le_inv_lambdaSq_sq_oneEighth.
Name collisions #
w1Infinity_incrementUnitCube₂_lecollides on the short name withAlgsuperdiff.Section3.Provider.Multiscale.w1Infinity_incrementUnitCube₂_le. Same short name, same left-hand side(incrementUnitCube₂ Q n L omega).w1Infinity, different right-hand sides: that one bounds bymax (incrementOscGauge₂ Q n L omega) (cubeSupBound Q n L omega.1), the one here by the pair of raw scale-weighted cube norms. The two namespaces are disjoint, so nothing is ambiguous as things stand; a consumer that opens both...Provider.Localizationand...Provider.Multiscalewill have to disambiguate.dilateCubeis genuinely ambiguous in this file's scope --Homogenization.Book.Ch02.dilateCubeversusAlgsuperdiff.Section3.Provider.Stream.dilateCube-- and is therefore writtenCh02.dilateCubethroughout. So isMultiscaleExponent(Homogenization.MultiscaleExponentversusCh02.MultiscaleExponent).
The wave lane's carrier, and how it relates to this one #
- The wave lane's extended carrier
MultiscaleEstimate.waveGaugeW2and this file'sunderlineW2Gaugeare NOT the same normalization of the same object:waveGaugeW2 m h Ris a SUM,cubeSupBound R (l-h) m + waveGauge l m h (cubeCenter R), at the3^{2l}normalization‖f‖_∞ + 3^l‖∇f‖_∞ + 3^{2l}‖∇²f‖_∞;underlineW2Gauge Qis a MAX, at the reciprocal normalizationmax{‖∇²f‖_∞, 3^{-l}‖∇f‖_∞, 3^{-2l}‖f‖_∞}, and is at the suprema throughout. The bridge that the injection will eventually need,3 ^ (2 * Q.scale) * underlineW2Gauge Q (shellIncrement omega n L) ≤ waveGaugeW2 L h Q omega, is not carried out in this module. It is proved, at the constant1, asLambdaGateChain.three_zpow_mul_underlineW2Gauge_le_waveGaugeW2(with its squared formthree_zpow_mul_underlineW2Gauge_sq_le_waveGaugeW2_sq, which is the shape the injection remainder meets). No passage from a pointwise fidelity statement to the three suprema is needed:waveGauge's own summands are already at the suprema. They areStream.localCubeDerivNormandStream.localCubeSecondDerivNorm, which are by definition the exactL∞norms on the open cube. The route is layer subadditivity of those exact gauges (Stream.localCubeDerivNorm_sum_le,Stream.localCubeSecondDerivNorm_sum_le) applied toshellIncrement = ShellField.sum (Ioc (l-h) m), and it costs the constant exactly1.
References #
- ABK26: the only volume-normalized Sobolev norm the manuscript defines is
W^{1,p}, as(‖∇f‖^p_{L^p} + |U|^{-p/d}‖f‖^p_{L^p})^{1/p}, i.e.max{‖∇f‖, |U|^{-1/d}‖f‖}atp = ∞. That display is what fixes the weights used here; theW^{2,∞}symbol is used but never defined. - ABK26,
e.ellipticities.monotone.ordered. - ABK26,
l.J.sensitivity, stated atsquare_0. - ABK26,
e.good.local.events. - ABK26, the gauge pricing
e.J.sensitivity.appppatdelta = 1, with the3^{4l}.
The zeroth-order unit-cube bridge #
Pointwise bounds on the literal open unit cube bound the frozen
zeroth-order gate UnitCubeSkewW2Infinity.w1Infinity.
Both components of w1Infinity are essential suprema on the open unit cube, so
a pointwise bound A on the stored derivative and a pointwise bound B on the
value transfer to max A B.
This is the public re-proof of the unreachable private
w1Infinity_shellFieldUnitCube_le of
Provider/Diffusivity/ApproximateRecurrence/PrincipalResponseCentre.lean, by
that private's own route.
: the statement holds only under the propositions supplied by its binders hA,
hB, hderiv and hval. It is a provider A, not a source-facing frozen
declaration.
The zeroth-order gate of a shell field's unit-cube package is below the
raw unit-cube gauges of the shell field. This is the exact zeroth-order twin
of BadEvents.gradientW1Infinity_shellFieldUnitCube_le: the derivative gauge
replaces the second-derivative gauge and the value gauge replaces the derivative
gauge.
The zeroth-order twin of the two-index unit-cube bridge #
The exact zeroth-order normalization. The unit-cube derivative and
value gauges of the field rescaled by y |-> z + 3^l y are the 3^l- and
1-weighted cube gauges of the field on z + square_l.
This is the zeroth-order twin of BadEvents.max_unitCubeDerivNorm_cube; the
weights are the ones ABK26's volume-normalized norms carry.
The zeroth-order bridge at an arbitrary shell field. The frozen
zeroth-order gate of the field rescaled from z + square_l to the unit cube is
below the scale-weighted cube norms max { 3^l ‖∇h‖_{L∞(z+square_l)}, ‖h‖_{L∞(z+square_l)} }.
(fingerprint) The 3^{4l} weight #
The manuscript's volume-normalized W^{2,∞} gauge of a shell field on the
localization cube z + square_l (ABK26, read at p = ∞ and |U|^{1/d} = 3^l):
‖h‖_{W^{2,∞}(z+square_l)} = max { ‖∇²h‖_∞, 3^{-l}‖∇h‖_∞, 3^{-2l}‖h‖_∞ } .
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first-order gate of the rescaled field is 3^{2l} times the
manuscript's W^{2,∞} gauge, at worst.
The zeroth-order gate of the rescaled field is 3^{2l} times the manuscript's
W^{2,∞} gauge, at worst. Together with the first-order twin this is the
source of the 3^{4l}: the frozen remainder carries the squares of these two
quantities.
The 3^{4l} fingerprint, first-order term. The square of the frozen
first-order gate quantity of the rescaled increment -- the quantity multiplying
|p . q| in the frozen remainder -- is below
3^{4l} ‖k_L - k_n‖²_{W^{2,∞}(z+square_l)}.
The 3^{4l} fingerprint, zeroth-order term. The square of the frozen
zeroth-order gate quantity of the rescaled increment -- the quantity multiplying
|p|² in the frozen remainder -- is below
3^{4l} ‖k_L - k_n‖²_{W^{2,∞}(z+square_l)}.
** The composed rescale companion.** The demanded response of the cutoff
family at an arbitrary triadic cube R = z + square_l, at an arbitrary
coefficient scale L and arbitrary loads p, q, is the response at the
unit cube of the rescaled and translated data --
BadEvents.unitRescaledCutoffCoeff, which is exactly the carrier at which the
frozen responseJ_sensitivity and the proved lambda-transfer are both
stated.
Both halves are exact identities, so no constant is created: the manuscript's
dimension-only C is untouched by the transport, and the whole scale
bookkeeping sits in the 3^{4l} fingerprint proved above, not here.
The 1/8 -> 3/8 gauge conversion #
The reciprocal gauge conversion, in general form. For 0 < t < s and
admissible q, the frozen unit-cube weight lambda_{s,q}^{-1} of the rescaled
coefficient object is below the manuscript's own
lambda_{t,q}^{-1}(z + square_l; a_n).
This is the reciprocal of the proved forward comparison
BadEvents.lambdaSq_le_unitCubeLambda_unitRescaledCutoffCoeff
(e.ellipticities.monotone.ordered, ABK26, composed with the
translation-and-dilation covariance of lambda_{s,q}); the reciprocal
direction is legitimate because Ch02.lambdaSq is strictly positive for every
coefficient family.
The gauge conversion at the manuscript's own exponents. The frozen
engine's weight lambda_{3/8,2}^{-1} is below the good event's own
lambda_{1/8,2}^{-1}(z + square_l; a_n), at the literal multiscale
observable.
The squared form of the gauge conversion, which is what the second term of
the frozen remainder (|p . q| * gradientW1Infinity² * lambda^{-2}) carries.