OAI/Probability/GammaPassage/SpatialWitnessProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.gamma_spatial_witness_BK line 14

   Source documentation

   Actual spatial path witnesses obey BK for every finite list of indices, including repeated indices and overlapping boxes.

   theorem gamma_spatial_witness_BK (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b m₀ am ap K η p₀ : ℝ) (hp₀ : 0 ≤ p₀) (k m : ℕ)
       (hrare : ∀ ih : ℤ×ℤ, P.real {ω | (fun e => τ e ω) ∈ spatialRareEvent b m₀ am ap K η k m ih} ≤ p₀)
       (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 := by
   …

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

2. theorem OAI.GammaFPP.CrossingBridge.gamma_spatial_witness_BK_scales line 47

   Source documentation

   The finite-list bound with the rare-event probabilities supplied by the actual model, at one common scale for every list of spatial indices.

   theorem gamma_spatial_witness_BK_scales (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b q₀ η : ℝ) (hb : |b| ≤ 1) (hq : 0 < q₀) (hq1 : q₀ < 1) (hη : 0 < η)
       (N : ℕ) (S D : ℝ) :
       ∃ k : ℕ, N < k ∧ S ≤ (2 : ℝ)^k ∧
         D*(2 : ℝ)^k ≤ (characteristicLength P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ k : ℝ) ∧
         ∀ is : List (ℤ×ℤ), P.real {ω | StrictDisjointPaths
           (spatialListSupport b k (characteristicExponent P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ k) is)
           (is.map (spatialWitnessFamily b ((gammaMeanNorm henv hshape hrate) (direction b))
             (extremeSlope (gammaMeanNorm henv hshape hrate) b false) (extremeSlope (gammaMeanNorm henv hshape hrate) b true)
             (sourceCrossingK shape rate (gammaMeanNorm henv hshape hrate) b) η k
             (characteristicExponent P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ k))) (fun e => τ e ω)} ≤
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.spatialListSupport, OAI.GammaFPP.CrossingBridge.characteristicExponent, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily, OAI.GammaFPP.CrossingBridge.sourceCrossingK