OAI/Probability/GammaPassage/SpatialWitnessCounts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.spatial_full_chunk_witnesses line 11

   Source documentation

   A constructive form of wi:full-defect. If the greedy family is empty, a cheap full chunk supplies a single witness. No maximum is assumed.

   theorem spatial_full_chunk_witnesses (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (b m₀ am ap K η : ℝ) (hb : |b| ≤ 1) (ha : am ≤ ap) (hη : 0 < η)
       (hgap : 4*η ≤ (ap-am)/2) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
       (hstep : max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*(2 : ℝ)^k)
       (hscale₁ : η*(2 : ℝ)^k < 2*m₀*(2 : ℝ)^m-|((am+ap)/2)| *((2 : ℝ)^k+1))
       (hscale₂ : 3*η*(2 : ℝ)^k+2*|((am+ap)/2)| *((2 : ℝ)^k+1) < K*(2 : ℝ)^k)
       (p : Vertex) (ds : List Step) (hfull : FullSpatialChunk b k m ds)
       (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 (spatialChunkIndex b k m p) ∧
           q.Good w ∧ q.edges ⊆ pathEdges p ds) ∧
   …

   Mentions: OAI.GammaFPP.CrossingBridge.FullSpatialChunk, OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily, OAI.GammaFPP.CrossingBridge.spatialChunkIndex, OAI.GammaFPP.CrossingBridge.pathEdges

2. theorem OAI.GammaFPP.CrossingBridge.spatial_total_witnesses line 47

   Source documentation

   Source wi:total-defect, including all physical-edge disjointness and the actual ordered chunk indices. Witness families are constructed, not supplied.

   theorem spatial_total_witnesses (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (b m₀ am ap K η : ℝ) (hb : |b| ≤ 1) (ha : am ≤ ap) (hη : 0 < η)
       (hgap : 4*η ≤ (ap-am)/2) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
       (hstep : max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*(2 : ℝ)^k)
       (hscale₁ : η*(2 : ℝ)^k < 2*m₀*(2 : ℝ)^m-|((am+ap)/2)| *((2 : ℝ)^k+1))
       (hscale₂ : 3*η*(2 : ℝ)^k+2*|((am+ap)/2)| *((2 : ℝ)^k+1) < K*(2 : ℝ)^k)
       (p : Vertex) (blocks : List (List Step)) (rest : List Step)
       (hfull : ∀ q ∈ blocks, FullSpatialChunk b k m q)
       (hrest : ∀ i ≤ rest.length, chunkInterior b k m (displacement (rest.take i)))
       (hsimple : ((trace p (blocks.flatten++rest)).map traversalEdge).Nodup) :
       ∃ packs : List (List GammaFPP.BK.StrictPathWitness),
         packs.length=blocks.length+1 ∧
   …

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