OAI/Probability/GammaPassage/EndpointProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Uniform over all positive coarse spans. The rare-fast estimate is used in its full joint form, before selecting any endpoint pair at a given scale.

   theorem gamma_coarsePair_bound (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε : ℝ) (hb : |b| ≤ 1) (hA : 0 < A) (hR : 0 ≤ R) (hε : 0 < ε)
       (plus : Bool) (J : ℕ) (κ : ℝ) (hκ : 0 < κ) :
       ∃ S D : ℝ, 1 ≤ S ∧ 0 < D ∧ ∀ k m : ℕ, S ≤ (2 : ℝ)^k →
         D*(2 : ℝ)^k ≤ (gridMesh m J : ℝ) → ∀ ij ∈ coarsePairIndices A J,
         P.real {ω | (fun e => τ e ω) ∈
           coarsePairEvent b ((gammaMeanNorm henv hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm henv hshape hrate) b plus) A R ε k m J ij} < κ := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.coarsePairIndices, OAI.GammaFPP.CrossingBridge.coarsePairEvent, OAI.GammaFPP.gammaMeanNorm

2. theorem OAI.GammaFPP.CrossingBridge.gamma_arbitraryEndpoint_probability_bound line 40

   Source documentation

   Actual arbitrary-endpoint probability is bounded by grid failure plus a fixed finite collection of jointly rare positive-span crossings.

   theorem gamma_arbitraryEndpoint_probability_bound (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b K A R ε : ℝ) (hb : |b| ≤ 1) (hK : 100 ≤ K) (hm : 0 < (gammaMeanNorm henv hshape hrate) (direction b))
       (hA : 0 < A) (hR : 0 < R) (hε : 0 < ε) (plus : Bool)
       (J : ℕ) (hJ : 1 ≤ J) (κ : ℝ) (hκ : 0 < κ) :
       ∃ S D : ℝ, 1 ≤ S ∧ 0 < D ∧ ∀ k m : ℕ,
         J ≤ gridLastLevel m → gridLastLevel m ≤ k → S ≤ (2 : ℝ)^k →
         D*(2 : ℝ)^k ≤ (gridMesh m J : ℝ) →
         2*endpointExtensionError shape rate K k J+2*|extremeSlope (gammaMeanNorm henv hshape hrate) b plus| ≤ ε*(2 : ℝ)^k/2 →
         (2*R*|extremeSlope (gammaMeanNorm henv hshape hrate) b plus| /((gammaMeanNorm henv hshape hrate) (direction b)))*(2 : ℝ)^k ≤ (gridMesh m J : ℝ) →
         P.real {ω | (fun e => τ e ω) ∈
           arbitraryEndpointEvent b ((gammaMeanNorm henv hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm henv hshape hrate) b plus) A R ε k m} ≤
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.endpointExtensionError, OAI.GammaFPP.CrossingBridge.arbitraryEndpointEvent