ScoreDomination

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

The deterministic domination of the 𝒢₀ score by the 𝒴 row sum

ABK26, §4.1, l.good.scales.ratio.lambda, score domination:

sup_{k ≤ m} 3^{−¼γ(m−k)} max_{z ∈ 3^{k−2}ℤ^d ∩ (□_m∖□_k)} ( … )_+
   ≤  γ⁴ Σ_{n ≤ m} 3^{−¼γ(m−n)} 𝒴_n .

Everything here is pointwise in ω and unconditional: the whole chain is run in ℝ≥0∞, where the k-series inside 𝒴_n and the n-row sum both always exist.

The normalization γ^{-4} is NOT carried by 𝒴 here; it is a lane prefactor and appears only in the downstream threshold. Consequently the display below has no γ⁴ on the right: the inequality is between the score and the un-normalized row sum.

Main results

• exists_mem_latticeAnnulusSet — the annulus decomposition of the shell □_m ∖ □_k at a fixed lattice spacing (the union bound).
• eventG0_score_le_YcalRowE — the display, pointwise and unconditional.
• one_lt_YcalRowE_of_notMem_eventG0 — its consumption: off 𝒢₀(m) the row sum exceeds 1.

Scope

Provider material: proved local helpers, pointwise in ω.

References

• ABK26, l.good.scales.ratio.lambda.

1. The annulus decomposition of a shell

theorem Algsuperdiff.Section4.Provider.Proportion.exists_mem_latticeAnnulusSet (d : ℕ) {j k m : ℤ} (hkm : k ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeAnnulusSet d j m k) : ∃ n ∈ Finset.Icc (k + 1) m, v ∈ Support.latticeAnnulusSet d j n (n - 1)

The annulus decomposition of a shell at a fixed lattice spacing ("by union bounds"). Every lattice point of □_m ∖ □_k lies in exactly one triadic annulus □_n ∖ □_{n−1} with k + 1 ≤ n ≤ m.

2. Two small ℝ≥0∞ / weight identities

theorem Algsuperdiff.Section4.Provider.Proportion.weightThird_add (sprime : ℝ) (a b : ℕ) : weightThird sprime (a + b) = weightThird sprime a * weightThird sprime b

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_weight_eq_weightThird {d : ℕ} (M : Section3.ABKModel d) {m k : ℤ} (hk : k ≤ m) : Real.rpow 3 (-(1 / 4) * M.gamma * ↑(m - k)) = weightThird (M.gamma / 4) (m - k).toNat

The 𝒢₀ weight is the geometric weight at rate s' = γ/4.

3. The row sum

noncomputable def Algsuperdiff.Section4.Provider.Proportion.YcalRowE {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

Total: no summability side condition.

Equations

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

4. The domination

theorem Algsuperdiff.Section4.Provider.Proportion.iSup_shell_le_sum_annMax {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {m k : ℤ} (hk : k ≤ m - 1) (omega : Section3.Cutoff.CutoffSample d) : ⨆ (v : ↑(Support.latticeAnnulusSet d (k - 2) m k)), ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M (k - 3)) * Support.lambdaAnnulusAtom M k (Support.triadicLatticePoint (k - 2) ↑v) omega - Ccg) ≤ ∑ n ∈ Finset.Icc (k + 1) m, ENNReal.ofReal (annMax M Ccg n k omega)

The inner union bound: the lattice maximum over the shell □_m ∖ □_k is at most the sum of the annulus maxima.

theorem Algsuperdiff.Section4.Provider.Proportion.eventG0_score_le_YcalRowE {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ⨆ (k : { k : ℤ // k ≤ m - 1 }), ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * M.gamma * ↑(m - ↑k))) * ⨆ (v : ↑(Support.latticeAnnulusSet d (↑k - 2) m ↑k)), ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M (↑k - 3)) * Support.lambdaAnnulusAtom M (↑k) (Support.triadicLatticePoint (↑k - 2) ↑v) omega - Ccg) ≤ YcalRowE M Ccg (M.gamma / 4) m omega

The score-domination display, pointwise and unconditional.

The supremum defining 𝒢₀(m) is at most the 𝒴 row sum at rate s' = γ/4. The manuscript's γ⁴ is absent because 𝒴 is not normalized here; the two statements differ by that lane prefactor alone.

theorem Algsuperdiff.Section4.Provider.Proportion.one_lt_YcalRowE_of_notMem_eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∉ Support.eventG0 M Ccg m) : 1 < YcalRowE M Ccg (M.gamma / 4) m omega

The consumption of the display. Off 𝒢₀(m) the 𝒴 row sum exceeds the threshold 1 of the good event. This is the deterministic half of the Appendix-D reduction.