OAI/Probability/GammaPassage/RareFast.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.gamma_rareFast_eventually line 13

   Source documentation

   Quantitative rare-fast bound in terms of an integer ceiling.

   theorem gamma_rareFast_eventually (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε : ℝ) (hb : |b| ≤ 1) (hA : 0 < A) (hR : 0 ≤ R) (hε : 0 < ε)
       (plus : Bool) (p0 : ℝ) (hp0 : 0 < p0) (hp1 : p0 ≤ 1) :
       ∃ D0 : ℝ, 1 ≤ D0 ∧ ∀ᶠ s : ℝ in atTop, ∀ n : ℤ,
         (⌈D0*s⌉ : ℝ)+s ≤ n →
         P.real {ω | (fun e => τ e ω) ∈
           rareFastEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm h hshape hrate) b plus) A R ε s n 0} < p0 := by
   …

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

2. theorem OAI.GammaFPP.CrossingBridge.gamma_rareFast_bound line 60

   Source documentation

   Exact two-parameter epsilon formulation: once s and n/s are large, the probability of the manuscript's strict localized event is small.

   theorem gamma_rareFast_bound (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε : ℝ) (hb : |b| ≤ 1) (hA : 0 < A) (hR : 0 ≤ R) (hε : 0 < ε)
       (plus : Bool) (κ : ℝ) (hκ : 0 < κ) :
       ∃ S K : ℝ, 1 ≤ S ∧ 0 < K ∧ ∀ s : ℝ, S ≤ s → ∀ n : ℤ,
         K*s ≤ n → P.real {ω | (fun e => τ e ω) ∈
           rareFastEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm h hshape hrate) b plus) A R ε s n 0} < κ := by
   …

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

3. theorem OAI.GammaFPP.CrossingBridge.gamma_rareFast_tendsto line 80

   Source documentation

   Rare-fast joint limit along arbitrary filters with s → ∞ and n/s → ∞, where n is integer-valued and eventually positive.

   theorem gamma_rareFast_tendsto {ι : Type*} {l : Filter ι}
       (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε : ℝ) (hb : |b| ≤ 1) (hA : 0 < A) (hR : 0 ≤ R) (hε : 0 < ε)
       (plus : Bool) (s : ι → ℝ) (n : ι → ℤ)
       (hs : Tendsto s l atTop) (hn : Tendsto (fun i => (n i : ℝ)/s i) l atTop) :
       Tendsto (fun i => P.real {ω | (fun e => τ e ω) ∈
         rareFastEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm h hshape hrate) b plus) A R ε (s i) (n i) 0}) l (𝓝 0) := by
   …

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

4. theorem OAI.GammaFPP.CrossingBridge.gamma_rareFast_translate_tendsto line 100

   Source documentation

   Exact translations, even chosen differently at each scale, have the same probability and therefore the same rare-fast limit.

   theorem gamma_rareFast_translate_tendsto {ι : Type*} {l : Filter ι}
       (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε : ℝ) (hb : |b| ≤ 1) (hA : 0 < A) (hR : 0 ≤ R) (hε : 0 < ε)
       (plus : Bool) (s : ι → ℝ) (n : ι → ℤ) (t : ι → Vertex)
       (hs : Tendsto s l atTop) (hn : Tendsto (fun i => (n i : ℝ)/s i) l atTop) :
       Tendsto (fun i => P.real {ω | (fun e => τ e ω) ∈
         rareFastEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm h hshape hrate) b plus) A R ε (s i) (n i) (t i)}) l (𝓝 0) := by
   …

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