OAI/Probability/GammaPassage/CrossingChain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.crossingChain line 10
2. theorem OAI.GammaFPP.CrossingBridge.crossingChain_endpoint line 14
3. theorem OAI.GammaFPP.CrossingBridge.crossingChain_defect line 24
4. theorem OAI.GammaFPP.CrossingBridge.oriented_path_coordinates line 49

   Source documentation

   A forward path from zero lies in its indexed layer, with nonnegative coordinates bounded by the layer index.

   theorem oriented_path_coordinates (v : ℕ → Vertex) (h0 : v 0=0)
       (hs : ∀ n, v (n+1)=v n+(1,0) ∨ v (n+1)=v n+(0,1)) (n : ℕ) :
       (v n).1+(v n).2=(n : ℤ) ∧ 0 ≤ (v n).1 ∧ 0 ≤ (v n).2 ∧ (v n).2 ≤ n := by
   …

5. theorem OAI.GammaFPP.CrossingBridge.UniformShape.no_crossing_chain line 60

   Source documentation

   A crossing chain with a linear deficit contradicts the uniform shape law when its endpoints escape with at most linear growth.

   theorem UniformShape.no_crossing_chain (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (μ : Plane → ℝ) (hu : UniformShape w μ) (b m a e B : ℝ) (he : 0 < e) (hB : 0 < B)
       (hf : ∀ v, m*v 0+a*(v 1-b*v 0) ≤ μ v)
       (initialPath : List Step) (trial connector : ℕ → List Step) (p z : ℕ → Vertex)
       (hp : displacement initialPath=p 0)
       (ht : ∀ n, p n+displacement (trial n)=z n)
       (hc : ∀ n, z n+displacement (connector n)=p (n+1))
       (htrial : ∀ n, defect w b m a (p n) (trial n) ≤ -e)
       (hconnector : ∀ n, defect w b m a (z n) (connector n) ≤ e/2)
       (hescape : Tendsto (fun n => ‖latticeEmbed (z n)‖) atTop atTop)
       (hbound : ∀ n, ‖latticeEmbed (z n)‖ ≤ B*((n : ℝ)+1)) : False := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.UniformShape