OAI/Probability/GammaPassage/CrossingTilt.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.crossingEvent_tilt_implication line 12
2. theorem OAI.GammaFPP.CrossingBridge.source_tilt_exponent_bound line 44
3. theorem OAI.GammaFPP.CrossingBridge.gamma_crossing_tilt_bound line 57

   Source documentation

   Squared change-of-measure estimate, with a constant independent of s and n whenever n ≥ s^3.

   theorem gamma_crossing_tilt_bound {shape rate : ℝ}
       (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
       (b m a K lam s : ℝ) (n : ℤ) (hK : 0 ≤ K) (hlam : 0 ≤ lam)
       (hs : 1 ≤ s) (hn : 1 ≤ n) (hn3 : s^3 ≤ n)
       (hsmall : lam*s/n ≤ 1/2) (hgain : K+16*|a|+1 < lam*m) :
       P.real {ω | (fun e => τ e ω) ∈ crossingEvent b m K s n 0} ^ 2 ≤
         Real.exp (288*shape*lam^2) *
           P.real {ω | (fun e => τ e ω) ∈ rareFastEvent b m a 1 8 1 s n 0} := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.CrossingBridge.rareFastEvent