LocalProbability

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

The local bad-event probability e.Bloc.prob

This module proves the local branch of ABK26's Lemma l.bad.event.probabilities (statement, proof Step 1): for every integer scale j <= m - 1 and every centre z in 3^j Z^d,

P[ B_loc(z + square_j) ] <= exp( - c E^{-2} gamma^{-1} ) ,

with the explicit dimension-free c = 1/512.

The proof

Step 1 of the manuscript reads: by e.bound.Lambdas.by.Es, sigma_j^{-1} Lambda_{1/4,2}(z+square_j; a_j) <= 4 + 4 E^2 and similarly for sigma_j lambda_{1/4,2}^{-1}; hence by Markov and the induction hypothesis e.new.induction.for.shom, the probability is at most exp(-c E^{-2}gamma^{-1}).

Here the two halves are:

• CenteredIdentification.measureReal_badLoc_le_measureReal_centeredTail (the sharp comparison, the deterministic translation covariance of TranslationCovariance.lean, and the translation invariance of the cutoff sample law) reduces to P[ E_{1/4,infinity,2}(square_j; a_j, sigma_j) > 1 ];
• the second clause of the induction state Algsuperdiff.Frozen.Section3.inductionState at s = 1/4 gives the two-term weak-Orlicz bound E_{1/4,infinity,2}(square_j) <= O_{Gamma_2}(4 E gamma^{1/2}) + O_{Gamma_{1/2}}(16 exp(-E^{-3}gamma^{-1})), and the two tails are evaluated at the levels t_1 = (2 A_1)^{-1}, t_2 = (2 A_2)^{-1} splitting the threshold 1 = 1/2 + 1/2.

The first tail contributes exp(-E^{-2}gamma^{-1}/64), the second exp(-(exp(E^{-3}gamma^{-1})/32)^{1/2}), and the second is far smaller than the first in the admissible range.

The admissibility gate

Both weak-Orlicz tails are only available at levels t >= 1, so the amplitudes must be below the threshold: 8 E gamma^{1/2} <= 1. With gamma <= E^{-5} this reads 8 E^{-3/2} <= 1, i.e. E >= 4. Likewise s = 1/4 lies in the induction state's window [8 gamma, 1] only when gamma <= 1/32, which again needs a lower bound on E. The lower bound is therefore carried explicitly here as 4 <= E; it is exactly what E >= C(d) c_star^{-1} yields at C(d):= 4 C_0(d) for any dimension-only c_star <= C_0(d).

Main results

• measureReal_upperTail_le_of_isTwoTermBigOWith: the union bound for a two-term weak-Orlicz relation.
• measureReal_badLoc_le: the displayed bound e.Bloc.prob.

References

• ABK26, l.bad.event.probabilities.
• ABK26, d.mathcalS.def / e.new.induction.for.shom.

The union bound behind a two-term weak-Orlicz tail

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_upperTail_le_of_isTwoTermBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {Psi1 Psi2 : ℝ → ℝ} {X : Omega → ℝ} {A1 A2 theta t1 t2 : ℝ} (h : Probability.IsTwoTermBigOWith mu Psi1 Psi2 X A1 A2) (ht1 : 1 ≤ t1) (ht2 : 1 ≤ t2) (hth : A1 * t1 + A2 * t2 ≤ theta) : mu.real {omega : Omega | theta < X omega} ≤ (Psi1 t1)⁻¹ + (Psi2 t2)⁻¹

Splitting a threshold into the two scaled levels of a two-term weak-Orlicz relation bounds the upper tail by the sum of the two tail values.

The displayed bound e.Bloc.prob

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_badLoc_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {m : ℤ} {E : ℝ} (hE : 1 ≤ E) (hE4 : 4 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hj : Q.scale ≤ m - 1) (hgamma : M.gamma ≤ E ^ (-5)) : (↑(Cutoff.cutoffSampleLaw M)).real (badLoc M Q) ≤ Real.exp (-(1 / 512 * E⁻¹ ^ 2 * M.gamma⁻¹))

ABK26 e.Bloc.prob. Under the induction state S(m-1, E), for every triadic cube Q = z + square_j with j <= m - 1,

P[ B_loc(z + square_j) ] <= exp( - (1/512) E^{-2} gamma^{-1} ) .