OAI/Probability/GammaPassage/ActualNoCorner.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.gamma_direction_nat_limit line 15

   Source documentation

   The actual time constant along the manuscript's rounded direction sequence.

   lemma gamma_direction_nat_limit (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate) (b : ℝ) :
       ∀ᵐ ω ∂P, Tendsto
         (fun n : ℕ => passageTime (fun e => τ e ω) 0 ((n : ℤ),⌊b*(n : ℝ)⌋)/(n : ℝ))
         atTop (𝓝 ((gammaMeanNorm henv hshape hrate) (direction b))) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm

2. theorem OAI.GammaFPP.CrossingBridge.gamma_no_corner line 26
3. theorem OAI.GammaFPP.CrossingBridge.gamma_direction_differentiable line 53

   Source documentation

   The Gamma mean norm is Fréchet differentiable in every direction (1, b) with |b| ≤ 1.

   theorem gamma_direction_differentiable (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate) (b : ℝ) (hb : |b| ≤ 1) :
       DifferentiableAt ℝ (gammaMeanNorm henv hshape hrate) (direction b) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm