ZScores

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

The two window scores of p.minimal.scale.separation.sec4, and their bad windows

ABK26, §4.2, the definitions of Z₁ and Z₂. The proposition's two conclusions are δ-thresholded inequalities for two ℝ≥0∞-valued scores attached to the window [n, m] of triadic scales:

• the Cesàro-𝓔 score — the centre-uniform Cesàro average of the flux-corrected error observable, gated by the good event; and
• the bad-density score — the centre-uniform Cesàro average of the complement indicator of the good event.

Both are copied here verbatim from the frozen statement's own display, so that a consumer discharging the frozen clause never has to move a single subterm. In particular the tolerance is spelled s * Real.sqrt delta, the normalisation is (((m - n).toNat : ℝ≥0∞) + 1)⁻¹, the centre set is Support.latticeCubeSet d (n - 1) m and the centre is Support.triadicLatticePoint (n - 1) z.

The scores are used directly as ℝ≥0∞-valued predicates: a window of length j is bad when.ofReal deltais strictly below the score of the window[m - j, m]. No real cast, no finiteness and no convergence side condition enters (survey item does not bite: Algsuperdiff.Probability's minimalScale is generic over the bad-window family).

Contents

• centerCesaroScore, centerDensityScore — the two per-centre window averages, and cesaroScore / densityScore, their suprema over the centre set, at the frozen display's exact shape (cesaroScore_eq_iSup, densityScore_eq_iSup are rfl).
• badCesaro, badDensity — the two bad-window families, indexed by the window length j : ℕ at base scale m, i.e. at the window [m - j, m].
• measurable_cesaroScore, measurable_densityScore, measurableSet_badCesaro, measurableSet_badDensity — the measurability layer feeding Algsuperdiff.Probability.measurable_minimalScaleEN.
• cesaroScore_le_of_minimalScaleEN_le, densityScore_le_of_minimalScaleEN_le — the two deterministic extractions, at the frozen conclusion's own n : ℤ indexing, holding for every omega (strictly stronger than the frozen statement's ∀ᵐ).

References

• ABK26, p.minimal.scale.separation.sec4.

1. The per-centre window averages

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.centerCesaroScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (y : HCPolySupport.Vec d) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The Cesàro-𝓔 window average at the centre y — the inner term of minimal_scale_separation's first conclusion, before the maximum over centres.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.centerDensityScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (y : HCPolySupport.Vec d) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The bad-density window average at the centre y — the inner term of minimal_scale_separation's second conclusion.

Equations

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

2. The centre-uniform scores, at the frozen display's shape

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.cesaroScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The Cesàro-𝓔 score of the window [n, m] — the left-hand side of e.scale.sep.for.mathcal.E as frozen.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.densityScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The bad-density score of the window [n, m] — the left-hand side of e.scale.sep.for.good.events as frozen.

Equations

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

