G2Score

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

The 𝒢₂ score layer: the squared annular maximum, the atom X_j, and the

exact interchange identity

ABK26, §4.1, the proof of l.ratio.of.good.scales.for.mathcal.E, Steps 1, 2 and 4.

The 𝒢₂ lane is structurally the cleanest of the three: where the 𝒢₀ reduction is a chain of inequalities, the 𝒢₂ reduction is an equality:

s Σ_{j ≤ m} Σ_{n ≤ j−1} 3^{−¼s(m−n)} max_{z ∈ 3ⁿℤ^d ∩ (□_j∖□_{j−1})} 𝓔_{s,2,2}(z+□_n;·)²
  = K₂^{−1} s ε² Y_m ,        Y_m = Σ_{j ≤ m} 3^{−¼s(m−j)} X_j ,

whose entire content is the exponent split 3^{−¼s(m−n)} = 3^{−¼s(m−j)}·3^{−¼s(j−n)} (annularWeight_split). Everything below is proved as an identity of ℝ≥0∞, so no convergence, no a.s. qualifier and no null set enters: the convergence caveat that the printed Y_m identity leaves implicit is therefore never needed.

Main definitions

• annularWeight — the ℝ≥0∞ weight 3^{−¼sk} of the 𝒢₂ displays.
• errorAtomSq — the per-cube atom 𝓔_{s,2,2}(z+□_n; 𝐚_{n−2}, σ_{n−2})², rendered by translating the sample, at the public measurable (2,2) observable of Support.ErrorRepresentative22.
• errorAnnMax — the 0-floored lattice maximum of Step 1's left side, over the Finset enumeration of 3^nℤ^d ∩ (□_j∖□_{j−1}).
• errorAnnSup — the same maximum in the ℝ≥0∞ supremum shape the frozen Support.eventG2 uses; errorAnnSup_eq_ofReal_errorAnnMax identifies the two.
• XcalE — the atom X_j, without the manuscript's lane prefactor K₂ε^{−2}: the normalizer is a free parameter of the downstream threshold, not a rescaling of the score field.
• XrowE — the one-sided row sum Σ_{j ≤ m} 3^{−¼s(m−j)} X_j.

Main results

• annularWeight_split — the exponent split; the whole content of the identity.
• inner_eq_annularWeight_mul_XcalE — the identity, an equality of ℝ≥0∞.
• eventG2_eq_row — the frozen 𝒢₂ event is {s·XrowE ≤ ε²}, exactly.

Deviations from the printed text

• The summand reads the field at the inner scale n (𝓔_{s,2,2}(z+□_n; 𝐚_{n−2}, σ_{n−2})), a per-inner-scale truncation. This is the proved Support.annularErrorObservable at index n, so the convention is the manuscript's.
• K₂ε^{−2} is a lane prefactor, kept explicit.
• The row XrowE is the manuscript's one-sided row; the reconciliation with Appendix D's two-sided row is downstream and is an inequality in the manuscript's favour (the j > m rows are nonnegative).
• The 𝒢₂ observable is the measurable representative, choice-dependent on a null set; the manuscript's literal event is recovered a.e. through Support.annularErrorAtom_ae_eq_annularErrorObservable. Nothing in this file depends on the choice: every statement is an identity between two expressions in the same observable.

Scope

Provider material: proved local helpers.

References

• ABK26, l.ratio.of.good.scales.for.mathcal.E; d.good.event.for.lambda.

1. The geometric weight of the 𝒢₂ lane

noncomputable def Algsuperdiff.Section4.Provider.Proportion.annularWeight (s : ℝ) (k : ℤ) : ENNReal

The 𝒢₂ weight 3^{−¼sk}, in ℝ≥0∞. Written exactly as the frozen Support.eventG2 writes it, so the identifications below are definitional on the weight.

Equations

• Algsuperdiff.Section4.Provider.Proportion.annularWeight s k = ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * s * ↑k))

theorem Algsuperdiff.Section4.Provider.Proportion.annularWeight_split (s : ℝ) (m j n : ℤ) : annularWeight s (m - n) = annularWeight s (m - j) * annularWeight s (j - n)

The exponent split. 3^{−¼s(m−n)} = 3^{−¼s(m−j)}·3^{−¼s(j−n)}: the single computation behind's "by interchanging summation".

theorem Algsuperdiff.Section4.Provider.Proportion.annularWeight_eq_weightThird {s : ℝ} {k : ℤ} (hk : 0 ≤ k) : annularWeight s k = ENNReal.ofReal (weightThird (s / 4) k.toNat)

The weight at a nonnegative offset is the 𝒢₀ lane's weightThird at rate ¼s; this is what lets the ℕ-indexed series apparatus of SeriesTail be reused verbatim.

2. The squared per-cube atom and its lattice maximum

