LambdaSensitivityTwin #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The lambda-sensitivity twin of the response-J switch #
LambdaTransfer.lean proves the frozen lambda-sensitivity switch on the good
local event, and ResponseCongruence.lean proves the identification
unitCubeLambda s q (perturbCoeffOn (square_0) (a_n rescaled) (k_L - k_n) 1)
= unitCubeLambda s q (a_L rescaled) .
Composing the two turns the frozen conclusion, which is stated about the
perturbed coefficient object, into the manuscript's own statement about the
honest field a_L. That is what the localization consumer of ABK26 reads:
lambda^{-1}_{1/8,2}(z + square_l; a_m) 1_{Q(l,l-h,z)}
<= 2 lambda^{-1}_{1/8,2}(z + square_l; a_{l-h}) 1_{Q(l,l-h,z)} ,
the factor 2 being the manuscript's rendering of (1 + C |grad(k_m - k_{l-h})| lambda^{-1}_{3/8,2}) under the good event. This module keeps the factor
explicit rather than relaxing it to 2, so nothing is lost.
The bad-event half, and why it is here #
The mirror is exact: the threshold delta_osc is normalized against
sensitivityConstMax, which dominates both frozen constants
(DeltaOsc.lean), so the same constant chain 2^{-9} . 10 < 1 holds with
lambdaSensitivityConst in place of responseSensitivityConst.
Main results #
unitCubeLambda_inv_le_of_mem_goodLocalEvent_ae,lambdaSq_inv_le_of_mem_goodLocalEvent_ae: the twin — the good-eventlambda-switch read at the honest fielda_L, at the unit-cube carrier and at the manuscript's cube carrier.oscThreshold_le_two_pow_neg_nine_mul_inv_lambdaSensitivityConst_mul_sigmaBar,gradientW1Infinity_incrementUnitCube_le_lambdaGate_notMem_bad_ae: thelambda-constant mirror of thee.we.can.apply.cgchain.
References #
- ABK26 (the localization consumer).
- ABK26 (
p.bfA.multiscalebound, Step 1).
The twin on the good local event #
The lambda-sensitivity twin (ABK26). On the good local event Q(m, n, z), the multiscale lower ellipticity of the later field a_L is comparable
to that of a_n, at the unit-cube carrier:
lambda^{-1}_{s,q}(a_L rescaled)
<= (1 + C |grad(k_L - k_n)| lambda^{-1}_{3/8,2}(a_n rescaled))
lambda^{-1}_{s,q}(a_n rescaled) .
This is the frozen lambda-sensitivity conclusion of LambdaTransfer.lean with
its perturbed carrier rewritten as the honest rescaled a_L, exactly as
responseJ_le_of_notMem_bad_ae does on the response side.
The twin at the manuscript's carrier: the same comparison read at
lambda_{s,q}(z + square_m; .) itself.
The constant chain of ABK26, at the lambda-sensitivity constant:
the e.Bosc.def threshold is below
2^{-9} C_{(e.lambda.sensitivity)}^{-1} sigmabar_j. This is the mirror of
oscThreshold_le_two_pow_neg_nine_mul_inv_responseSensitivityConst_mul_sigmaBar,
available because delta_osc is normalized against the maximum of the two
frozen constants.
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
e.lambda.sensitivity.smallness.condition at the gauge
lambda_{3/8,2} of the rescaled a_j, for every L >= j.
The transfer on the bad-event complement #
Almost surely, on not B_osc(z + square_j) and not B_loc(z + square_j) and
under the induction state,
lambda^{-1}_{s,q}(a_L rescaled)
<= (1 + C |grad(k_L - k_j)| lambda^{-1}_{3/8,2}(a_j rescaled))
lambda^{-1}_{s,q}(a_j rescaled)
for every L >= j and every admissible (s, q) with s in (0, 1/2].
The same transfer at the manuscript's carrier lambda_{s,q}(z + square_j; .).