OAI/Probability/GammaPassage/ShapeDeficit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.GammaFPP.CrossingBridge.UniformShape line 9
2. theorem OAI.GammaFPP.CrossingBridge.uniformShape_iff_gamma line 11
3. theorem OAI.GammaFPP.CrossingBridge.UniformShape.no_linear_deficit line 17

   Source documentation

   A supporting functional cannot be beaten by a linear amount along a linearly bounded escaping sequence of endpoints, even if that sequence was chosen after seeing the weights.

   theorem UniformShape.no_linear_deficit (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (μ f : Plane → ℝ) (hu : UniformShape w μ) (hf : ∀ v, f v ≤ μ v)
       (z : ℕ → Vertex) (ds : ℕ → List Step) (C a B : ℝ) (ha : 0 < a) (hB : 0 < B)
       (hescape : Tendsto (fun n => ‖latticeEmbed (z n)‖) atTop atTop)
       (hbound : ∀ n, ‖latticeEmbed (z n)‖ ≤ B*((n : ℝ)+1))
       (hend : ∀ n, displacement (ds n)=z n)
       (hcost : ∀ n, pathCost w 0 (ds n) ≤ f (latticeEmbed (z n))+C-a*n) : False := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.UniformShape