OAI/Probability/GammaPassage/NoCornerContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.long_paths_contradict_directional_limit line 13

   Source documentation

   The source no-corner contradiction, using actual near-optimal simple paths and the cut-number bound. No geodesic existence or selected-path limit is assumed.

   theorem long_paths_contradict_directional_limit (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (b m₀ a η : ℝ) (hb : |b| ≤ 1) (hη : 0 < η) (k m : ℕ)
       (hlim : Tendsto (fun n : ℕ => passageTime w 0 ((n : ℤ),⌊b*(n : ℝ)⌋)/(n : ℝ)) atTop (𝓝 m₀))
       (hlong : ∀ᶠ N : ℕ in atTop, ∀ blocks : List (List Step), ∀ rest : List Step,
         blocks.length=N → (∀ q ∈ blocks, FullSpatialChunk b k m q) →
         (∀ i ≤ rest.length, chunkInterior b k m (displacement (rest.take i))) →
         ((trace 0 (blocks.flatten++rest)).map traversalEdge).Nodup →
         N*η*(2 : ℝ)^k/2 ≤ defect w b m₀ a 0 (blocks.flatten++rest)) : False := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.FullSpatialChunk, OAI.GammaFPP.CrossingBridge.chunkInterior