ScaleDecomposition

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

The scale decomposition of the bad event and its per-scale concentration

Step 1 of ABK26's l.percolation.bound.general controls the centered density average

⨍_{z ∈ □_m ∩ ℤ^d} (1_{B(z)} - ℙ[B(z)]), where B(z) = ⋃_{L ∈ ℕ} B_L(z),

by decomposing it over the scales L.

A replacement for the printed decomposition

The printed argument sums the raw scale events, invoking 1_{B(z)} ≤ ∑_L 1_{B_L(z)} and ℙ[B(z)] ≤ ∑_L ℙ[B_L(z)]. Those two inequalities point in opposite directions once the centering is subtracted: they give

1_{B(z)} - ℙ[B(z)] ≤ ∑_L (1_{B_L(z)} - ℙ[B_L(z)]) + Δ(z), Δ(z) := ∑_L ℙ[B_L(z)] - ℙ[B(z)] ≥ 0,

and the deterministic overshoot Δ(z), of size up to ∑_L exp(-T² 3^{aL}), is not dominated by the target amplitude C(a^{-1}+(d-a)^{-1}) T^{-1} 3^{-am/2}, which tends to 0 as m → ∞ while Δ does not.

The decomposition used here replaces B_L(z) by the first-occurrence events

badFirst B L z := B_L(z) \ ⋃_{L' < L} B_{L'}(z).

These are pairwise disjoint with union B(z), so both inequalities become equalities and Δ ≡ 0; and since badFirst B L z ⊆ B_L(z) the tail bound ℙ[B_L(z)] ≤ exp(-T² 3^{aL}) is inherited. Crucially the first-occurrence event is still measurable with respect to siteSigma B {z} L, the σ-algebra of the scales ≤ L at the single site z, so ABK26's finite-range hypothesis at range 3 ^ L applies to it verbatim. No hypothesis of the source lemma is used beyond those already present.

Main definitions

• badUnion: ABK26's B(z) of e.badevent.decomp.
• badFirst: the first-occurrence refinement of the scale decomposition.
• centeredScale, centeredUnion: the centered indicators.
• scaleAverage, densityAverage: the cube averages of ABK26 Step 1.
• colorScale: the colouring cost factor produced by isBigO_gammaSigma_average_of_separatedIndep.

Main results

• tsum_scaleAverage: ∑'_L scaleAverage L = densityAverage, the exact scale decomposition.
• densityAverage_le_tsum_abs_scaleAverage: the signed series is dominated by the absolutely convergent series of absolute values, which is the form the countable triangle inequality consumes.
• isBigO_gammaSigma_scaleAverage: the per-scale estimate.

References

• ABK26, Lemma l.percolation.bound.general, Step 1.

The scale decomposition

