OAI/Probability/GammaPassage/ShortCrossingProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.gamma_origin_local_travel line 13

   Source documentation

   Origin-to-endpoint local travel from the actual simultaneous ball event.

   theorem gamma_origin_local_travel (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate) (D η δ : ℝ)
       (hD : 0 < D) (hη : 0 < η) (hδ : 0 < δ) :
       ∀ κ > 0, ∀ᶠ s : ℝ in atTop, ∀ q : Vertex, ‖latticeEmbed q‖ ≤ D*s →
         P.real {ω | ¬LocalTravel (gammaMeanNorm h hshape hrate) η δ s 0 q (fun e => τ e ω)} < κ := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm

2. theorem OAI.GammaFPP.CrossingBridge.gamma_bounded_crossing_failure line 34

   Source documentation

   Bounded longitudinal scales use an explicit horizontal path.

   theorem gamma_bounded_crossing_failure (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
       (b m K s N : ℝ) (n : ℤ) (hb : |b| ≤ 1) (hm : 0 ≤ m)
       (hn : 0 ≤ n) (hnN : (n : ℝ) ≤ N) (hns : (n : ℝ) ≤ 8*s) :
       P.real {ω | (fun e => τ e ω) ∉ crossingEvent b m K s n 0} ≤
         Real.exp (-(rate/2)*(K*s-coordinateAllowance shape rate*N)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.coordinateAllowance

3. theorem OAI.GammaFPP.CrossingBridge.gamma_short_crossing_failure line 62

   Source documentation

   This is the joint short-crossing limit in gr:characteristic-lengths, expressed as uniform convergence of the failure probabilities.

   theorem gamma_short_crossing_failure (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b K C : ℝ) (hb : |b| ≤ 1) (hK : 0 < K) (hC : 0 < C) :
       ∀ κ > 0, ∀ᶠ s : ℝ in atTop, ∀ n : ℤ, 1 ≤ n → (n : ℝ) ≤ C*s →
         P.real {ω | (fun e => τ e ω) ∉ crossingEvent b ((gammaMeanNorm h hshape hrate) (direction b)) K s n 0} < κ := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.gammaMeanNorm

4. theorem OAI.GammaFPP.CrossingBridge.gamma_short_crossing_probability line 124

   Source documentation

   Equivalent success-probability formulation from eq:gr-short-crossings.

   theorem gamma_short_crossing_probability (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b K C : ℝ) (hb : |b| ≤ 1) (hK : 0 < K) (hC : 0 < C) :
       ∀ q < 1, ∀ᶠ s : ℝ in atTop, ∀ n : ℤ, 1 ≤ n → (n : ℝ) ≤ C*s →
         q < P.real {ω | (fun e => τ e ω) ∈ crossingEvent b ((gammaMeanNorm h hshape hrate) (direction b)) K s n 0} := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.gammaMeanNorm