OAI/Probability/GammaPassage/SourceTilt.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.norm_direction_pos line 13
2. theorem OAI.GammaFPP.CrossingBridge.gamma_crossing_cubic_tendsto line 23

   Source documentation

   A stronger form of gr:tilt: any integer n >= s^3 works. In particular, no dyadic-grid property is used in the measure-change argument.

   theorem gamma_crossing_cubic_tendsto {ι : Type*} {l : Filter ι}
       (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate) (b K : ℝ) (hb : |b| ≤ 1) (hK : 0 ≤ K)
       (s : ι → ℝ) (n : ι → ℤ) (hs : Tendsto s l atTop)
       (hn3 : ∀ᶠ i in l, (s i)^3 ≤ n i) :
       Tendsto (fun i => P.real {ω | (fun e => τ e ω) ∈
         crossingEvent b ((gammaMeanNorm h hshape hrate) (direction b)) K (s i) (n i) 0}) l (𝓝 0) := by
   …

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

3. def OAI.GammaFPP.CrossingBridge.sourceCrossingK line 69
4. theorem OAI.GammaFPP.CrossingBridge.sourceCrossingK_ge_hundred line 72
5. theorem OAI.GammaFPP.CrossingBridge.sourceCrossingK_ge_coordinateAllowance line 78
6. theorem OAI.GammaFPP.CrossingBridge.gamma_source_tilt line 85

   Source documentation

   Dyadic tilt limit with a Gamma geometric and coordinate allowance.

   theorem gamma_source_tilt (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b : ℝ) (hb : |b| ≤ 1) :
       Tendsto (fun k : ℕ => P.real {ω | (fun e => τ e ω) ∈
         crossingEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (sourceCrossingK shape rate (gammaMeanNorm h hshape hrate) b) ((2 : ℝ)^k) ((2 : ℤ)^(3*k)) 0})
         atTop (𝓝 0) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.sourceCrossingK