LambdaTransfer #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The lambda-transfer, and the unconditional good-event gates #
GoodLocalEvents.lean delivers the gate opening of ABK26 in two
layers: the unconditional cube-level bound against
lambda_{1/8,2}(z + square_m; a_n), and four helpers named
..._of_lambdaTransfer which carry the missing comparison
lambda_{1/8,2}(z + square_m; a_n) <= unitCubeLambda (3/8) 2 (a rescaled)
as an explicit binder. This module supplies that comparison and discharges the binder.
The two inputs #
- Exponent monotonicity
e.ellipticities.monotone.ordered(ABK26), proved locally inAlgsuperdiff.Section3.Provider.ErrorComparison.ExponentMonotonicity; here at the instancet = 1/8 < 3/8 = s,q = 2. - Translation and dilation covariance of
lambda_{s,q}, proved locally inLambdaCovariance.lean:unitCubeLambda s q (unitRescaledCutoffCoeff M Q n omega) = lambda_{s,q}(Q; a_n(omega)).
Why the discharged gates are almost-sure statements #
The event goodLocalEvent is stated against cubeLowerEllipticity, the
measurable representative of lambda_{1/8,2}(Q; a_n) built in
CubeEllipticity.lean from A.mk. A measurable representative agrees with
the literal observable only almost everywhere, and no pointwise information
about it is available. The comparison is therefore proved
- pointwise, at the literal observable
(
lambda_transfer_literal), and - almost surely, at the representative (
lambda_transfer_ae),
and the discharged gates inherit the almost-sure quantifier. This is a carrier
consequence of the repository's representative construction, not a weakening of
the manuscript statement; the manuscript's lambda_{1/8,2} is the literal
observable, for which the transfer is unconditional and pointwise.
Main results #
lambda_transfer_literal: the pointwise comparison at the literal multiscale observable.lambda_transfer_ae: the same comparison at the representative used bygoodLocalEvent, almost surely.gradientW1Infinity_incrementUnitCube₂_le_lambdaGate_ae,gradientW1Infinity_incrementUnitCube₂_le_responseGate_ae,lambda_sensitivity_of_mem_goodLocalEvent_ae: three conditional helpers ofGoodLocalEvents.lean, with thehlambinder discharged.perturbCoeffOn_unitRescaledCutoffCoeff_toCoeffField_ae_eq: the identificationa_L(z + 3^m .) = a_n(z + 3^m .) + (k_L - k_n)(z + 3^m .)at the unit-cube carrier, needed by the#J-smallness consumer (ABK26).
References #
- ABK26,
e.good.local.events. - ABK26,
e.ellipticities.monotone.ordered. - ABK26 (the
#J-smallness consumer).
The literal multiscale observable of the cutoff #
The exponent carrier q = 2 of e.good.local.events is CoarseGraining's
finite exponent 2.
The literal observable of CubeEllipticity.lean is CoarseGraining's
Ch02.lambdaSq of the compatible triadic family of the actual cutoff.
The lambda-transfer #
The lambda-transfer, in general form. For every 0 < t < s and every
admissible q, the manuscript's lambda_{t,q}(z + square_m; a_n) is below the
frozen Section 2.4 unit-cube gauge lambda_{s,q} of the rescaled coefficient
field. This is the composition of the exponent monotonicity
e.ellipticities.monotone.ordered with the translation-and-dilation covariance
of lambda_{s,q}.
The lambda-transfer, at the literal observable. The manuscript's
lambda_{1/8,2}(z + square_m; a_n) is below the frozen Section 2.4 unit-cube
gauge lambda_{3/8,2} of the rescaled coefficient field. This is the
composition of the exponent monotonicity e.ellipticities.monotone.ordered at
1/8 < 3/8 with the translation-and-dilation covariance of lambda_{s,q}.
The lambda-transfer, at the representative used by the good event.
Almost surely, the event's own cubeLowerEllipticity is below the frozen
unit-cube gauge of the rescaled coefficient field.
The unconditional gates #
The frozen lambda-sensitivity gate on the good event, unconditional:
the _of_lambdaTransfer binder of GoodLocalEvents.lean is discharged by
lambda_transfer_ae.
The frozen response-sensitivity gate on the good event, unconditional.
The lambda-sensitivity switch on the good event, unconditional: the
coefficient switch of ABK26, in the form used.
The perturbed unit-cube coefficient is the rescaled a_L #
The base point of a triadic cube, as used by the increment rescaling, is
CoarseGraining's triadicCubeShift.
The #J-smallness identification (ABK26). At the unit-cube carrier,
the frozen perturbation of the rescaled a_n by the rescaled literal increment
k_L - k_n is the rescaled a_L:
a_L(z + 3^m y) = a_n(z + 3^m y) + (k_L - k_n)(z + 3^m y)
almost everywhere on the open unit cube.