OAI/Probability/GammaPassage/SpatialChunkWitness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.negative_midpoint_spatial_witness line 11

   Source documentation

   A negative midpoint defect in the actual chunk box is already a labelled witness for one of the extreme support events.

   lemma negative_midpoint_spatial_witness (w : Edge → ℝ) (b m₀ am ap K η : ℝ)
       (ha : am ≤ ap) (k m : ℕ) (ih : ℤ×ℤ) (p : Vertex) (ds : List Step)
       (hin : PathIn p ds {z | z-spatialTranslate b k m ih ∈ endpointBox b 4 4 k m})
       (hc : defect w b m₀ ((am+ap)/2) p ds < -η*(2 : ℝ)^k) :
       ∃ q ∈ spatialWitnessFamily b m₀ am ap K η k m ih,
         q.start=p ∧ q.steps=ds ∧ q.Good w := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.PathIn, OAI.GammaFPP.CrossingBridge.spatialTranslate, OAI.GammaFPP.CrossingBridge.endpointBox, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily

2. theorem OAI.GammaFPP.CrossingBridge.full_chunk_transverse_witness line 34

   Source documentation

   The transverse-exit case of wi:chunk-witness. The witnessing path is the whole original chunk, so its physical edge set is unchanged.

   theorem full_chunk_transverse_witness (w : Edge → ℝ) (b m₀ am ap K η : ℝ)
       (hb : |b| ≤ 1) (ha : am ≤ ap) (hη : 0 < η) (hgap : 4*η ≤ (ap-am)/2)
       (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k) (p : Vertex) (ds : List Step)
       (hfull : FullSpatialChunk b k m ds)
       (htrans : (2 : ℝ)^k ≤ |transverse b (displacement 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.start=p ∧ q.steps=ds ∧ q.Good w := by
   …

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

3. lemma OAI.GammaFPP.CrossingBridge.negative_longitudinal_chunk_not_cheap line 58

   Source documentation

   Nonnegative weights exclude a cheap chunk exiting through the negative longitudinal boundary, at the exact deterministic source scale.

   lemma negative_longitudinal_chunk_not_cheap (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (b m₀ a η : ℝ) (hb : |b| ≤ 1) (k m : ℕ) (p : Vertex) (ds : List Step)
       (hfull : FullSpatialChunk b k m ds)
       (hx : (displacement ds).1= -2*(2 : ℤ)^m)
       (hscale : η*(2 : ℝ)^k < 2*m₀*(2 : ℝ)^m-|a| *((2 : ℝ)^k+1)) :
       η*(2 : ℝ)^k < defect w b m₀ a p ds := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.FullSpatialChunk