DensityBound

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

Conclusion (1) of ABK26's general percolation lemma: the density bound

This module proves the density bound e.density.bound, conclusion (1) of l.percolation.bound.general (ABK26), from hypotheses (ii) and (iii) of that lemma, following Step 1 of its proof.

The printed statement, and its correction

The printed conclusion reads: there is c(d) > 0 such that for every t > 0, if a < d,

ℙ[ ⨍_{z ∈ □_m ∩ ℤ^d} (1_{B(z)} - ℙ[B(z)]) > t ] ≤ exp(-c t² a² (d-a)² T² 3^{am}).

The range ∀ t > 0 outruns the proof: Step 1 delivers the weak-Orlicz estimate

⨍_{z ∈ □_m ∩ ℤ^d} (1_{B(z)} - ℙ[B(z)]) ≤ 𝒪_{Γ₂}(A), A = C(a^{-1} + (d-a)^{-1}) T^{-1} 3^{-am/2},

which yields ℙ[· > t] ≤ 2 exp(-t²/A²); absorbing the factor 2 into a constant-free exp(-c t²/A²) needs t ≳ A, and for t ≪ A the argument gives only the trivial bound ≤ 1 while the printed right-hand side is < 1. The corrected statement is the weak-Orlicz estimate itself — equivalently, the printed tail bound restricted to t ≥ A. Both forms are proved below: isBigOWith_gammaSigma_densityAverage and measureReal_densityAverage_gt_le_exp.

The proof

ScaleDecomposition.lean supplies the exact first-occurrence scale decomposition and the per-scale estimate; ColoredConcentration.lean supplies the colouring corollary of the concentration inequality. What remains here is arithmetic: the per-scale amplitude

Ā_L = C (T^{-1}) min(2^{d/2} 3^{-dm/2} 3^{(d-a)L/2}, 3^{-aL/2})

dominates the per-scale estimate — the first entry of the min is the genuine concentration gain, available while 3^L is below the diameter of □_m, the second is the trivial triangle-inequality bound — and

∑_{L ∈ ℕ} Ā_L ≤ C(d) (a^{-1} + (d-a)^{-1}) T^{-1} 3^{-am/2},

the two halves of the geometric sum producing the two poles a^{-1} (from L > m, where a > 0 is needed) and (d-a)^{-1} (from L ≤ m, where a < d is needed). Hypothesis (i) of the source lemma, independence across disjoint sets of scales, is not used by Step 1 and is therefore not assumed.

Main results

• Algsuperdiff.Section3.Provider.Percolation.isBigOWith_gammaSigma_densityAverage
• Algsuperdiff.Section3.Provider.Percolation.measureReal_densityAverage_gt_le_exp

References

• ABK26, l.percolation.bound.general (1) e.density.bound.
• ABK26, Step 1 of its proof.

Elementary rpow arithmetic

The per-scale amplitude

noncomputable def Algsuperdiff.Section3.Provider.Percolation.perScaleAmplitude (d : ℕ) (a T : ℝ) (m L : ℕ) : ℝ

The per-scale amplitude of ABK26 Step 1. The first entry of the min is the concentration gain from the colouring, the second the trivial triangle-inequality bound; the min is what keeps the scale sum convergent in both regimes.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.perScaleAmplitude_pos (d : ℕ) {a T : ℝ} (hT : 0 < T) (m L : ℕ) : 0 < perScaleAmplitude d a T m L

theorem Algsuperdiff.Section3.Provider.Percolation.summable_perScaleAmplitude (d : ℕ) {a T : ℝ} (ha : 0 < a) (hT : 0 < T) (m : ℕ) : Summable (perScaleAmplitude d a T m)

The per-scale estimate at the amplitude perScaleAmplitude

theorem Algsuperdiff.Section3.Provider.Percolation.isBigOWith_gammaSigma_abs_scaleAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a T : ℝ} {m L : ℕ} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (htail : ∀ (l : ℕ) (y : Fin d → ℤ), μ.real (B l y) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑l)))) (ha : 0 < a) (hT : 1 ≤ T) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (ω : Ω) => |scaleAverage B μ L m ω|) (perScaleAmplitude d a T m L)

The per-scale estimate of Step 1 at the amplitude perScaleAmplitude.

The scale sum

noncomputable def Algsuperdiff.Section3.Provider.Percolation.densityBoundConst (d : ℕ) : ℝ

The dimensional constant in the corrected amplitude of e.density.bound.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.densityBoundConst_pos (d : ℕ) : 0 < densityBoundConst d

theorem Algsuperdiff.Section3.Provider.Percolation.tsum_perScaleAmplitude_le (d : ℕ) {a T : ℝ} (ha : 0 < a) (had : a < ↑d) (hT : 0 < T) (m : ℕ) : ∑' (L : ℕ), perScaleAmplitude d a T m L ≤ 2 * HCPolySupport.IndependentSums.gammaTriangleConst 2 * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * (2 * 2 ^ (↑d / 2) * (↑d + 2)) * (a⁻¹ + (↑d - a)⁻¹) * T⁻¹ * (3 ^ (-a / 2)) ^ m

The scale sum of ABK26 Step 1. The pole a^{-1} comes from the scales L > m, the pole (d-a)^{-1} from the scales L ≤ m.

The density bound

theorem Algsuperdiff.Section3.Provider.Percolation.isBigOWith_gammaSigma_densityAverage {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a T : ℝ} {m : ℕ} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (htail : ∀ (l : ℕ) (y : Fin d → ℤ), μ.real (B l y) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑l)))) (ha : 0 < a) (had : a < ↑d) (hT : 1 ≤ T) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 2) (densityAverage B μ m) (densityBoundConst d * (a⁻¹ + (↑d - a)⁻¹) * T⁻¹ * (3 ^ (-a / 2)) ^ m)

The tail form on the corrected range is measureReal_densityAverage_gt_le_exp.

The hypotheses are exactly (ii) and (iii) of the source lemma together with its parameter constraints a ∈ (0,d) and T ≥ 1; hypothesis (i) is not needed for Step 1. Measurability of the bad events is the reading of the word "events".

noncomputable def Algsuperdiff.Section3.Provider.Percolation.densityBoundExpConst (d : ℕ) : ℝ

The constant c(d) > 0 in the exponent of the printed tail bound.

Equations

• Algsuperdiff.Section3.Provider.Percolation.densityBoundExpConst d = (Algsuperdiff.Section3.Provider.Percolation.densityBoundConst d ^ 2 * ↑d ^ 2)⁻¹

theorem Algsuperdiff.Section3.Provider.Percolation.densityBoundExpConst_pos {d : ℕ} (hd : 0 < d) : 0 < densityBoundExpConst d

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_densityAverage_gt_le_exp {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a T t : ℝ} {m : ℕ} (hB : ∀ (l : ℕ) (y : Fin d → ℤ), MeasurableSet (B l y)) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (htail : ∀ (l : ℕ) (y : Fin d → ℤ), μ.real (B l y) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑l)))) (ha : 0 < a) (had : a < ↑d) (hT : 1 ≤ T) (ht : densityBoundConst d * (a⁻¹ + (↑d - a)⁻¹) * T⁻¹ * (3 ^ (-a / 2)) ^ m ≤ t) : μ.real {ω : Ω | t < densityAverage B μ m ω} ≤ Real.exp (-(densityBoundExpConst d * t ^ 2 * a ^ 2 * (↑d - a) ^ 2 * T ^ 2 * 3 ^ (a * ↑m)))

On that range it is an exact reformulation of isBigOWith_gammaSigma_densityAverage.