OAI/Probability/GammaPassage/GoodSitePaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.goodSite_trial_witness line 10
2. theorem OAI.GammaFPP.CrossingBridge.sourceSupportCost_of_endpoint line 33
3. theorem OAI.GammaFPP.CrossingBridge.goodSite_connector_witness line 41

   Source documentation

   Both forward neighbors are exactly the two tested endpoint windows.

   theorem goodSite_connector_witness (μ : Plane → ℝ) (b A R ε s : ℝ) (plus : Bool)
       (n d : ℤ) (M : ℕ) (v v' : Vertex) (w : Edge → ℝ)
       (hg : w ∈ goodSiteEvent μ b A R ε s plus n d M v)
       (hstep : v'=v+(1,0) ∨ v'=v+(0,1))
       (p q : Vertex)
       (hp : p ∈ connectorWindow b (blockX n d v+n)
         (blockY (contactSign plus) (trialWindow M R s) v) (trialWindow M R s))
       (hq : q ∈ connectorWindow b (blockX n d v')
         (blockY (contactSign plus) (trialWindow M R s) v') (trialWindow M R s)) :
       ∃ ds, p+displacement ds=q ∧
         defect w b (μ (direction b)) (extremeSlope μ b plus) p ds ≤ ε*s/2 := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.goodSiteEvent, OAI.GammaFPP.CrossingBridge.connectorWindow, OAI.GammaFPP.CrossingBridge.blockX, OAI.GammaFPP.CrossingBridge.blockY, OAI.GammaFPP.CrossingBridge.contactSign, OAI.GammaFPP.CrossingBridge.trialWindow

4. theorem OAI.GammaFPP.CrossingBridge.UniformShape.no_goodSite_path line 75

   Source documentation

   At every fixed admissible scale, an infinite path of actual good sites is incompatible with the origin shape law. Adaptive endpoint choices are allowed.

   theorem UniformShape.no_goodSite_path (μ : Plane → ℝ) (hμ : TimeConstantNorm μ)
       (b A R ε s : ℝ) (plus : Bool) (n d : ℤ) (M : ℕ)
       (hb : |b| ≤ 1) (hR : 0 ≤ R) (hε : 0 < ε) (hs : 1 ≤ s)
       (hn : 0 < n) (hd : 0 ≤ d) (hM : 0 < M)
       (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (hu : UniformShape w μ) :
       ¬infiniteOrientedPath (fun v => w ∈ goodSiteEvent μ b A R ε s plus n d M v) 0 := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.UniformShape, OAI.GammaFPP.CrossingBridge.goodSiteEvent

5. theorem OAI.GammaFPP.CrossingBridge.gamma_goodSite_path_probability_zero line 112

   Source documentation

   The almost-sure uniform Gamma shape theorem gives probability zero for an infinite good-site path.

   theorem gamma_goodSite_path_probability_zero (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε s : ℝ) (plus : Bool) (n d : ℤ) (M : ℕ)
       (hb : |b| ≤ 1) (hR : 0 ≤ R) (hε : 0 < ε) (hs : 1 ≤ s)
       (hn : 0 < n) (hd : 0 ≤ d) (hM : 0 < M) :
       P {ω | infiniteOrientedPath (fun v => (fun e => τ e ω) ∈
         goodSiteEvent (gammaMeanNorm h hshape hrate) b A R ε s plus n d M v) 0}=0 := by
   …

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