theorem Algsuperdiff.Section4.Provider.MinimalScale.cesaroScore_eq_iSup {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : cesaroScore M s delta hs n m omega = ⨆ (z : ↑(Support.latticeCubeSet d (n - 1) m)), centerCesaroScore M s delta hs (Support.triadicLatticePoint (n - 1) ↑z) n m omega

The centre-uniform Cesàro score is the supremum of the per-centre averages over the frozen centre set.

theorem Algsuperdiff.Section4.Provider.MinimalScale.densityScore_eq_iSup {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : densityScore M s delta hs n m omega = ⨆ (z : ↑(Support.latticeCubeSet d (n - 1) m)), centerDensityScore M s delta hs (Support.triadicLatticePoint (n - 1) ↑z) n m omega

The centre-uniform density score is the supremum of the per-centre averages over the frozen centre set.

3. The bad-window families

def Algsuperdiff.Section4.Provider.MinimalScale.badCesaro {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The bad windows of the Cesàro-𝓔 score, indexed by the window length j : ℕ at base scale m: the window [m - j, m] is bad when its score exceeds δ.

Equations

• Algsuperdiff.Section4.Provider.MinimalScale.badCesaro M s delta hs m j omega = (ENNReal.ofReal delta < Algsuperdiff.Section4.Provider.MinimalScale.cesaroScore M s delta hs (m - ↑j) m omega)

def Algsuperdiff.Section4.Provider.MinimalScale.badDensity {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The bad windows of the bad-density score.

Equations

• Algsuperdiff.Section4.Provider.MinimalScale.badDensity M s delta hs m j omega = (ENNReal.ofReal delta < Algsuperdiff.Section4.Provider.MinimalScale.densityScore M s delta hs (m - ↑j) m omega)

4. The window-index bridge

theorem Algsuperdiff.Section4.Provider.MinimalScale.sub_toNat_sub_cancel {n m : ℤ} (hnm : n ≤ m) : m - ↑(m - n).toNat = n

For n ≤ m the window length (m - n).toNat recovers the lower endpoint: m - ((m - n).toNat : ℤ) = n.

theorem Algsuperdiff.Section4.Provider.MinimalScale.toNat_sub_sub (m : ℤ) (j : ℕ) : (m - (m - ↑j)).toNat = j

The window length of [m - j, m] is j.

5. Measurability

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurable_centerCesaroScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (y : HCPolySupport.Vec d) (n m : ℤ) : Measurable (centerCesaroScore M s delta hs y n m)

Each summand of the Cesàro-𝓔 window average is measurable.

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurable_centerDensityScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (y : HCPolySupport.Vec d) (n m : ℤ) : Measurable (centerDensityScore M s delta hs y n m)

The bad-density window average is measurable.

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurable_cesaroScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) : Measurable (cesaroScore M s delta hs n m)

The Cesàro-𝓔 score is measurable. The centre set is a subtype of the countable type Fin d → ℤ, so the supremum is a countable one.

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurable_densityScore {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) : Measurable (densityScore M s delta hs n m)

The bad-density score is measurable.

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurableSet_badCesaro {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) : MeasurableSet {omega : Section3.Cutoff.CutoffSample d | badCesaro M s delta hs m j omega}

Every Cesàro bad-window event is measurable — the input of Algsuperdiff.Probability.measurable_minimalScaleEN.

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurableSet_badDensity {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) : MeasurableSet {omega : Section3.Cutoff.CutoffSample d | badDensity M s delta hs m j omega}

Every density bad-window event is measurable.

6. The deterministic extractions

theorem Algsuperdiff.Section4.Provider.MinimalScale.cesaroScore_le_of_minimalScaleEN_le {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) {n m : ℤ} (hnm : n ≤ m) {omega : Section3.Cutoff.CutoffSample d} (h : Probability.minimalScaleEN (badCesaro M s delta hs m) omega ≤ ↑(m - n).toNat) : cesaroScore M s delta hs n m omega ≤ ENNReal.ofReal delta

The Cesàro-𝓔 clause, pointwise. If the Cesàro random scale is at most the window length (m - n).toNat, then the window [n, m] clears δ. This holds for every omega, with no almost-sure qualifier and no finiteness hypothesis: it is Probability.minimalScaleEN_not_bad_of_le, vacuous exactly on the ⊤-event.

theorem Algsuperdiff.Section4.Provider.MinimalScale.densityScore_le_of_minimalScaleEN_le {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) {n m : ℤ} (hnm : n ≤ m) {omega : Section3.Cutoff.CutoffSample d} (h : Probability.minimalScaleEN (badDensity M s delta hs m) omega ≤ ↑(m - n).toNat) : densityScore M s delta hs n m omega ≤ ENNReal.ofReal delta

The bad-density clause, pointwise — the deterministic half of Z₂.

7. The centre-wise cover of a bad window

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_center_of_badCesaro {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) {omega : Section3.Cutoff.CutoffSample d} (h : badCesaro M s delta hs m j omega) : ∃ z ∈ Support.latticeCubeSet d (m - ↑j - 1) m, ENNReal.ofReal delta < centerCesaroScore M s delta hs (Support.triadicLatticePoint (m - ↑j - 1) z) (m - ↑j) m omega

hcover, as a theorem. A bad Cesàro window is witnessed by some centre of the frozen centre set — the converse direction of the maximum, which is lt_iSup_iff in the complete linear order ℝ≥0∞ and needs no finiteness, no positivity of δ and no measurability.

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_center_of_badDensity {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) {omega : Section3.Cutoff.CutoffSample d} (h : badDensity M s delta hs m j omega) : ∃ z ∈ Support.latticeCubeSet d (m - ↑j - 1) m, ENNReal.ofReal delta < centerDensityScore M s delta hs (Support.triadicLatticePoint (m - ↑j - 1) z) (m - ↑j) m omega

hcover, as a theorem — the density leg.