BigLambdaSensitivity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Lambda-half of the coefficient switch, at the manuscript's cube #
LambdaCovariance.lean transports the multiscale lower ellipticity from the
frozen unit-cube gauge to the manuscript's cube z + square_m, and
LambdaTransfer.lean / LambdaSensitivityTwin.lean read the frozen
lambda-sensitivity switch there. This module is the exact Lambda
counterpart: it transports Lambda_{s,q} to the same carrier and reads the
frozen e.big.Lambda.sensitivity (ABK26) at it.
The consumer is the middle of Step 1 of p.bfA.multiscalebound, which passes
Lambda_{1/4,2}(z + square_j; a_L)
<= C Lambda_{1/4,2}(z + square_j; a_j)
+ C (|(k_L - k_j)| + 3^j ||grad (k_L - k_j)||)^2
lambda^{-1}_{1/4,2}(z + square_j; a_j) ,
i.e. e.big.Lambda.sensitivity at the cube z + square_j.
The smallness gate, and how it is discharged #
e.big.Lambda.sensitivity is the second display of Lemma l.J.sensitivity: in
the manuscript it carries the same constant C and the same smallness
condition e.J.sensitivity.smallness.condition as e.J.sensitivity. In the
Lean rendering the two displays are two frozen theorems,
Algsuperdiff.Frozen.Section24.responseJ_sensitivity and
Algsuperdiff.Frozen.Section24.bigLambda_sensitivity, each with its own
existential constant.
DeltaOsc.lean therefore normalizes the manuscript's delta_osc against
sensitivityConstMax d = max 1 (max (max C_lambda C_J) C_BigLambda), the
three-way maximum that restores the manuscript's single-constant reading. The
bad-event chain not B_osc and not B_loc ==> gate of JSmallness.lean and
LambdaSensitivityTwin.lean consequently opens the Lambda gate too, and the
..._of_notMem_bad_ae conclusions below carry no gate hypothesis at all. The
..._of_gate forms are kept as the deterministic, omega-free core: their
hypothesis is the manuscript's own e.J.sensitivity.smallness.condition,
read at the cube, so no proof step has migrated into a hypothesis either way.
Main results #
coarseBMatrixNorm_cutoff_translateCutoffSample,LambdaSq_cutoff_translateCutoffSample,LambdaSq_originCube_dilate: the translation and dilation covariance ofLambda_{s,q}for the actual coefficient cutoff.unitCubeBigLambda_unitRescaledCutoffCoeff: theLambda-transfer,unitCubeBigLambda s q (a_n rescaled) = Lambda_{s,q}(z + square_m; a_n).unitCubeBigLambda_eq_of_aeeq,unitCubeBigLambda_perturbCoeffOn_unitRescaledCutoffCoeff: the frozenLambdagauge is an a.e. invariant, and the perturbed rescaleda_nis the rescaleda_Linside it.LambdaSq_le_of_gate:e.big.Lambda.sensitivityat the manuscript's cube and at the honest fielda_L, from the smallness gate, with the dimension-only constantbigLambdaSensitivityConst d.oscThreshold_le_two_pow_neg_nine_mul_inv_bigLambdaSensitivityConst_mul_sigmaBar,gradientW1Infinity_incrementUnitCube_le_bigLambdaGate_notMem_bad_ae: theLambda-constant mirror of thee.we.can.apply.cgchain.LambdaSq_le_of_notMem_bad_ae,LambdaSq_quarter_le_of_notMem_bad_ae: the gate discharged —e.big.Lambda.sensitivityat the manuscript's cube holds almost surely onnot B_osc and not B_loc, with no smallness hypothesis.
References #
- ABK26 (
l.J.sensitivity, one constant and one smallness condition for both displays; second displaye.big.Lambda.sensitivity). - ABK26,
e.Bosc.def,e.delta.osc.choice. - ABK26,
p.bfA.multiscalebound,e.we.can.apply.cg. - ABK26 (
p.bfA.multiscalebound, Step 1). - ABK26 (the definitions (2.22)--(2.23)).
One-cube translation covariance of |b| #
One-cube translation covariance of |b(Q; a)| for the actual coefficient
cutoff. This is the b-half of
coarseSigmaStarInvMatrixNorm_cutoff_translateCutoffSample, read off the same
covariance of the coarse block matrix.
Translation covariance of the multiscale upper ellipticity #
Deterministic translation covariance of Lambda_{s,q}. For the actual
coefficient cutoff, the multiscale upper ellipticity on an arbitrary triadic
cube Q equals the one on the centered cube of the same scale, evaluated at the
sample translated by the base point triadicCubeShift Q of Q.
Dilation to the unit cube #
Scale normalization of Lambda_{s,q}. The multiscale upper ellipticity
of a family on the centered scale-m cube is that of its 3^{-m}-dilation on
the unit cube.
The Lambda-transfer #
The Lambda-transfer identity. The multiscale upper ellipticity of the
cutoff a_n on the cube Q = z + square_m is the frozen unit-cube gauge
unitCubeBigLambda of the rescaled coefficient object. This is the exact
analogue of the proved unitCubeLambda_unitRescaledCutoffCoeff.
The frozen scalar unitCubeBigLambda only depends on the coefficient field
up to a.e. equality. This is the Lambda-mirror of
Section24.Sensitivity.Provider.Lambda.unitCubeLambda_eq_of_aeeq.
The #J-smallness identification, read at the frozen unit-cube upper gauge:
the frozen perturbation of the rescaled a_n by the rescaled literal increment
k_L - k_n has the same Lambda_{s,q} as the rescaled a_L.
The frozen constant of e.big.Lambda.sensitivity #
The fixed-factor constant of e.big.Lambda.sensitivity is
Algsuperdiff.Section3.Provider.BadEvents.bigLambdaSensitivityConst, extracted
in DeltaOsc.lean next to the lambda- and J-sensitivity constants and
merged with them into sensitivityConstMax; its frozen conclusion is
bigLambda_sensitivity_const there. Only the free-delta variant, which has
no counterpart among the manuscript's displays, is extracted here.
e.big.Lambda.sensitivity at the manuscript's cube #
e.big.Lambda.sensitivity at the translated triadic cube (ABK26, the
statement display; its proof is; consumed). If the increment k_L - k_n
satisfies the manuscript's smallness condition
e.J.sensitivity.smallness.condition at the cube Q = z + square_m, then for
every s in (0, 3/8),
Lambda_{s,2}(Q; a_L)
<= 4 Lambda_{s,2}(Q; a_n)
+ C (3/8 - s)^{-1} ||k_L - k_n||^2 lambda_{s,2}^{-1}(Q; a_n) ,
with C = bigLambdaSensitivityConst d the dimension-only frozen constant.
Every carrier is the manuscript's own cube, and the field on the left is the
honest a_L, not a perturbed object; the increment gauges are the normalized
quantities of IncrementBridge.lean.
The gate discharged on the bad-event complement #
The constant chain of ABK26, at the Lambda-sensitivity constant: the
e.Bosc.def threshold is below 2^{-9} C_{(e.big.Lambda.sensitivity)}^{-1} sigmabar_j. This is the mirror of
oscThreshold_le_two_pow_neg_nine_mul_inv_responseSensitivityConst_mul_sigmaBar
and of its lambda twin, available because delta_osc is normalized against
the maximum of the three frozen constants — which is what ABK26's single
constant C_{(e.J.sensitivity.smallness.condition)} (label) says.
The Lambda-gate on a good cube: the mirror of
gradientW1Infinity_incrementUnitCube_le_responseGate_ae at the
Lambda-sensitivity constant. Almost surely, on not B_osc(z + square_j) and
not B_loc(z + square_j) and under the induction state, the frozen gate
quantity of the rescaled increment k_L - k_j satisfies the manuscript's
e.J.sensitivity.smallness.condition at the gauge lambda_{3/8,2} of
the rescaled a_j, for every L >= j.
e.big.Lambda.sensitivity on the bad-event complement (ABK26,
consumed). Almost surely, on not B_osc(z + square_j) and not B_loc(z + square_j) and under the induction state at a scale above j = Q.scale, for
every L >= j and every s in (0, 3/8),
Lambda_{s,2}(z + square_j; a_L)
<= 4 Lambda_{s,2}(z + square_j; a_j)
+ C (3/8 - s)^{-1} ||k_L - k_j||^2 lambda_{s,2}^{-1}(z + square_j; a_j) .
This is LambdaSq_le_of_gate with its smallness hypothesis discharged by
gradientW1Infinity_incrementUnitCube_le_bigLambdaGate_notMem_bad_ae, exactly
as responseJ_le_of_notMem_bad_ae discharges the response half.
The instance on the bad-event complement: s = 1/4, q = 2, at the cube
Q = z + square_j, with no smallness hypothesis.