JSmallness

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The corrected response-J smallness gate on a good cube

This module proves a local version of the display e.we.can.apply.cg of ABK26, the J-smallness step of p.bfA.multiscalebound:

3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z+square_j)} 1_{not B(spx)}
  <=  delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j}
  <=  2^{-5} C_{(e.J.sensitivity.smallness.condition)}^{-1} sigmabar_j
  <=  C_{(e.J.sensitivity.smallness.condition)}^{-1} lambda_{1/4,2}(z+square_j; a_j) ,

and then transfers the last gauge to the exponent the frozen Section 2.4 sensitivity lemmas consume.

The three inequalities

• The first is the complement control of e.Bosc.def, proved as incrementOscGauge_le_oscThreshold (IncrementOscillation.lean).
• The second is the induction-state clause e.shom.h.bounds combined with e.delta.osc.choice, proved as oscThreshold_le_two_pow_neg_nine_mul_inv_lambdaSensitivityConst_mul_sigmaBar (LambdaSensitivityTwin.lean), at the lambda-sensitivity constant the chain below is read against. The factor used here is 2^{-9}, which is below the manuscript's 2^{-5}.
• The third is the complement of e.Bloc.def: lambda^{-1}_{1/4,2}(z+square_j; a_j) <= 10 sigma_j^{-1}, i.e. sigmabar_j <= 10 lambda_{1/4,2}(z+square_j; a_j), which proves the final local inequality in the chain because 2^{-9} . 10 < 1.

The exponent correction

The passage is the exponent monotonicity e.ellipticities.monotone.ordered at 1/4 < 3/8 composed with the translation-and-dilation covariance of lambda_{s,q}, i.e. the general lambdaSq_le_unitCubeLambda_unitRescaledCutoffCoeff of LambdaTransfer.lean read at t = 1/4; the manuscript's own inequality is the stronger one, so no strength is lost.

Why the assembled statements are almost-sure

e.Bloc.def is stated against the measurable representative cubeLowerEllipticityInv built by A.mk, of which no pointwise information is available; the last inequality of the chain divides by it and so needs its positivity, which holds almost surely (cubeLowerEllipticityInv_pos_ae). The same carrier phenomenon already governs lambda_transfer_ae in LambdaTransfer.lean. Every statement below is proved first in pointwise form with the positivity as an explicit binder, and then almost surely with that binder discharged.

Main results

• sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc: the not B_loc arithmetic.
• lambda_transfer_quarter_literal, lambda_transfer_quarter_ae: the t = 1/4 instance of the lambda-transfer, in pointwise and in almost-sure form.

References

• ABK26, p.bfA.multiscalebound, e.we.can.apply.cg.
• ABK26, e.Bosc.def, e.delta.osc.choice, e.Bloc.def.
• ABK26, e.ellipticities.monotone.ordered.

The not B_loc arithmetic

theorem Algsuperdiff.Section3.Provider.BadEvents.sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {omega : Cutoff.CutoffSample d} (homega : omega ∉ badLoc M Q) (hpos : 0 < cubeLowerEllipticityInv M Q Q.scale (1 / 4) sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc._proof_1 exponentTwo omega) : ↑(Annealed.sigmaBar M Q.scale) ≤ 10 * cubeLowerEllipticity M Q Q.scale (1 / 4) sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc._proof_1 exponentTwo omega

The complement of e.Bloc.def (ABK26), read as a lower bound on the coarse-grained lower ellipticity: since lambda^{-1}_{1/4,2}(z+square_j; a_j) <= 10 sigma_j^{-1}, we have sigmabar_j <= 10 lambda_{1/4,2}(z+square_j; a_j).

The lambda-transfer at t = 1/4

theorem Algsuperdiff.Section3.Provider.BadEvents.lambda_transfer_quarter_literal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (n : ℤ) (omega : Cutoff.CutoffSample d) : (cubeLowerEllipticityInvLiteral M Q n (1 / 4) exponentTwo omega)⁻¹ ≤ Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (unitRescaledCutoffCoeff M Q n omega)

The lambda-transfer at the exponent of e.Bloc.def, at the literal observable. The manuscript's lambda_{1/4,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 e.ellipticities.monotone.ordered at 1/4 < 3/8 composed with the translation-and-dilation covariance of lambda_{s,q}.

theorem Algsuperdiff.Section3.Provider.BadEvents.lambda_transfer_quarter_ae {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), cubeLowerEllipticity M Q n (1 / 4) sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc._proof_1 exponentTwo omega ≤ Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (unitRescaledCutoffCoeff M Q n omega)

The lambda-transfer at t = 1/4, at the representative used by e.Bloc.def.