SpatialEntropyProbability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.spatial_bad_path_probability line 14

Source documentation

Source wi:entropy-bound for actual bad paths, using the proved geometric cover and a same-scale actual spatial BK bound.

theorem spatial_bad_path_probability (henv : GammaEnvironment shape rate P τ)
    (_hshape : 0 < shape) (_hrate : 0 < rate)
    (b m₀ am ap K η p₀ : ℝ) (hb : |b| ≤ 1) (ha : am ≤ ap) (hη : 0 < η) (hp₀ : 0 ≤ p₀)
    (hgap : 4*η ≤ (ap-am)/2) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
    (hstep : max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*(2 : ℝ)^k)
    (hscale₁ : η*(2 : ℝ)^k < 2*m₀*(2 : ℝ)^m-|((am+ap)/2)| *((2 : ℝ)^k+1))
    (hscale₂ : 3*η*(2 : ℝ)^k+2*|((am+ap)/2)| *((2 : ℝ)^k+1) < K*(2 : ℝ)^k)
    (hBK : ∀ is : List (ℤ×ℤ), P.real {ω | StrictDisjointPaths (spatialListSupport b k m is)
      (is.map (spatialWitnessFamily b m₀ am ap K η k m)) (fun e => τ e ω)} ≤ p₀^is.length)
    (N : ℕ) (hN : 4 ≤ N) :
    P.real {ω | SpatialBadPath (fun e => τ e ω) b m₀ ((am+ap)/2) η k m N} ≤
      (196 : ℝ)^N*p₀^(N/16) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.spatialListSupport, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily, OAI.GammaFPP.CrossingBridge.SpatialBadPath