OAI/Probability/GammaPassage/EndpointNet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.IntervalTravelBridge.latticeEmbed_add line 10
2. theorem OAI.GammaFPP.IntervalTravelBridge.step_embed_norm_le line 15
3. theorem OAI.GammaFPP.IntervalTravelBridge.displacement_norm_le_length line 19
4. theorem OAI.GammaFPP.IntervalTravelBridge.coordinatePath_length line 29
5. theorem OAI.GammaFPP.IntervalTravelBridge.coordinatePath_prefix_bound line 39
6. theorem OAI.GammaFPP.IntervalTravelBridge.segmentPoint_perturbation line 47
7. theorem OAI.GammaFPP.IntervalTravelBridge.segmentTube_perturbation line 65
8. theorem OAI.GammaFPP.IntervalTravelBridge.localTravel_attach line 78

   Source documentation

   Concatenates two explicit coordinate attachments and a net connection. Every traversal is charged and every vertex is retained in the tube.

   theorem localTravel_attach (μ : Plane → ℝ) (w : Edge → ℝ)
       (β : ℝ) (hβ : 0 ≤ β) (hlip : ∀ v u, |μ v-μ u| ≤ β*‖v-u‖)
       (p q p' q' : Vertex) (r a η δ s : ℝ)
       (hp : ‖latticeEmbed (p'-p)‖ ≤ r) (hq : ‖latticeEmbed (q'-q)‖ ≤ r)
       (hleft : pathCost w p (coordinatePath p p') ≤ a)
       (hright : pathCost w q' (coordinatePath q' q) ≤ a)
       (hmid : LocalTravel μ η δ s p' q' w) :
       ∃ ds, p+displacement ds=q ∧
           pathCost w p ds ≤ μ (latticeEmbed (q-p))+η*s+2*a+2*β*r ∧
           PathIn p ds (SegmentTube p q (max (3*r) (δ*s+r))) := by
   …

   Mentions: OAI.GammaFPP.IntervalTravelBridge.LocalTravel, OAI.GammaFPP.IntervalTravelBridge.PathIn, OAI.GammaFPP.IntervalTravelBridge.SegmentTube

9. theorem OAI.GammaFPP.IntervalTravelBridge.finite_ball_net line 139

   Source documentation

   A fixed finite Euclidean net; its cardinality is independent of scale.

   theorem finite_ball_net (D γ : ℝ) (hγ : 0 < γ) :
       ∃ S : Finset {v : Plane // ‖v‖ ≤ D},
         ∀ v : Plane, ‖v‖ ≤ D → ∃ u ∈ S, ‖v-u.val‖ < γ := by
   …

10. theorem OAI.GammaFPP.IntervalTravelBridge.lattice_mem_box_of_norm line 155
11. theorem OAI.GammaFPP.IntervalTravelBridge.scaled_net_norm line 165
12. theorem OAI.GammaFPP.IntervalTravelBridge.scaled_net_approximates line 174