OAI/Probability/GammaPassage/ContiguousWitnesses.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.trace_append line 8
2. lemma OAI.GammaFPP.CrossingBridge.trace_split line 15

   Source documentation

   A contiguous split of actual traversals is a split into actual paths.

   lemma trace_split (p : Vertex) (ds : List Step) (xs ys : List Traversal)
       (h : trace p ds=xs++ys) :
       ∃ pre rest : List Step, ds=pre++rest ∧ trace p pre=xs ∧
         trace (p+displacement pre) rest=ys := by
   …

3. lemma OAI.GammaFPP.CrossingBridge.trace_edges line 31
4. lemma OAI.GammaFPP.CrossingBridge.simple_append_edges line 37
5. theorem OAI.GammaFPP.CrossingBridge.spatial_negative_prefix_witnesses line 50

   Source documentation

   Source wi:chunk-defect. Construct actual labelled negative-prefix witnesses inside the original box, with disjoint physical edges and the basic bound.

   theorem spatial_negative_prefix_witnesses (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (b m₀ am ap K η : ℝ) (ha : am ≤ ap) (hη : 0 ≤ η)
       (k m : ℕ) (ih : ℤ×ℤ)
       (hscale : max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*(2 : ℝ)^k)
       (p : Vertex) (ds : List Step)
       (hin : PathIn p ds {z | z-spatialTranslate b k m ih ∈ endpointBox b 4 4 k m})
       (hsimple : ((trace p ds).map traversalEdge).Nodup) :
       ∃ ws : List GammaFPP.BK.StrictPathWitness,
         ws.Pairwise (fun q r => Disjoint q.edges r.edges) ∧
         (∀ q ∈ ws, q ∈ spatialWitnessFamily b m₀ am ap K η k m ih ∧
           q.Good w ∧ q.edges ⊆ pathEdges p ds) ∧
         -η*(2 : ℝ)^k-2*η*(2 : ℝ)^k*ws.length ≤ defect w b m₀ ((am+ap)/2) p ds := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.PathIn, OAI.GammaFPP.CrossingBridge.spatialTranslate, OAI.GammaFPP.CrossingBridge.endpointBox, OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily, OAI.GammaFPP.CrossingBridge.pathEdges