OAI/Probability/GammaPassage/GridEvents.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.measurableSet_gridBinGood line 10
2. def OAI.GammaFPP.CrossingBridge.gridTestsEvent line 25
3. def OAI.GammaFPP.CrossingBridge.gridConnectionsEvent line 31
4. lemma OAI.GammaFPP.CrossingBridge.measurableSet_gridConnectionsEvent line 34
5. theorem OAI.GammaFPP.CrossingBridge.gridConnectionsEvent_paths line 52

   Source documentation

   On the constructed event, all endpoint pairs in all bins connect, with the Gamma cost and localization allowance K+200*shape/rate.

   theorem gridConnectionsEvent_paths (weights : Edge → ℝ)
       (shape rate b m₀ K A R : ℝ) (hs : 0 < shape) (hrate : 0 < rate) (hK : 100 ≤ K) (k m J : ℕ) (hJ : 1 ≤ J)
       (hg : weights ∈ gridConnectionsEvent shape rate b m₀ K A R k m J)
       (j : ℕ) (hj : J ≤ j ∧ j ≤ gridLastLevel m) (i : ℤ)
       (hi : -(A+4)*(2 : ℝ)^m ≤ ((gridMesh m j*i : ℤ) : ℝ) ∧
         ((gridMesh m j*i+gridMesh m j : ℤ) : ℝ) ≤ (A+4)*(2 : ℝ)^m)
       (r₀ : ℝ) (hr : |r₀| ≤ R*(2 : ℝ)^k)
       (p q : Vertex)
       (hp : p.1=gridMesh m j*i ∧ |transverse b p-r₀| ≤ 1)
       (hq : q.1=gridMesh m j*i+gridMesh m j ∧ |transverse b q-r₀| ≤ 1) :
       ∃ ds, p+displacement ds=q ∧
         pathCost weights p ds ≤ m₀*(gridMesh m j)+(Grid.attachmentAllowance shape rate K)*(j : ℝ)^2*(gridWidth k j) ∧
   …

   Mentions: OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.Grid.attachmentAllowance, OAI.GammaFPP.CrossingBridge.gridWidth