def Algsuperdiff.Section3.Provider.Percolation.badUnion {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (z : Fin d → ℤ) : Set Ω

ABK26, e.badevent.decomp: B(z) := ⋃_{L ∈ ℕ} B_L(z).

Equations

• Algsuperdiff.Section3.Provider.Percolation.badUnion B z = ⋃ (L : ℕ), B L z

def Algsuperdiff.Section3.Provider.Percolation.badFirst {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (L : ℕ) (z : Fin d → ℤ) : Set Ω

The first-occurrence refinement of the scale decomposition: the event that B_L(z) occurs and no B_{L'}(z) with L' < L does.

Equations

• Algsuperdiff.Section3.Provider.Percolation.badFirst B L z = B L z \ ⋃ L' ∈ Set.Iio L, B L' z

theorem Algsuperdiff.Section3.Provider.Percolation.badFirst_subset {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (L : ℕ) (z : Fin d → ℤ) : badFirst B L z ⊆ B L z

theorem Algsuperdiff.Section3.Provider.Percolation.mem_badFirst_iff {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {L : ℕ} {z : Fin d → ℤ} {ω : Ω} : ω ∈ badFirst B L z ↔ ω ∈ B L z ∧ ∀ L' < L, ω ∉ B L' z

theorem Algsuperdiff.Section3.Provider.Percolation.mem_badUnion_iff {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {z : Fin d → ℤ} {ω : Ω} : ω ∈ badUnion B z ↔ ∃ (L : ℕ), ω ∈ B L z

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_badFirst_siteSigma {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (L : ℕ) (z : Fin d → ℤ) : MeasurableSet (badFirst B L z)

The first-occurrence event at scale L is localised at the single site z and involves only the scales ≤ L.

theorem Algsuperdiff.Section3.Provider.Percolation.pairwise_disjoint_badFirst {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (z : Fin d → ℤ) : Pairwise (Function.onFun Disjoint fun (L : ℕ) => badFirst B L z)

theorem Algsuperdiff.Section3.Provider.Percolation.iUnion_badFirst {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (z : Fin d → ℤ) : ⋃ (L : ℕ), badFirst B L z = badUnion B z

theorem Algsuperdiff.Section3.Provider.Percolation.exists_mem_badFirst {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {z : Fin d → ℤ} {ω : Ω} (h : ω ∈ badUnion B z) : ∃ (L : ℕ), ω ∈ badFirst B L z

theorem Algsuperdiff.Section3.Provider.Percolation.notMem_badFirst_of_notMem_badUnion {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {z : Fin d → ℤ} {ω : Ω} (h : ω ∉ badUnion B z) (L : ℕ) : ω ∉ badFirst B L z

theorem Algsuperdiff.Section3.Provider.Percolation.summable_indicator_badFirst {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (z : Fin d → ℤ) (ω : Ω) : Summable fun (L : ℕ) => (badFirst B L z).indicator (fun (x : Ω) => 1) ω

theorem Algsuperdiff.Section3.Provider.Percolation.tsum_indicator_badFirst {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (z : Fin d → ℤ) (ω : Ω) : ∑' (L : ℕ), (badFirst B L z).indicator (fun (x : Ω) => 1) ω = (badUnion B z).indicator (fun (x : Ω) => 1) ω

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_badFirst {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (L : ℕ) (z : Fin d → ℤ) : MeasurableSet (badFirst B L z)

theorem Algsuperdiff.Section3.Provider.Percolation.summable_measureReal_badFirst {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (z : Fin d → ℤ) : Summable fun (L : ℕ) => μ.real (badFirst B L z)

theorem Algsuperdiff.Section3.Provider.Percolation.tsum_measureReal_badFirst {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (z : Fin d → ℤ) : ∑' (L : ℕ), μ.real (badFirst B L z) = μ.real (badUnion B z)

Centered indicators

noncomputable def Algsuperdiff.Section3.Provider.Percolation.centeredScale {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (B : ℕ → (Fin d → ℤ) → Set Ω) (μ : MeasureTheory.Measure Ω) (L : ℕ) (z : Fin d → ℤ) : Ω → ℝ

The centered indicator of the first-occurrence event at scale L.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Percolation.centeredUnion {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (B : ℕ → (Fin d → ℤ) → Set Ω) (μ : MeasureTheory.Measure Ω) (z : Fin d → ℤ) : Ω → ℝ

The centered indicator of B(z): the summand of ABK26's density average.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.summable_abs_centeredScale {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (z : Fin d → ℤ) (ω : Ω) : Summable fun (L : ℕ) => |centeredScale B μ L z ω|

theorem Algsuperdiff.Section3.Provider.Percolation.summable_centeredScale {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (z : Fin d → ℤ) (ω : Ω) : Summable fun (L : ℕ) => centeredScale B μ L z ω

theorem Algsuperdiff.Section3.Provider.Percolation.tsum_centeredScale {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (z : Fin d → ℤ) (ω : Ω) : ∑' (L : ℕ), centeredScale B μ L z ω = centeredUnion B μ z ω

theorem Algsuperdiff.Section3.Provider.Percolation.measurable_centeredScale {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (L : ℕ) (z : Fin d → ℤ) : Measurable (centeredScale B μ L z)

theorem Algsuperdiff.Section3.Provider.Percolation.measurable_centeredScale_siteSigma {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (B : ℕ → (Fin d → ℤ) → Set Ω) (μ : MeasureTheory.Measure Ω) (L : ℕ) (z : Fin d → ℤ) : Measurable (centeredScale B μ L z)

theorem Algsuperdiff.Section3.Provider.Percolation.integral_centeredScale_eq_zero {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (L : ℕ) (z : Fin d → ℤ) : ∫ (ω : Ω), centeredScale B μ L z ω ∂μ = 0

The cube averages

noncomputable def Algsuperdiff.Section3.Provider.Percolation.scaleAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (B : ℕ → (Fin d → ℤ) → Set Ω) (μ : MeasureTheory.Measure Ω) (L m : ℕ) : Ω → ℝ

The per-scale cube average of ABK26 Step 1.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Percolation.densityAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (B : ℕ → (Fin d → ℤ) → Set Ω) (μ : MeasureTheory.Measure Ω) (m : ℕ) : Ω → ℝ

ABK26's centered density average ⨍_{z ∈ □_m ∩ ℤ^d} (1_{B(z)} - ℙ[B(z)]).

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.summable_abs_scaleAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (m : ℕ) (ω : Ω) : Summable fun (L : ℕ) => |scaleAverage B μ L m ω|

theorem Algsuperdiff.Section3.Provider.Percolation.tsum_scaleAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (m : ℕ) (ω : Ω) : ∑' (L : ℕ), scaleAverage B μ L m ω = densityAverage B μ m ω

The exact scale decomposition. With the first-occurrence events the density average is the sum of the per-scale averages, with no deterministic overshoot.

theorem Algsuperdiff.Section3.Provider.Percolation.densityAverage_le_tsum_abs_scaleAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (m : ℕ) (ω : Ω) : densityAverage B μ m ω ≤ ∑' (L : ℕ), |scaleAverage B μ L m ω|

The signed decomposition is dominated by the absolutely convergent series of absolute values. This is the step that lets the ABK26 countable triangle inequality — which requires nonnegative summands — be applied to a signed scale decomposition.

The per-scale estimate

noncomputable def Algsuperdiff.Section3.Provider.Percolation.colorScale (d m L : ℕ) : ℝ

The colouring cost factor at scale L for the cube □_m, as produced by isBigO_gammaSigma_average_of_separatedIndep.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.isBigO_gammaSigma_scaleAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {m L : ℕ} {A : ℝ} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (hindep : ∀ (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ L < latDist u v) → ProbabilityTheory.Indep (siteSigma B S L) (siteSigma B S' L) μ) (hA : 0 < A) (hA1 : A ≤ 1) (htail : ∀ (z : Fin d → ℤ), μ.real (B L z) ≤ Real.exp (-A ^ (-2))) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (scaleAverage B μ L m) (colorScale d m L * (2 * A))

The per-scale estimate of ABK26 Step 1.

If every bad event at scale L has probability at most exp(-A^{-2}) with 0 < A ≤ 1, then the scale-L cube average is O_{Γ₂} at the colouring scale times 2A. At the ABK26 call site A = T^{-1} 3^{-aL/2}, so that A^{-2} = T² 3^{aL}.