Events

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

The Section 4 good events 𝒢₀, 𝒢₁, 𝒢₂ and their intersection

This module renders d.good.event.for.lambda (ABK26) as Set (Cutoff.CutoffSample d) valued definitions over the proved Section 3 carriers, on top of the public (measurable) observables of ShellNorms, ErrorRepresentative22 and Observable/CutoffMultiscaleEllipticity.

Carrier conventions realized here

• Well-definedness. Every countable interior — the k-supremum of 𝒢₀, the k- and n-sums of 𝒢₁ and 𝒢₂, and every lattice maximum — is taken in ℝ≥0∞, so the events are well defined with no convergence side condition, and the thresholds are compared through ENNReal.ofReal.
• Lattice maxima. The manuscript's max_{z ∈ 3^j ℤ^d ∩ S} is the ℝ≥0∞ supremum over the explicit integer enumeration latticeCubeSet / latticeAnnulusSet of the lattice points lying in S. The index type is a subtype of Fin d → ℤ, hence countable, which is what the measurability lemmas consume; the supremum over the empty index is 0, matching the sign convention of the printed maxima (all their entries are nonnegative).
• Translation. λ_{γ,2}^{-1}(z+□_{k−2}; a_{k−2}) and 𝓔_{s,2,2}(z+□_n; a_{n−2}, σ_{n−2}) are rendered by translating the sample, never the cube: … ∘ Cutoff.translateCutoffSample z.
• The coarse-graining constant. C_{(e.cg.ellip.lower)} is the explicit real parameter Ccg.
• Positive parts. (x)_+ inside 𝒢₀ is realized by ENNReal.ofReal, which is max x 0 transported to [0,∞]; no separate truncation enters.

The cubes □_j are the open triadic cubes openCubeSet (originCube d j). The open/half-open choice is immaterial for every lattice enumeration below: the boundary of □_j sits at |x_i| = 3^j/2, and 3^j/2 is never an integer multiple of the lattice spacing 3^i occurring in the displays, so no lattice point of 3^i ℤ^d lies on ∂□_j.

Main definitions

• eventG0, eventG1, eventG2 —.
• goodEventBase — e.lambda.good.events.

Parameter-binder convention (recorded)

