GoodLocalEllipticity

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

The coarse-ellipticity clause of the good local sensitivity event

ABK26 defines, in e.good.local.events, for m, n integers and a centre z, the good local sensitivity event

Q(m,n,z) := { C_sens sup_{L >= n} 3^{2m} ||grad (k_L - k_n)||_{W^{1,infinity}(z+square_m)}
              <= (1/2) C_{(e.cg.ellip.lower)}^{-1} 3^{-(1/2)(n-m)_+} sigmaBar_{n-1}
              <= 3^{-(1/4)(n-m)_+} lambda_{1/8,2}(z+square_m; a_n) } .

The displayed event is a chain of two inequalities. This module defines and proves a local version of the second one — the comparison of the middle threshold with the coarse-grained lower ellipticity of the cutoff field a_n on the cube — as a measurable event goodLocalEllipticity, and proves the exact identification of its complement with the second event of the manuscript's own decomposition of not Q(m,n,0) in the proof of l.bad.event.lemma,

{ lambda^{-1}_{1/8,2}(square_m; a_n) sigmaBar_{n-1} > 2 . 3^{(1/4)(n-m)_+}
    C_{(e.cg.ellip.lower)} } .

Carrier and constant conventions (recorded)

• The centre z is carried by a TriadicCube d, exactly as for the bad events of Definitions.lean: Q.scale = m is the cube scale and cubeSet Q = z + square_m with z in 3^m Z^d. The manuscript writes z in R^d; every consumer of e.good.local.events instantiates z in a triadic lattice, and this repository has no multiscale ellipticity observable on off-grid translates.
• C_{(e.cg.ellip.lower)} is carried as an explicit real parameter Ccg. Its source is the constant of e.cg.ellip.lower in p.cg.ellipticity.bounds, whose frozen statement Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds is now proved and available to consumers. This conditional A remains parametrized by Ccg; downstream assemblies may instantiate it from the frozen export, while every statement below that uses it carries 0 < Ccg explicitly.
• lambda_{1/8,2}(z+square_m; a_n) is the measurable representative cubeLowerEllipticity, defined as the pointwise inverse of the proved representative cubeLowerEllipticityInv of lambda^{-1}_{1/8,2}. Since Ch02.lambdaSq is a real number and the literal observable is its inverse, the double inverse is the literal lambda exactly (cubeLowerEllipticityInvLiteral_inv_eq).

Main definitions

• scaleGapPos: the manuscript's positive part (n - m)_+.
• cubeLowerEllipticity: measurable representative of lambda_{s,q}(Q; a_r).
• goodLocalThreshold: the middle term (1/2) Ccg^{-1} 3^{-(1/2)(n-m)_+} sigmaBar_{n-1} of e.good.local.events.
• goodLocalEllipticity: the second inequality of e.good.local.events, as an event.

Main results

• cubeLowerEllipticityInvLiteral_pos, cubeLowerEllipticityInv_pos_ae.
• measurable_cubeLowerEllipticity, cubeLowerEllipticity_ae_eq_literal, cubeLowerEllipticityInvLiteral_inv_eq.
• measurableSet_goodLocalEllipticity.
• notMem_goodLocalEllipticity_iff: the exact equivalence with the manuscript's coarse-ellipticity failure event, at a point where the representative of lambda^{-1} is positive.
• compl_goodLocalEllipticity_ae_eq, measureReal_compl_goodLocalEllipticity: the same identification almost everywhere, and the resulting equality of probabilities — the first reduction in the proof of l.bad.event.lemma.

References

• ABK26, e.good.local.events.
• ABK26, l.bad.event.lemma.
• ABK26, p.cg.ellipticity.bounds (e.cg.ellip.lower).

The scale gap

def Algsuperdiff.Section3.Provider.BadEvents.scaleGapPos (m n : ℤ) : ℝ

The manuscript's positive part (n - m)_+ of the scale gap between the cutoff scale n and the cube scale m.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.scaleGapPos m n = max (↑n - ↑m) 0

theorem Algsuperdiff.Section3.Provider.BadEvents.scaleGapPos_nonneg (m n : ℤ) : 0 ≤ scaleGapPos m n

theorem Algsuperdiff.Section3.Provider.BadEvents.scaleGapPos_of_le {m n : ℤ} (h : m ≤ n) : scaleGapPos m n = ↑n - ↑m

On the branch n >= m the positive part is the plain gap.

theorem Algsuperdiff.Section3.Provider.BadEvents.scaleGapPos_of_lt {m n : ℤ} (h : n < m) : scaleGapPos m n = 0

On the branch n < m the positive part vanishes.