noncomputable def Algsuperdiff.Section4.Provider.Proportion.errorAtomSq {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The 𝒢₂ per-cube atom 𝓔_{s,2,2}(z+□_n; 𝐚_{n−2}, σ_{n−2})², rendered by translating the sample, at the measurable (2,2) observable.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.errorAtomSq_nonneg {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ errorAtomSq M n s z omega

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_errorAtomSq {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (z : HCPolySupport.Vec d) : Measurable (errorAtomSq M n s z)

noncomputable def Algsuperdiff.Section4.Provider.Proportion.errorAnnMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The left side of Step 1: max_{z ∈ 3^nℤ^d ∩ (□_j∖□_{j−1})} 𝓔_{s,2,2}(z+□_n; 𝐚_{n−2}, σ_{n−2})², 0-floored so that it is total (the annulus enumeration may be empty).

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.errorAnnMax_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ errorAnnMax M s j n omega

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_errorAnnMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j n : ℤ) : Measurable (errorAnnMax M s j n)

noncomputable def Algsuperdiff.Section4.Provider.Proportion.errorAnnSup {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The same maximum in the ℝ≥0∞ supremum shape of the frozen event.

Equations

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

The Finset maximum and the set supremum agree

theorem Algsuperdiff.Section4.Provider.Proportion.exists_mem_eq_fmax {iota : Type u_1} {S : Finset iota} {f : iota → ℝ} (hS : S.Nonempty) (hf : ∀ i ∈ S, 0 ≤ f i) : ∃ i ∈ S, fmax S f = f i

A nonempty Finset attains its 0-floored maximum at a member, provided the values there are nonnegative.

theorem Algsuperdiff.Section4.Provider.Proportion.errorAnnSup_eq_ofReal_errorAnnMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {j n : ℤ} (hn : n ≤ j) (omega : Section3.Cutoff.CutoffSample d) : errorAnnSup M s j n omega = ENNReal.ofReal (errorAnnMax M s j n omega)

The two renderings of the lattice maximum coincide. The Finset enumeration latticeAnnulusFinset and the proved set latticeAnnulusSet have the same members at n ≤ j, and all entries are squares, hence nonnegative, so the 0-floor is not felt.

3. The atom X_j and the row sum

noncomputable def Algsuperdiff.Section4.Provider.Proportion.XcalE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The atom X_j, formed in ℝ≥0∞ and WITHOUT the manuscript's lane prefactor K₂ε^{−2}: Σ_{n ≤ j−1} 3^{−¼s(j−n)} max_{z ∈ 3^nℤ^d ∩ (□_j∖□_{j−1})} 𝓔_{s,2,2}(z+□_n;·)².

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Proportion.XrowE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The one-sided row sum Y_m, before the K₂ε^{−2} normalization.

Equations

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

The ℕ-enumeration of the inner scales

def Algsuperdiff.Section4.Provider.Proportion.innerScaleEquiv (j : ℤ) : ℕ ≃ { n : ℤ // n ≤ j - 1 }

The inner scales n ≤ j − 1 enumerated by the offset j − n − 1 ∈ ℕ.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.XcalE_eq_wsumE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : ℤ) (omega : Section3.Cutoff.CutoffSample d) : XcalE M s j omega = wsumE (fun (i : ℕ) => errorAnnMax M s j (j - 1 - ↑i)) (fun (i : ℕ) => weightThird (↑s / 4) (i + 1)) omega

The atom is the SeriesTail weighted series at the 𝒢₀ lane's weight weightThird (¼s) shifted by one (the inner offset j − n starts at 1). This is the bridge that lets the countable generalized triangle inequality isBigOWith_wsum and the moment engine be reused verbatim on the 𝒢₂ lane.

4. The identity

theorem Algsuperdiff.Section4.Provider.Proportion.inner_eq_annularWeight_mul_XcalE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (m j : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ∑' (n : { n : ℤ // n ≤ j - 1 }), annularWeight (↑s) (m - ↑n) * errorAnnSup M s j (↑n) omega = annularWeight (↑s) (m - j) * XcalE M s j omega

The identity. For every row index m and every annulus index j, the inner block of the 𝒢₂ display is exactly the discounted atom. This is an equality of ℝ≥0∞: nothing is dropped, no convergence is used, and the entire content is annularWeight_split.

5. The frozen event, in row-sum form

theorem Algsuperdiff.Section4.Provider.Proportion.eventG2_eq_row {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) : Support.eventG2 M m s ep = {omega : Section3.Cutoff.CutoffSample d | ENNReal.ofReal ↑s * XrowE M s m omega ≤ ENNReal.ofReal (ep ^ 2)}

The frozen 𝒢₂ event IS {s·XrowE ≤ ε²}. A set equality, obtained by applying the identity inside the outer sum.

theorem Algsuperdiff.Section4.Provider.Proportion.notMem_eventG2_iff {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (ep : ℝ) (omega : Section3.Cutoff.CutoffSample d) : omega ∉ Support.eventG2 M m s ep ↔ ENNReal.ofReal (ep ^ 2) < ENNReal.ofReal ↑s * XrowE M s m omega

The complement of the frozen 𝒢₂ event, in row form.