OAI/Probability/GammaPassage/SpatialWitnesses.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.translatedArbitraryEndpointEvent line 11
2. lemma OAI.GammaFPP.CrossingBridge.mem_translatedArbitraryEndpointEvent line 16

   Source documentation

   Exact source event in a translated box, with unrestricted endpoints.

   lemma mem_translatedArbitraryEndpointEvent (b m₀ a A R ε : ℝ) (k m : ℕ) (t : Vertex) (w : Edge → ℝ) :
       w ∈ translatedArbitraryEndpointEvent b m₀ a A R ε k m t ↔
         ∃ p ds, PathIn p ds {z | z-t ∈ endpointBox b A R k m} ∧ defect w b m₀ a p ds < -ε*(2 : ℝ)^k := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.translatedArbitraryEndpointEvent, OAI.GammaFPP.CrossingBridge.PathIn, OAI.GammaFPP.CrossingBridge.endpointBox

3. def OAI.GammaFPP.CrossingBridge.eitherEndpointEvent line 37
4. lemma OAI.GammaFPP.CrossingBridge.mem_eitherEndpointEvent line 41
5. def OAI.GammaFPP.CrossingBridge.spatialTranslate line 54
6. def OAI.GammaFPP.CrossingBridge.spatialRareEvent line 57
7. def OAI.GammaFPP.CrossingBridge.spatialWitnessFamily line 63

   Source documentation

   Exact labelled path witnesses for the two defining spatial rare events. A support-defect witness retains which strict bound it satisfies.

   noncomputable def spatialWitnessFamily (b m₀ am ap K η : ℝ) (k m : ℕ) (ih : ℤ×ℤ) : Set GammaFPP.BK.StrictPathWitness :=
   …

   Mentions: OAI.GammaFPP.BK.StrictPathWitness

8. lemma OAI.GammaFPP.CrossingBridge.spatialWitness_good_event line 72
9. lemma OAI.GammaFPP.CrossingBridge.spatialRareEvent_has_witness line 96
10. lemma OAI.GammaFPP.CrossingBridge.translatedEndpointBox_finite line 117
11. def OAI.GammaFPP.CrossingBridge.spatialWitnessVertices line 123
12. def OAI.GammaFPP.CrossingBridge.spatialWitnessSupport line 127
13. lemma OAI.GammaFPP.CrossingBridge.spatialWitness_edges line 130
14. lemma OAI.GammaFPP.CrossingBridge.spatialWitness_event_iff line 141
15. def OAI.GammaFPP.CrossingBridge.spatialListSupport line 151