CenteredIdentification

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

From the local bad event to the centered homogenization error

Step 1 of the proof of ABK26's l.bad.event.probabilities reads: by e.bound.Lambdas.by.Es, on B_loc(z + square_j) the multiscale homogenization error at that cube is larger than a constant; the induction hypothesis e.new.induction.for.shom then bounds the probability.

This module proves a local version of the first half of that sentence and moves the resulting event to the centered cube where the induction state lives.

The two links

• one_lt_cubeHomogenizationErrorLiteral_of_mem_badLoc. The proved sharp two-sided comparison ErrorComparison.max_weightedEllipticity_le_one_add_two_mul_sq_add_sqrt_two_mul gives max{sigma^{-1} Lambda_{1/4,2}, sigma lambda_{1/4,2}^{-1}} <= 1 + 2 E^2 + 2^{1/2} E. On B_loc the left side exceeds 10, while at E <= 1 the right side is at most 1 + 2 + 2 = 5 < 10. Hence E > 1 on B_loc. (The manuscript's unspecified threshold constant C is chosen here as 1; the honest root of 2x^2 + 2^{1/2} x = 9 is 1.797....)
• badLoc_ae_le_preimage. Combining with the deterministic covariance of TranslationCovariance.lean and the translation invariance of the cutoff sample law, the event B_loc(z + square_j) is almost surely contained in the translate of the centered upper-tail event { E_{1/4,infinity,2}(square_j; a_j, sigma_j) > 1 }, whose probability is what the induction state controls.

Main results

• cubeHomogenizationErrorLiteral
• one_lt_cubeHomogenizationErrorLiteral_of_mem_badLoc
• badLoc_ae_le_preimage
• measureReal_badLoc_le_measureReal_centeredTail

References

• ABK26, l.bad.event.probabilities, Step 1.
• ABK26, e.bound.Lambdas.by.Es.

theorem Algsuperdiff.Section3.Provider.BadEvents.neZeroOfModel {d : ℕ} (M : ABKModel d) : NeZero d

Nonzero dimension, from the paper-wide assumption 2 <= d stored in the model.

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.quarter : { s : ℝ // 0 < s }

The exponent s = 1/4 of e.Bloc.def, in the positivity subtype used by the induction state d.mathcalS.def.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.quarter = ⟨1 / 4, Algsuperdiff.Section3.Provider.BadEvents.quarter._proof_1⟩

The literal multiscale homogenization error at an arbitrary cube

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeHomogenizationErrorLiteral {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : ℝ

The literal mathcal E_{1/4,infinity,2}(Q; a_{Q.scale}, sigma_{Q.scale} Id) of the actual coefficient cutoff at an arbitrary triadic cube. On the centered cube it is almost surely the proved observable Observable.cutoffHomogenizationError.

Equations

• One or more equations did not get rendered due to their size.

The two literal ellipticity observables as Chapter 2 quantities

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInvLiteral_eq {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : cubeLowerEllipticityInvLiteral M Q cutoffScale s q omega = (HCPolySupport.Book.Ch02.lambdaSq Q s (↑q) (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField (Cutoff.coefficientCutoff M.nu cutoffScale omega) ⋯))⁻¹

The literal inverse lower ellipticity of the cutoff is the Chapter 2 quantity of the canonical Chapter 4 coefficient family.

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticityLiteral_eq {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : cubeUpperEllipticityLiteral M Q cutoffScale s q omega = HCPolySupport.Book.Ch02.LambdaSq Q s (↑q) (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField (Cutoff.coefficientCutoff M.nu cutoffScale omega) ⋯)

The literal upper ellipticity of the cutoff is the Chapter 2 quantity of the canonical Chapter 4 coefficient family.

Step 1 of the manuscript's proof

theorem Algsuperdiff.Section3.Provider.BadEvents.one_lt_cubeHomogenizationErrorLiteral_of_mem_badLoc {d : ℕ} [NeZero d] (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {omega : Cutoff.CutoffSample d} (hlow : cubeLowerEllipticityInv M Q Q.scale (1 / 4) quarter._proof_1 exponentTwo omega = cubeLowerEllipticityInvLiteral M Q Q.scale (1 / 4) exponentTwo omega) (hup : cubeUpperEllipticity M Q Q.scale (1 / 4) quarter._proof_1 exponentTwo omega = cubeUpperEllipticityLiteral M Q Q.scale (1 / 4) exponentTwo omega) (hmem : omega ∈ badLoc M Q) : 1 < cubeHomogenizationErrorLiteral M Q omega

Step 1 of l.bad.event.probabilities. At any sample where the two measurable ellipticity representatives take their literal values, membership in B_loc(z + square_j) forces the multiscale homogenization error at that cube to exceed 1.

The manuscript's display is P[B_loc] <= P[E^2 > C]; the chosen threshold is the explicit E > 1, which is below the honest root 1.797... of 2x^2 + 2^{1/2} x = 9.

Transport to the centered cube

theorem Algsuperdiff.Section3.Provider.BadEvents.badLoc_ae_le_preimage {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : badLoc M Q ≤ᵐ[↑(Cutoff.cutoffSampleLaw M)] Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift Q) ⁻¹' {omega : Cutoff.CutoffSample d | 1 < Observable.cutoffHomogenizationError M Q.scale quarter omega}

Step 1 local event identification. The local bad event at z + square_j is almost surely contained in the translateCutoffSample-preimage of the centered upper-tail event { E_{1/4,infinity,2}(square_j; a_j, sigma_j) > 1 }.

The deterministic content is homogenizationErrorOnCube_translateCutoffSample; the null sets discarded are the two ellipticity-representative sets and the representative set of the centered observable, pulled back along the measure-preserving translation.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_badLoc_le_measureReal_centeredTail {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : (↑(Cutoff.cutoffSampleLaw M)).real (badLoc M Q) ≤ (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | 1 < Observable.cutoffHomogenizationError M Q.scale quarter omega}

The probability of the local bad event at z + square_j is bounded by the probability of the centered upper-tail event, by translation invariance of the cutoff sample law.