eventG0 M (Ccg : ℝ) (m : ℤ) and eventG1 M (m : ℤ) (s T : ℝ) take plain real parameters. eventG2 and goodEventBase take s : {s : ℝ // 0 < s} because the public 𝒢₂ observable annularErrorObservable does: the (2,2) measurable representative is selected on the source window 0 < s.

References

• ABK26, d.good.event.for.lambda.

The explicit triadic lattice enumerations

noncomputable def Algsuperdiff.Section4.Support.triadicLatticePoint {d : ℕ} (j : ℤ) (v : Fin d → ℤ) : HCPolySupport.Vec d

The point 3^j v of the lattice 3^j ℤ^d.

Equations

• Algsuperdiff.Section4.Support.triadicLatticePoint j v i = 3 ^ j * ↑(v i)

def Algsuperdiff.Section4.Support.latticeCubeSet (d : ℕ) (j outer : ℤ) : Set (Fin d → ℤ)

The integer index set of 3^j ℤ^d ∩ □_outer.

Equations

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

def Algsuperdiff.Section4.Support.latticeAnnulusSet (d : ℕ) (j outer inner : ℤ) : Set (Fin d → ℤ)

The integer index set of 3^j ℤ^d ∩ (□_outer ∖ □_inner).

Equations

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

The 𝒢₀ ingredients

def Algsuperdiff.Section4.Support.coarseEllipticityExponentTwo : Section3.CoarseEllipticityExponent

The coarse-ellipticity exponent q = 2 read by 𝒢₀'s λ_{γ,2}^{-1}.

Equations

• Algsuperdiff.Section4.Support.coarseEllipticityExponentTwo = Algsuperdiff.Section3.CoarseEllipticityExponent.finite ⟨2, Algsuperdiff.Section4.Support.coarseEllipticityExponentTwo._proof_1⟩

noncomputable def Algsuperdiff.Section4.Support.lambdaAnnulusAtom {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (z : HCPolySupport.Vec d) : Section3.Cutoff.CutoffSample d → ℝ

The 𝒢₀ atom λ_{γ,2}^{-1}(z+□_{k−2}; a_{k−2}), rendered by translating the sample (resolution A4). The λ-literal is genuinely measurable (Section 3's literal-measurability engine), so no representative is selected here.

Equations

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

theorem Algsuperdiff.Section4.Support.measurable_lambdaAnnulusAtom {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (z : HCPolySupport.Vec d) : Measurable (lambdaAnnulusAtom M k z)

noncomputable def Algsuperdiff.Section4.Support.eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) : Set (Section3.Cutoff.CutoffSample d)

The event 𝒢₀(m) of d.good.event.for.lambda:

{ sup_{k ≤ m−1} 3^{−γ(m−k)/4}
    max_{z ∈ 3^{k−2}ℤ^d ∩ (□_m ∖ □_k)}
      ( σ_{k−3} λ_{γ,2}^{-1}(z+□_{k−2}; a_{k−2}) − C_{(e.cg.ellip.lower)} )_+
  ≤ 1 }

Equations

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

theorem Algsuperdiff.Section4.Support.measurableSet_eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) : MeasurableSet (eventG0 M Ccg m)

theorem Algsuperdiff.Section4.Support.eventG0_subset_of_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {Ccg Ccg' : ℝ} (h : Ccg ≤ Ccg') : eventG0 M Ccg m ⊆ eventG0 M Ccg' m

𝒢₀ is monotone in the displayed constant: raising C_{(e.cg.ellip.lower)} lowers every positive part.

noncomputable def Algsuperdiff.Section4.Support.eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s T : ℝ) : Set (Section3.Cutoff.CutoffSample d)

The event 𝒢₁(m; s, T) of d.good.event.for.lambda: the intersection of

{ ∑_{k=m}^∞ 3^{(2−γ)m} ‖∇j_k‖_{W^{1,∞}(□_m)} ≤ T }

and

{ ∑_{n=−∞}^{m} 3^{−s(m−n)/4}
    ∑_{k=n−1}^{m} ( 3^{(2−γ)k} max_{z ∈ 3^kℤ^d ∩ □_m} ‖j_k‖_{W^{2,∞}(z+□_k)} )^2
  ≤ T^2 }

Equations

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

theorem Algsuperdiff.Section4.Support.mem_eventG1_iff {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s T : ℝ) (omega : Section3.Cutoff.CutoffSample d) : omega ∈ eventG1 M m s T ↔ ∑' (k : { k : ℤ // m ≤ k }), ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑m) * shellW1InfGradNorm m (↑omega ↑k)) ≤ ENNReal.ofReal T ∧ ∑' (n : { n : ℤ // n ≤ m }), ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * s * ↑(m - ↑n))) * ∑ k ∈ Finset.Icc (↑n - 1) m, (ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑k)) * ⨆ (v : ↑(latticeCubeSet d k m)), ENNReal.ofReal (shellW2InfNormAt (triadicLatticePoint k ↑v) k (↑omega k))) ^ 2 ≤ ENNReal.ofReal (T ^ 2)

theorem Algsuperdiff.Section4.Support.measurableSet_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s T : ℝ) : MeasurableSet (eventG1 M m s T)

theorem Algsuperdiff.Section4.Support.eventG1_subset_of_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : ℝ) {T T' : ℝ} (hT : 0 ≤ T) (h : T ≤ T') : eventG1 M m s T ⊆ eventG1 M m s T'

𝒢₁ is monotone in its threshold.

noncomputable def Algsuperdiff.Section4.Support.eventG2 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : Set (Section3.Cutoff.CutoffSample d)

The event 𝒢₂(m; s, ε) of d.good.event.for.lambda:

{ s ∑_{j=−∞}^{m} ∑_{n=−∞}^{j−1} 3^{−s(m−n)/4}
    max_{z ∈ 3^nℤ^d ∩ (□_j ∖ □_{j−1})} 𝓔_{s,2,2}(z+□_n; a_{n−2}, σ_{n−2})^2
  ≤ ε^2 }

The square sits inside the lattice maximum, exactly as printed.

Equations

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

theorem Algsuperdiff.Section4.Support.mem_eventG2_iff {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) (omega : Section3.Cutoff.CutoffSample d) : omega ∈ eventG2 M m s ep ↔ ENNReal.ofReal ↑s * ∑' (j : { j : ℤ // j ≤ m }) (n : { n : ℤ // n ≤ ↑j - 1 }), ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * ↑s * ↑(m - ↑n))) * ⨆ (v : ↑(latticeAnnulusSet d (↑n) (↑j) (↑j - 1))), ENNReal.ofReal (annularErrorObservable M (↑n) s (Section3.Cutoff.translateCutoffSample (triadicLatticePoint ↑n ↑v) omega) ^ 2) ≤ ENNReal.ofReal (ep ^ 2)

theorem Algsuperdiff.Section4.Support.measurableSet_eventG2 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : MeasurableSet (eventG2 M m s ep)

theorem Algsuperdiff.Section4.Support.eventG2_subset_of_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) {ep ep' : ℝ} (hep : 0 ≤ ep) (h : ep ≤ ep') : eventG2 M m s ep ⊆ eventG2 M m s ep'

𝒢₂ is monotone in its threshold.

The composed good event

noncomputable def Algsuperdiff.Section4.Support.goodEventBase {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : Set (Section3.Cutoff.CutoffSample d)

The composed good event 𝒢(m; s, ε) of e.lambda.good.events:

𝒢(m; s, ε) = 𝒢₀(m) ∩ 𝒢₁(m; s, s ε c⋆^{1/2} γ^{−1/2}) ∩ 𝒢₂(m; s, ε).

The translate 𝒢(m, y; s, ε) is Cutoff.translateCutoffSample y ⁻¹' goodEventBase M Ccg m s ep (resolution A4); it is not introduced here.

Equations

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

theorem Algsuperdiff.Section4.Support.measurableSet_goodEventBase {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : MeasurableSet (goodEventBase M Ccg m s ep)

theorem Algsuperdiff.Section4.Support.goodEventBase_subset_eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : goodEventBase M Ccg m s ep ⊆ eventG0 M Ccg m

theorem Algsuperdiff.Section4.Support.goodEventBase_subset_eventG1 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : goodEventBase M Ccg m s ep ⊆ eventG1 M m (↑s) (↑s * ep * √(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)

theorem Algsuperdiff.Section4.Support.goodEventBase_subset_eventG2 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : goodEventBase M Ccg m s ep ⊆ eventG2 M m s ep