Nonlocal

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

The far-field leg of l.localize.lambdas.for.regularity

ABK26, §4.1. This module renders the proof abbreviation 𝒳_k(z) and the display e.localize.lambdas.for.regularity.nonlocal

max_{z ∈ 3^{n−2}ℤ^d ∩ (□_m ∖ □_n)} 𝒳_{n−2}(z) · 𝟙_{𝒢₀(m)} ≤ 3^{γ(m−n)/4}

over the proved Section 4 support carriers (Section4/Support/Events.lean). The display is, as the source says, nothing but the defining inequality of 𝒢₀(m) read at the single index k = n and rearranged, and that is exactly what the proofs below do: a le_iSup at k = n, a le_iSup at the lattice point, and one division by the positive weight 3^{−γ(m−n)/4}.

The index conversion (versus)

𝒢₀'s own bracket is σ_{k−3} λ_{γ,2}^{-1}(z+□_{k−2}; a_{k−2}), while the proof's abbreviation is 𝒳_k(z) = (σ_{k−1} λ_{γ,2}^{-1}(z+□_k; a_k) − C_cg)_+. It is discharged here, once, by cgExcess_sub_two — an equality of the two readings at the same proved observable Support.lambdaAnnulusAtom.

Range of n

The source states the display for the n of the enclosing supremum, i.e. for every n ≤ m, while 𝒢₀'s own supremum ranges over k ≤ m−1. Both cases are covered below: at n ≤ m−1 the bound is the rearranged 𝒢₀ inequality, and at n = m the index set 3^{m−2}ℤ^d ∩ (□_m ∖ □_m) is empty, so the left side is 0. No hypothesis beyond n ≤ m is used.

References

• ABK26, l.localize.lambdas.for.regularity; the abbreviation 𝒳_k; the display.
• d.good.event.for.lambda, (𝒢₀).

1. The proof's abbreviation 𝒳_k(z)

noncomputable def Algsuperdiff.Section4.Provider.Localize.cgExcess {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (k : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The coarse-grained ellipticity excess 𝒳_k(z):

𝒳_k(z) := ( σ_{k−1} λ_{γ,2}^{-1}(z+□_k; a_k) − C_{(e.cg.ellip.lower)} )_+ .

The cube translate is realized, as everywhere in Section 4, by translating the sample rather than the cube, and (·)_+ is max · 0.

Equations

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

theorem Algsuperdiff.Section4.Provider.Localize.cgExcess_nonneg {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (k : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ cgExcess M Ccg k z omega

theorem Algsuperdiff.Section4.Provider.Localize.cgExcess_sub_two {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (k : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : cgExcess M Ccg (k - 2) z omega = max (↑(Section3.Annealed.sigmaBar M (k - 3)) * Support.lambdaAnnulusAtom M k z omega - Ccg) 0

The index conversion 𝒳_{k−2}(z) = the 𝒢₀ bracket at k. The manuscript's two readings of the same quantity (versus) are equal at the proved observable; the source never writes this out.

2. The weight of 𝒢₀ and its reciprocal

3. The rearranged 𝒢₀ inequality

theorem Algsuperdiff.Section4.Provider.Localize.cgExcess_le_of_mem_eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {m n : ℤ} (hn : n ≤ m - 1) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG0 M Ccg m) (v : ↑(Support.latticeAnnulusSet d (n - 2) m n)) : cgExcess M Ccg (n - 2) (Support.triadicLatticePoint (n - 2) ↑v) omega ≤ Real.rpow 3 (1 / 4 * M.gamma * ↑(m - n))

e.localize.lambdas.for.regularity.nonlocal, per lattice point.

On 𝒢₀(m), every centre z = 3^{n−2}v of the annulus □_m ∖ □_n satisfies 𝒳_{n−2}(z) ≤ 3^{γ(m−n)/4}. No constant: the right side is the bare power.

4. The display, at the lattice supremum and with the indicator