OAI/Probability/GammaPassage/CheapPathDecay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.cheapChernoff line 12
2. def OAI.GammaFPP.cheapSlope line 15
3. lemma OAI.GammaFPP.cheapChernoff_pos line 18
4. lemma OAI.GammaFPP.cheapSlope_pos line 23
5. lemma OAI.GammaFPP.cheapChernoff_factor line 28

   Source documentation

   The exact native Gamma Laplace factor is 1/16 at the chosen parameter.

   lemma cheapChernoff_factor {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate) :
       (rate / (rate + cheapChernoff shape rate)) ^ shape = (1 / 16 : ℝ) := by
   …

   Mentions: OAI.GammaFPP.cheapChernoff

6. lemma OAI.GammaFPP.cheapChernoff_mul_slope line 44
7. lemma OAI.GammaFPP.cheap_count_bound_eq line 50

   Source documentation

   Exact cancellation of counting, Laplace factor and linear threshold.

   lemma cheap_count_bound_eq {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate) (n : ℕ) :
       (4 : ℝ)^n * (((rate / (rate + cheapChernoff shape rate)) ^ shape)^n /
         Real.exp (-cheapChernoff shape rate * (cheapSlope shape rate * (n : ℝ)))) =
           (1 / 2 : ℝ)^n := by
   …

   Mentions: OAI.GammaFPP.cheapChernoff, OAI.GammaFPP.cheapSlope

8. theorem OAI.GammaFPP.GammaEnvironment.cheap_fixed_length_decay_real line 70

   Source documentation

   All actual trails of n steps from p are exponentially unlikely to cost at most c*n. This includes n=0, where the empty path has probability one.

   theorem GammaEnvironment.cheap_fixed_length_decay_real
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p : Vertex) (n : ℕ) :
       P.real {ω | ∃ ds : List Step, ds.length = n ∧
         ((trace p ds).map traversalEdge).Nodup ∧
           pathCost (fun e => τ e ω) p ds ≤ cheapSlope shape rate * (n : ℝ)} ≤
         (1 / 2 : ℝ)^n := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.cheapSlope