OAI/Probability/GammaPassage/EndpointEvents.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.endpointBox_finite line 9
2. def OAI.GammaFPP.CrossingBridge.endpointBoxVertices line 12
3. def OAI.GammaFPP.CrossingBridge.arbitraryEndpointEvent line 15
4. lemma OAI.GammaFPP.CrossingBridge.mem_arbitraryEndpointEvent line 19
5. lemma OAI.GammaFPP.CrossingBridge.measurableSet_arbitraryEndpointEvent line 27
6. lemma OAI.GammaFPP.CrossingBridge.arbitraryEndpointEvent_depends line 31
7. def OAI.GammaFPP.CrossingBridge.coarsePairIndices line 35
8. def OAI.GammaFPP.CrossingBridge.coarsePairEvent line 38
9. theorem OAI.GammaFPP.CrossingBridge.arbitraryEndpointEvent_coarse_cover line 44

   Source documentation

   On the grid event, the arbitrary-endpoint bad event is covered by a scale-independent finite list of translated rare-fast events.

   theorem arbitraryEndpointEvent_coarse_cover (shape rate b m₀ K A R a ε : ℝ)
       (hshape : 0 < shape) (hrate : 0 < rate) (hK : 100 ≤ K) (hm : 0 < m₀) (hA : 0 ≤ A) (hR : 0 ≤ R) (hε : 0 < ε)
       (k m J : ℕ) (hJ : 1 ≤ J) (hJlast : J ≤ gridLastLevel m) (hlast : gridLastLevel m ≤ k)
       (herror : 2*endpointExtensionError shape rate K k J+2*|a| ≤ ε*(2 : ℝ)^k/2)
       (hscale : (2*R*|a| /m₀)*(2 : ℝ)^k ≤ (gridMesh m J : ℝ)) :
       arbitraryEndpointEvent b m₀ a A R ε k m ⊆
         (gridConnectionsEvent shape rate b m₀ K A R k m J)ᶜ ∪
           ⋃ ij ∈ coarsePairIndices A J,coarsePairEvent b m₀ a A (R+2*(Grid.attachmentAllowance shape rate K)) ε k m J ij := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.endpointExtensionError, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.arbitraryEndpointEvent, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.coarsePairIndices, OAI.GammaFPP.CrossingBridge.coarsePairEvent, OAI.GammaFPP.Grid.attachmentAllowance