PercolationScaleTail

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

The union bound over scales for the percolation scale

The percolation estimate of Section 5.2 produces, at every scale k, a bound P[light crossing at scale k] ≤ exp(-A 3^k) with a rate A independent of k. This file turns a family of such bounds into the two statements the chains-of-good-cubes proposition needs:

• the light crossings stop occurring almost surely, so the percolation scale percolationScaleTotal is almost surely given by its defining property; and
• the tail P[Y ≥ N] ≤ exp(-(A/6) 3^N) for every N ≥ 1.

Both come from the same elementary observation: because 3^i ≥ 1 + 2i, the sequence exp(-u 3^i) is dominated by the geometric sequence exp(-u) exp(-2u)^i, whose sum is at most 2 exp(-u) as soon as exp(-2u) ≤ 1/2. Summing from the scale N - 1 — the first scale at which the defining property of the percolation scale can fail when Y ≥ N — gives 2 exp(-A 3^{N-1}), and the second factor of 2 is absorbed into the exponent by lowering the rate from A/3 to A/6. The clause is stated for N ≥ 1: at N = 0 the left-hand side is 1 and no positive rate can bound it.

Main results

• tsum_exp_mul_three_pow_le — the geometric domination of exp(-u 3^i).
• measure_iUnion_shift_le — the union bound from the scale j upwards.
• ae_mem_eventuallyHeavyPaths — the light crossings stop almost surely.
• measure_le_percolationScaleTotal_le — the tail of the percolation scale.

References

• ABK26, the chains of good cubes of Section 5.2.

1. Geometric domination of a doubly exponential sequence

theorem Algsuperdiff.Section5.Provider.one_add_two_mul_le_three_pow (i : ℕ) : 1 + 2 * ↑i ≤ 3 ^ i

The elementary inequality 1 + 2 i ≤ 3 ^ i, which is what makes the sequence exp(-u 3^i) geometrically dominated.

theorem Algsuperdiff.Section5.Provider.exp_mul_three_pow_le {u : ℝ} (hu : 0 < u) (i : ℕ) : Real.exp (-(u * 3 ^ i)) ≤ Real.exp (-u) * Real.exp (-(2 * u)) ^ i

The doubly exponential sequence is dominated by a geometric one of ratio exp(-2u).

theorem Algsuperdiff.Section5.Provider.exp_two_mul_le_half {u : ℝ} (hu : Real.log 2 ≤ 2 * u) : Real.exp (-(2 * u)) ≤ 1 / 2

The ratio of the dominating geometric sequence is at most 1/2 once log 2 ≤ 2 u.

theorem Algsuperdiff.Section5.Provider.summable_exp_mul_three_pow {u : ℝ} (hu : 0 < u) : Summable fun (i : ℕ) => Real.exp (-(u * 3 ^ i))

theorem Algsuperdiff.Section5.Provider.tsum_exp_mul_three_pow_le {u : ℝ} (hu : Real.log 2 ≤ 2 * u) (hupos : 0 < u) : ∑' (i : ℕ), Real.exp (-(u * 3 ^ i)) ≤ 2 * Real.exp (-u)

The geometric domination: the whole sum from the base scale is at most twice its first term.

theorem Algsuperdiff.Section5.Provider.two_mul_exp_le_exp_div {A : ℝ} (hA : 2 * Real.log 2 ≤ A) (j : ℕ) : 2 * Real.exp (-(A * 3 ^ j)) ≤ Real.exp (-(A / 6 * 3 ^ (j + 1)))

Absorbing the factor 2 of the geometric sum into the exponent: the rate drops from A/3 at the scale j to A/6 at the scale j + 1.

2. The union bound over scales, for an abstract family

theorem Algsuperdiff.Section5.Provider.measure_iUnion_shift_le {Omega : Type u_1} [MeasurableSpace Omega] (P : MeasureTheory.Measure Omega) (E : ℕ → Set Omega) {A : ℝ} (hApos : 0 < A) (hA : Real.log 2 ≤ 2 * A) (hE : ∀ (k : ℕ), P (E k) ≤ ENNReal.ofReal (Real.exp (-(A * 3 ^ k)))) (j : ℕ) : P (⋃ (i : ℕ), E (j + i)) ≤ ENNReal.ofReal (2 * Real.exp (-(A * 3 ^ j)))

