SpatialPositiveChunk.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.positive_longitudinal_chunk_witness line 10

Source documentation

Positive-longitudinal case of wi:chunk-witness. The outer pieces are checked first; otherwise the actual middle subcrossing witnesses E(s,L).

theorem positive_longitudinal_chunk_witness (w : Edge → ℝ) (b m₀ am ap K η : ℝ)
    (hb : |b| ≤ 1) (ha : am ≤ ap) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
    (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)
    (hx : (displacement ds).1=2*(2 : ℤ)^m)
    (hcheap : defect w b m₀ ((am+ap)/2) p ds < η*(2 : ℝ)^k) :
    ∃ q ∈ spatialWitnessFamily b m₀ am ap K η k m (spatialChunkIndex b k m p),
      q.Good w ∧ q.edges ⊆ pathEdges p ds := by
…

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

theorem OAI.GammaFPP.CrossingBridge.cheap_full_spatial_chunk_witness line 108

Source documentation

Complete source wi:chunk-witness for actual full chunks.

theorem cheap_full_spatial_chunk_witness (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)
    (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)
    (hcheap : defect w b m₀ ((am+ap)/2) p ds < η*(2 : ℝ)^k) :
    ∃ q ∈ spatialWitnessFamily b m₀ am ap K η k m (spatialChunkIndex b k m p),
      q.Good w ∧ q.edges ⊆ pathEdges p ds := by
…

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