OAI/Probability/GammaPassage/FiniteTails.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.GammaEnvironment.exponential_markov_edgeSum line 16

   Source documentation

   Exponential Markov bound for a real parameter theta and an arbitrary real threshold.

   theorem GammaEnvironment.exponential_markov_edgeSum
       (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
       (htheta : theta < rate) (S : Finset PlanarFPP.Edge) (a : ℝ) :
       P {ω | theta * a ≤ theta * edgeSum S τ ω} ≤
         (ENNReal.ofReal ((rate / (rate - theta)) ^ shape)) ^ S.card /
           ENNReal.ofReal (Real.exp (theta * a)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.edgeSum

2. theorem OAI.GammaFPP.GammaEnvironment.upper_tail_edgeSum line 39

   Source documentation

   Gamma Chernoff upper-tail estimate for 0 < theta < rate.

   theorem GammaEnvironment.upper_tail_edgeSum
       (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
       (htheta_pos : 0 < theta) (htheta : theta < rate)
       (S : Finset PlanarFPP.Edge) (a : ℝ) :
       P {ω | a ≤ edgeSum S τ ω} ≤
         (ENNReal.ofReal ((rate / (rate - theta)) ^ shape)) ^ S.card /
           ENNReal.ofReal (Real.exp (theta * a)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.edgeSum

3. theorem OAI.GammaFPP.GammaEnvironment.lower_tail_edgeSum line 52

   Source documentation

   Gamma Chernoff lower-tail estimate for theta < 0.

   theorem GammaEnvironment.lower_tail_edgeSum
       (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
       (htheta_neg : theta < 0) (S : Finset PlanarFPP.Edge) (a : ℝ) :
       P {ω | edgeSum S τ ω ≤ a} ≤
         (ENNReal.ofReal ((rate / (rate - theta)) ^ shape)) ^ S.card /
           ENNReal.ofReal (Real.exp (theta * a)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.edgeSum

4. theorem OAI.GammaFPP.GammaEnvironment.upper_tail_edgeSum_linear line 63
5. theorem OAI.GammaFPP.GammaEnvironment.lower_tail_edgeSum_linear line 76

   Source documentation

   A lower-tail estimate at a threshold proportional to the number of edges.

   theorem GammaEnvironment.lower_tail_edgeSum_linear
       (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
       (htheta_neg : theta < 0) (S : Finset PlanarFPP.Edge) (c : ℝ) :
       P {ω | edgeSum S τ ω ≤ (S.card : ℝ) * c} ≤
         (ENNReal.ofReal ((rate / (rate - theta)) ^ shape) /
           ENNReal.ofReal (Real.exp (theta * c))) ^ S.card := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.edgeSum