OAI/Probability/GammaPassage/LocalResamplingModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.FiniteLocal.localEdges line 9
2. lemma OAI.GammaFPP.FiniteLocal.candidate_edges_subset line 13
3. abbrev OAI.GammaFPP.FiniteLocal.Coordinates line 20
4. def OAI.GammaFPP.FiniteLocal.extend line 22
5. lemma OAI.GammaFPP.FiniteLocal.extend_apply line 26
6. lemma OAI.GammaFPP.FiniteLocal.extend_nonneg line 31
7. lemma OAI.GammaFPP.FiniteLocal.extend_update line 39
8. def OAI.GammaFPP.FiniteLocal.finitePassageTime line 54
9. lemma OAI.GammaFPP.FiniteLocal.trailCost_one_edge_change line 59

   Source documentation

   Changing one edge weight changes a trail cost by that weight difference when the edge belongs to the trail, and by zero otherwise.

   lemma trailCost_one_edge_change (w w' : Edge → ℝ) (e : Edge)
       (h : ∀ f, f ≠ e → w' f = w f) (p : Vertex) (ds : List Step)
       (hn : ((trace p ds).map traversalEdge).Nodup) :
       pathCost w' p ds - pathCost w p ds =
         if e ∈ (trace p ds).map traversalEdge then w' e - w e else 0 := by
   …

10. def OAI.GammaFPP.FiniteLocal.upward line 81

    Source documentation

    Upward change in the exact finite candidate infimum.

    noncomputable def upward (w : Edge → ℝ) (p q : Vertex) (R : ℕ)
        (e : Edge) (u : ℝ) : ℝ := by
    …

11. lemma OAI.GammaFPP.FiniteLocal.upward_nonneg line 86
12. lemma OAI.GammaFPP.FiniteLocal.upward_le line 91

    Source documentation

    One minimizing trail in the initial environment controls every upward coordinate-resampling increment.

    lemma upward_le (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
        (p q : Vertex) (R : ℕ) (ds : List Step) (hds : ds ∈ candidates p q R)
        (hm : pathCost w p ds = passageTime w p q R) (e : Edge) (u : ℝ) (hu : 0 ≤ u) :
        upward w p q R e u ≤ if e ∈ (trace p ds).map traversalEdge then u else 0 := by
    …

    Mentions: OAI.GammaFPP.FiniteLocal.candidates, OAI.GammaFPP.FiniteLocal.passageTime, OAI.GammaFPP.FiniteLocal.upward