OAI/Probability/GammaPassage/LoopErasure.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.GammaFPP.LoopGraph.Weights line 14

   Source documentation

   Undirected edge weights; the domain contains only actual edges.

   abbrev Weights (G : SimpleGraph V) := G.edgeSet → ℝ

2. def OAI.GammaFPP.LoopGraph.edgeCost line 16
3. theorem OAI.GammaFPP.LoopGraph.edgeCost_symm line 19
4. def OAI.GammaFPP.LoopGraph.pathCost line 24

   Source documentation

   Recursion counts repeated traversals with multiplicity.

   def pathCost (w : Weights G) {x y : V} : G.Walk x y → ℝ
     | .nil => 0
     | .cons h p => edgeCost w h + pathCost w p

   Mentions: OAI.GammaFPP.LoopGraph.Weights, OAI.GammaFPP.LoopGraph.edgeCost

5. theorem OAI.GammaFPP.LoopGraph.pathCost_nil line 28
6. theorem OAI.GammaFPP.LoopGraph.pathCost_cons line 31
7. lemma OAI.GammaFPP.LoopGraph.pathCost_eq_darts_sum line 35
8. theorem OAI.GammaFPP.LoopGraph.bypass_cost_le line 42

   Source documentation

   Loop erasure does not increase a path's physical cost.

   theorem bypass_cost_le [DecidableEq V] (w : Weights G) (hw : ∀ e, 0 ≤ w e)
       {x y : V} (p : G.Walk x y) : pathCost w p.bypass ≤ pathCost w p := by
   …

   Mentions: OAI.GammaFPP.LoopGraph.Weights, OAI.GammaFPP.LoopGraph.pathCost

9. abbrev OAI.GammaFPP.LoopGraph.Vertex line 50
10. def OAI.GammaFPP.LoopGraph.lattice line 52
11. abbrev OAI.GammaFPP.LoopGraph.Edge line 57
12. abbrev OAI.GammaFPP.LoopGraph.Environment line 58
13. lemma OAI.GammaFPP.LoopErase.companion_adj_step line 65
14. lemma OAI.GammaFPP.LoopErase.companion_adj_iff line 69
15. def OAI.GammaFPP.LoopErase.companionEdge line 86
16. lemma OAI.GammaFPP.LoopErase.companionEdge_step line 90
17. lemma OAI.GammaFPP.LoopErase.companionEdge_injective line 95
18. lemma OAI.GammaFPP.LoopErase.companionEdge_surjective line 102
19. def OAI.GammaFPP.LoopErase.companionEdgeEquiv line 109
20. def OAI.GammaFPP.LoopErase.companionWeights line 112
21. lemma OAI.GammaFPP.LoopErase.companionWeights_edge line 115
22. lemma OAI.GammaFPP.LoopErase.companion_pathCost_copy line 120
23. lemma OAI.GammaFPP.LoopErase.steps_companion_walk line 125
24. lemma OAI.GammaFPP.LoopErase.companion_walk_steps_edges line 143

    Source documentation

    The walk-to-step bridge preserves the ordered list of unoriented edges, in addition to endpoints and traversal-counted cost.

    lemma companion_walk_steps_edges (w : Edge → ℝ) {p q : Vertex}
        (walk : GammaFPP.LoopGraph.lattice.Walk p q) :
        ∃ ds : List Step, p+displacement ds=q ∧
          pathCost w p ds=GammaFPP.LoopGraph.pathCost (companionWeights w) walk ∧
          ((trace p ds).map (fun t => (companionEdge (traversalEdge t)).val))=walk.edges := by
    …

    Mentions: OAI.GammaFPP.LoopGraph.pathCost, OAI.GammaFPP.LoopErase.companionWeights, OAI.GammaFPP.LoopErase.companionEdge

25. theorem OAI.GammaFPP.LoopErase.erase_path_loops line 161

    Source documentation

    Loop erasure in the exact original path model, for arbitrary endpoints and nonnegative real weights. It never increases cost.

    theorem erase_path_loops (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (p : Vertex) (ds : List Step) :
        ∃ es : List Step, displacement es=displacement ds ∧
          ((trace p es).map traversalEdge).Nodup ∧ pathCost w p es ≤ pathCost w p ds := by
    …

26. theorem OAI.GammaFPP.LoopErase.exists_near_optimal_simple_path line 176

    Source documentation

    Near-optimal paths with simple physical-edge traces, at every pair of lattice endpoints and every positive approximation error.

    theorem exists_near_optimal_simple_path (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
        (p q : Vertex) (ε : ℝ) (hε : 0 < ε) :
        ∃ ds : List Step, p+displacement ds=q ∧
          ((trace p ds).map traversalEdge).Nodup ∧
          passageTime w p q ≤ pathCost w p ds ∧ pathCost w p ds < passageTime w p q+ε := by
    …