The union bound from a base scale. A family of events whose probabilities decay like exp(-A 3^k) has union from the scale j upwards of probability at most twice the j-th bound.

theorem Algsuperdiff.Section5.Provider.tsum_measure_ne_top {Omega : Type u_1} [MeasurableSpace Omega] (P : MeasureTheory.Measure Omega) (E : ℕ → Set Omega) {A : ℝ} (hApos : 0 < A) (hE : ∀ (k : ℕ), P (E k) ≤ ENNReal.ofReal (Real.exp (-(A * 3 ^ k)))) : ∑' (k : ℕ), P (E k) ≠ ⊤

theorem Algsuperdiff.Section5.Provider.ae_exists_forall_notMem {Omega : Type u_1} [MeasurableSpace Omega] (P : MeasureTheory.Measure Omega) (E : ℕ → Set Omega) {A : ℝ} (hApos : 0 < A) (hE : ∀ (k : ℕ), P (E k) ≤ ENNReal.ofReal (Real.exp (-(A * 3 ^ k)))) : ∀ᵐ (omega : Omega) ∂P, ∃ (N : ℕ), ∀ (k : ℕ), N ≤ k → omega ∉ E k

Almost surely the events stop occurring. This is the first Borel-Cantelli lemma applied to the summable family.

3. The percolation scale

theorem Algsuperdiff.Section5.Provider.subset_iUnion_lightQPathEvent {d : ℕ} (M : Section3.ABKModel d) (Creg Cinj : ℝ) (m : ℤ) (ep : ℝ) (j : ℕ) : {omega : Section3.Cutoff.CutoffSample d | j + 1 ≤ Support.percolationScaleTotal M Creg Cinj m ep omega} ⊆ ⋃ (i : ℕ), Support.lightQPathEvent M Creg Cinj m ep (j + i)

The level set of the percolation scale is covered from the scale j. If Y ≥ j + 1 then the defining property fails at j, so a light crossing occurs at some scale at least j.

theorem Algsuperdiff.Section5.Provider.ae_mem_eventuallyHeavyPaths {d : ℕ} (M : Section3.ABKModel d) (Creg Cinj : ℝ) (m : ℤ) (ep : ℝ) {P : MeasureTheory.Measure (Section3.Cutoff.CutoffSample d)} {A : ℝ} (hApos : 0 < A) (hE : ∀ (k : ℕ), P (Support.lightQPathEvent M Creg Cinj m ep k) ≤ ENNReal.ofReal (Real.exp (-(A * 3 ^ k)))) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂P, omega ∈ Support.eventuallyHeavyPaths M Creg Cinj m ep

The light crossings stop almost surely, which is the hypothesis of percolationScaleTotal_ae_crossing.

theorem Algsuperdiff.Section5.Provider.measure_le_percolationScaleTotal_le {d : ℕ} (M : Section3.ABKModel d) (Creg Cinj : ℝ) (m : ℤ) (ep : ℝ) {P : MeasureTheory.Measure (Section3.Cutoff.CutoffSample d)} {A : ℝ} (hA : 2 * Real.log 2 ≤ A) (hE : ∀ (k : ℕ), P (Support.lightQPathEvent M Creg Cinj m ep k) ≤ ENNReal.ofReal (Real.exp (-(A * 3 ^ k)))) {N : ℕ} (hN : 1 ≤ N) : P {omega : Section3.Cutoff.CutoffSample d | N ≤ Support.percolationScaleTotal M Creg Cinj m ep omega} ≤ ENNReal.ofReal (Real.exp (-(A / 6 * 3 ^ N)))

The tail of the percolation scale, for every N ≥ 1. The union bound runs from the scale N - 1, and the factor 2 of the geometric sum is absorbed by lowering the rate from A/3 to A/6.