Positivity of the lower multiscale ellipticity

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInvLiteral_pos {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : 0 < cubeLowerEllipticityInvLiteral M Q cutoffScale s q omega

The literal inverse lower multiscale ellipticity of the cutoff field is strictly positive: Ch02.lambdaSq is positive for every coefficient family, and the cutoff field is always in the elliptic branch of Ch04.lambdaSqCoeffField.

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv_pos_ae {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), 0 < cubeLowerEllipticityInv M Q cutoffScale s hs q omega

The measurable representative of lambda^{-1}_{s,q}(Q; a_r) is almost surely positive.

The lower multiscale ellipticity observable

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticity {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

Measurable representative of lambda_{s,q}(Q; a_r) for the actual cutoff on an arbitrary triadic cube: the pointwise inverse of the proved representative of lambda^{-1}_{s,q}(Q; a_r).

Equations

• Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticity M Q cutoffScale s hs q omega = (Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv M Q cutoffScale s hs q omega)⁻¹

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeLowerEllipticity {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeLowerEllipticity M Q cutoffScale s hs q)

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticity_nonneg {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : 0 ≤ cubeLowerEllipticity M Q cutoffScale s hs q omega

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInvLiteral_inv_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.Ch04.lambdaSqCoeffField Q s (↑q) (Cutoff.coefficientCutoff M.nu cutoffScale omega)

The inverse of the literal inverse lower ellipticity is the literal lower ellipticity lambda_{s,q}(Q; a_r) of the actual cutoff.

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticity_ae_eq_literal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cubeLowerEllipticity M Q cutoffScale s hs q =ᵐ[↑(Cutoff.cutoffSampleLaw M)] fun (omega : Cutoff.CutoffSample d) => (cubeLowerEllipticityInvLiteral M Q cutoffScale s q omega)⁻¹

The representative of lambda_{s,q}(Q; a_r) agrees almost everywhere with the inverse of the literal observable, hence — by cubeLowerEllipticityInvLiteral_inv_eq — with lambda_{s,q}(Q; a_r).

The middle threshold of e.good.local.events

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.goodLocalThreshold {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (m n : ℤ) : ℝ

The middle term of the chain e.good.local.events: (1/2) C_{(e.cg.ellip.lower)}^{-1} 3^{-(1/2)(n-m)_+} sigmaBar_{n-1}.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.goodLocalThreshold_pos {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (m n : ℤ) : 0 < goodLocalThreshold M Ccg m n

The coarse-ellipticity clause of e.good.local.events

def Algsuperdiff.Section3.Provider.BadEvents.goodLocalEllipticity {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : Set (Cutoff.CutoffSample d)

The second inequality of e.good.local.events (ABK26), as an event: the middle threshold is below 3^{-(1/4)(n-m)_+} lambda_{1/8,2}(z+square_m; a_n), where m = Q.scale and z is the base point of Q.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_goodLocalEllipticity {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : MeasurableSet (goodLocalEllipticity M Ccg Q n)

def Algsuperdiff.Section3.Provider.BadEvents.coarseEllipticityFailure {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : Set (Cutoff.CutoffSample d)

The manuscript's coarse-ellipticity failure event of the decomposition in the proof of l.bad.event.lemma (ABK26): { lambda^{-1}_{1/8,2}(z+square_m; a_n) sigmaBar_{n-1} > 2. 3^{(1/4)(n-m)_+} C_{(e.cg.ellip.lower)} }.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.notMem_goodLocalEllipticity_iff {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) (n : ℤ) {omega : Cutoff.CutoffSample d} (hpos : 0 < cubeLowerEllipticityInv M Q n (1 / 8) goodLocalEllipticity._proof_1 exponentTwo omega) : omega ∉ goodLocalEllipticity M Ccg Q n ↔ omega ∈ coarseEllipticityFailure M Ccg Q n

The decomposition step of l.bad.event.lemma (ABK26). Wherever the representative of lambda^{-1}_{1/8,2} is positive, failure of the coarse-ellipticity clause of e.good.local.events is exactly the manuscript's event { lambda^{-1}_{1/8,2} sigmaBar_{n-1} > 2 . 3^{(1/4)(n-m)_+} C }.

theorem Algsuperdiff.Section3.Provider.BadEvents.compl_goodLocalEllipticity_ae_eq {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : (goodLocalEllipticity M Ccg Q n)ᶜ =ᵐ[↑(Cutoff.cutoffSampleLaw M)] coarseEllipticityFailure M Ccg Q n

The identification of the previous theorem, almost everywhere: the representative of lambda^{-1}_{1/8,2} is almost surely positive.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_compl_goodLocalEllipticity {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : (↑(Cutoff.cutoffSampleLaw M)).real (goodLocalEllipticity M Ccg Q n)ᶜ = (↑(Cutoff.cutoffSampleLaw M)).real (coarseEllipticityFailure M Ccg Q n)

The first reduction in the proof of l.bad.event.lemma (ABK26): the probability that the coarse-ellipticity clause of e.good.local.events fails is the probability of the manuscript's coarse-ellipticity failure event.