OAI/Probability/GammaPassage/GlobalCenteredConcentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.centered_event_comparison line 14

   Source documentation

   Comparing two observables and their centers bounds the probability of a centered deviation. The estimate holds for arbitrary measures.

   lemma centered_event_comparison (P : Measure Ω) (X Y : Ω → ℝ)
       (a b s d : ℝ) (hd : |b-a| ≤ d) :
       P {ω | s+d ≤ |X ω-a|} ≤
         P {ω | s ≤ |Y ω-b|} + P {ω | Y ω ≠ X ω} := by
   …

2. theorem OAI.GammaFPP.GammaEnvironment.passageTime_centered_exponential_of_mean_gap line 36

   Source documentation

   The localization error and a bound on the deterministic mean shift control unrestricted centered deviations. The case p = q is included when 0 < R.

   theorem GammaEnvironment.passageTime_centered_exponential_of_mean_gap
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R)
       (b : ℝ)
       (hb : |(∫ ω, FiniteLocal.passageTime (fun e => τ e ω) p q R ∂P) -
         ∫ ω, PlanarFPP.passageTime (fun e => τ e ω) p q ∂P| ≤ b)
       (t : ℝ) :
       P.real {ω | t*sqrt R+b ≤ |PlanarFPP.passageTime (fun e => τ e ω) p q -
         ∫ η, PlanarFPP.passageTime (fun e => τ e η) p q ∂P|} ≤
         2*exp (1-FiniteLocal.concentrationKappa shape rate*t) +
         ((1/2 : ℝ)^R + 2*exp (-(rate/4) *
           (cheapSlope shape rate*(R : ℝ) -
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.FiniteLocal.passageTime, OAI.PlanarFPP.passageTime, OAI.GammaFPP.FiniteLocal.concentrationKappa, OAI.GammaFPP.cheapSlope

3. theorem OAI.GammaFPP.GammaEnvironment.passageTime_centered_exponential_shifted line 73

   Source documentation

   Gamma centered concentration with the difference of the localized and unrestricted means included in the deviation threshold.

   theorem GammaEnvironment.passageTime_centered_exponential_shifted
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R) (t : ℝ) :
       P.real {ω | t*sqrt R +
         |(∫ η, FiniteLocal.passageTime (fun e => τ e η) p q R ∂P) -
           ∫ η, PlanarFPP.passageTime (fun e => τ e η) p q ∂P| ≤
         |PlanarFPP.passageTime (fun e => τ e ω) p q -
           ∫ η, PlanarFPP.passageTime (fun e => τ e η) p q ∂P|} ≤
         2*exp (1-FiniteLocal.concentrationKappa shape rate*t) +
         ((1/2 : ℝ)^R + 2*exp (-(rate/4) *
           (cheapSlope shape rate*(R : ℝ) -
             coordinateAllowance shape rate*(latticeDistance p q : ℝ)))) :=
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.FiniteLocal.passageTime, OAI.PlanarFPP.passageTime, OAI.GammaFPP.FiniteLocal.concentrationKappa, OAI.GammaFPP.cheapSlope, OAI.GammaFPP.coordinateAllowance

4. lemma OAI.GammaFPP.localization_exponential_scale_separation line 89

   Source documentation

   A quantitative separation of the distance and localization scales bounds the difference between localized and unrestricted means.

   lemma localization_exponential_scale_separation
       {shape rate d r : ℝ} (hr : 0 < rate)
       (hscale : 2 * coordinateAllowance shape rate * d ≤ cheapSlope shape rate * r) :
       exp (-(rate/4) * (cheapSlope shape rate*r-coordinateAllowance shape rate*d)) ≤
         exp (-(rate*cheapSlope shape rate/8)*r) := by
   …

   Mentions: OAI.GammaFPP.coordinateAllowance, OAI.GammaFPP.cheapSlope