OAI/Probability/GammaPassage/CoordinateTails.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.coordinateAllowance line 19

   Source documentation

   A linear allowance depending on the Gamma shape and rate.

   noncomputable def coordinateAllowance (shape rate : ℝ) : ℝ := 2 * (shape + 1) / rate

2. lemma OAI.GammaFPP.coordinateAllowance_pos line 21
3. theorem OAI.GammaFPP.GammaEnvironment.costly_straight_probability line 27

   Source documentation

   Exponential upper tail for the cost of a straight lattice path.

   theorem GammaEnvironment.costly_straight_probability
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p : Vertex) (d : Step) (n : ℕ) (t : ℝ) :
       P {ω | t ≤ pathCost (fun e => τ e ω) p (List.replicate n d)} ≤
         (ENNReal.ofReal ((2 : ℝ) ^ shape)) ^ n /
           ENNReal.ofReal (Real.exp ((rate / 2) * t)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment

4. theorem OAI.GammaFPP.GammaEnvironment.costly_straight_probability_real line 44

   Source documentation

   The real-valued upper tail for the cost of a straight lattice path.

   theorem GammaEnvironment.costly_straight_probability_real
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p : Vertex) (d : Step) (n : ℕ) (t : ℝ) :
       P.real {ω | t ≤ pathCost (fun e => τ e ω) p (List.replicate n d)} ≤
         ((2 : ℝ) ^ shape) ^ n * Real.exp (-(rate / 2) * t) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment

5. lemma OAI.GammaFPP.gamma_half_rate_mgf_bound line 62
6. theorem OAI.GammaFPP.GammaEnvironment.costly_straight_excess_probability_real line 73

   Source documentation

   Exponential tail above the linear allowance, for every real excess t.

   theorem GammaEnvironment.costly_straight_excess_probability_real
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p : Vertex) (d : Step) (n : ℕ) (t : ℝ) :
       P.real {ω | coordinateAllowance shape rate * (n : ℝ) + t ≤
         pathCost (fun e => τ e ω) p (List.replicate n d)} ≤
         Real.exp (-(rate / 2) * t) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.coordinateAllowance

7. theorem OAI.GammaFPP.GammaEnvironment.costly_horizontal_excess_probability_real line 97
8. theorem OAI.GammaFPP.GammaEnvironment.costly_vertical_excess_probability_real line 110
9. theorem OAI.GammaFPP.GammaEnvironment.costly_coordinatePath_probability_real line 124

   Source documentation

   A union bound for the two coordinate legs, counting every edge traversal.

   theorem GammaEnvironment.costly_coordinatePath_probability_real
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (t : ℝ) :
       P.real {ω | coordinateAllowance shape rate * (latticeDistance p q : ℝ) + t ≤
         pathCost (fun e => τ e ω) p (coordinatePath p q)} ≤
         2 * Real.exp (-(rate / 4) * t) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.coordinateAllowance