OAI/Probability/GammaPassage/ConnectorEvents.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.allPairsRegionEvent line 11
2. theorem OAI.GammaFPP.CrossingBridge.mem_allPairsRegionEvent line 16
3. theorem OAI.GammaFPP.CrossingBridge.measurableSet_allPairsRegionEvent line 23
4. theorem OAI.GammaFPP.CrossingBridge.allPairsRegionEvent_depends line 30
5. theorem OAI.GammaFPP.CrossingBridge.gamma_allPairsRegionEvent line 50

   Source documentation

   Uniform connection estimates for finite-region endpoint tests from diameter, support-cost, and tube-containment bounds.

   theorem gamma_allPairsRegionEvent (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (D η δ : ℝ) (hD : 0 < D) (hη : 0 < η) (hδ : 0 < δ) :
       ∀ ε > 0, ∀ᶠ s : ℝ in atTop, ∀ (V : Finset Vertex) (I J : Set Vertex)
         (bound : Vertex → Vertex → ℝ),
         (∀ p ∈ I ∪ J, ∀ q ∈ I ∪ J, ‖latticeEmbed (q-p)‖ ≤ D*s) →
         (∀ p ∈ I, ∀ q ∈ J, gammaMeanNorm h hshape hrate (latticeEmbed (q-p))+η*s ≤ bound p q) →
         (∀ p ∈ I, ∀ q ∈ J, SegmentTube p q (δ*s) ⊆ (V : Set Vertex)) →
         P.real {ω | (fun e => τ e ω) ∉ allPairsRegionEvent V I J bound} < ε := by
   …

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