OAI/Probability/GammaPassage/RareFastEvents.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.finite_tilted_rectangle line 8
2. def OAI.GammaFPP.CrossingBridge.rareFastRegion line 44
3. theorem OAI.GammaFPP.CrossingBridge.rareFastRegion_finite line 48
4. def OAI.GammaFPP.CrossingBridge.rareFastVertices line 63
5. theorem OAI.GammaFPP.CrossingBridge.mem_rareFastVertices line 66
6. def OAI.GammaFPP.CrossingBridge.rareFastEvent line 70
7. theorem OAI.GammaFPP.CrossingBridge.mem_rareFastEvent line 75
8. theorem OAI.GammaFPP.CrossingBridge.measurableSet_rareFastEvent line 89
9. theorem OAI.GammaFPP.CrossingBridge.rareFastEvent_depends line 93
10. theorem OAI.GammaFPP.CrossingBridge.rareFastEvent_translate line 100

    Source documentation

    Translating weights is exactly equivalent to translating all path vertices; the supporting functional is evaluated on the unchanged displacement.

    theorem rareFastEvent_translate (b m a A R ε s : ℝ) (n : ℤ) (t : Vertex) (w : Edge → ℝ) :
        (fun e => w (shiftEdge t e)) ∈ rareFastEvent b m a A R ε s n 0 ↔
          w ∈ rareFastEvent b m a A R ε s n t := by
    …

    Mentions: OAI.GammaFPP.CrossingBridge.rareFastEvent

11. theorem OAI.GammaFPP.CrossingBridge.rareFastEvent_probability_translate line 129