OAI/Probability/GammaPassage/CheapPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.trace_edge_length line 10
2. lemma OAI.GammaFPP.pathCost_trace_edge_sum line 18
3. lemma OAI.GammaFPP.pathCost_eq_distinct_edgeSum line 26

   Source documentation

   Only a trail's traversal sum can be replaced by its distinct-edge set sum.

   lemma pathCost_eq_distinct_edgeSum (w : Edge → ℝ) (p : Vertex) (ds : List Step)
       (hn : ((trace p ds).map traversalEdge).Nodup) :
       pathCost w p ds = ∑ e ∈ ((trace p ds).map traversalEdge).toFinset, w e := by
   …

4. theorem OAI.GammaFPP.GammaEnvironment.cheap_path_probability line 38

   Source documentation

   Genuine Gamma lower tail for any fixed trail, with arbitrary real threshold. The positive parameter s uses the native MGF at theta=-s.

   theorem GammaEnvironment.cheap_path_probability
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (s : ℝ) (hsp : 0 < s) (p : Vertex) (ds : List Step)
       (hn : ((trace p ds).map traversalEdge).Nodup) (t : ℝ) :
       P {ω | pathCost (fun e => τ e ω) p ds ≤ t} ≤
         (ENNReal.ofReal ((rate / (rate + s)) ^ shape)) ^ ds.length /
           ENNReal.ofReal (Real.exp (-s * t)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment

5. theorem OAI.GammaFPP.GammaEnvironment.cheap_path_probability_real line 56

   Source documentation

   Conversion keeps the upper bound finite before passing to real probability.

   theorem GammaEnvironment.cheap_path_probability_real
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (s : ℝ) (hsp : 0 < s) (p : Vertex) (ds : List Step)
       (hn : ((trace p ds).map traversalEdge).Nodup) (t : ℝ) :
       P.real {ω | pathCost (fun e => τ e ω) p ds ≤ t} ≤
         ((rate / (rate + s)) ^ shape) ^ ds.length * Real.exp (s * t) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment

6. theorem OAI.GammaFPP.GammaEnvironment.cheap_path_family_probability line 78

   Source documentation

   The probability that a finite family contains a cheap trail is bounded by its cardinality times the single-trail estimate.

   theorem GammaEnvironment.cheap_path_family_probability
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (s : ℝ) (hsp : 0 < s) (p : Vertex) (F : Finset (List Step)) (n : ℕ)
       (hF : ∀ ds ∈ F, ((trace p ds).map traversalEdge).Nodup ∧ ds.length = n)
       (t : ℝ) :
       P {ω | ∃ ds ∈ F, pathCost (fun e => τ e ω) p ds ≤ t} ≤
         (F.card : ℝ≥0∞) * ((ENNReal.ofReal ((rate / (rate + s)) ^ shape)) ^ n /
           ENNReal.ofReal (Real.exp (-s * t))) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment