OAI/Probability/GammaPassage/LocalMeanGap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.integral_indicator_le_sqrt_second_moment line 14

   Source documentation

   Cauchy–Schwarz bounds an integral restricted to a measurable event.

   lemma integral_indicator_le_sqrt_second_moment
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
       {S : Ω → ℝ} {E : Set Ω} (hE : MeasurableSet E)
       (hS : MemLp S 2 P) (hpos : 0 ≤ᵐ[P] S) :
       (∫ ω, E.indicator S ω ∂P) ≤
         Real.sqrt (∫ ω, (S ω)^2 ∂P) * Real.sqrt (P.real E) := by
   …

2. theorem OAI.GammaFPP.GammaEnvironment.ae_localPassageTime_gap_indicator line 46

   Source documentation

   The gap between local and unrestricted passage times is nonnegative and bounded by the coordinate-path cost on the event where they differ.

   theorem GammaEnvironment.ae_localPassageTime_gap_indicator
       (h : GammaEnvironment shape rate P τ) (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) :
       ∀ᵐ ω ∂P,
         0 ≤ FiniteLocal.passageTime (fun e => τ e ω) p q R -
           PlanarFPP.passageTime (fun e => τ e ω) p q ∧
         FiniteLocal.passageTime (fun e => τ e ω) p q R -
           PlanarFPP.passageTime (fun e => τ e ω) p q ≤
         {ω | FiniteLocal.passageTime (fun e => τ e ω) p q R ≠
           PlanarFPP.passageTime (fun e => τ e ω) p q}.indicator
             (fun ω => pathCost (fun e => τ e ω) p (coordinatePath p q)) ω := by
   …

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

3. theorem OAI.GammaFPP.GammaEnvironment.localPassageTime_mean_gap_le line 74

   Source documentation

   The difference of the local and unrestricted mean passage times is controlled by the coordinate-path second moment and the localization probability.

   theorem GammaEnvironment.localPassageTime_mean_gap_le
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R) :
       0 ≤ (∫ ω, FiniteLocal.passageTime (fun e => τ e ω) p q R ∂P) -
         (∫ ω, PlanarFPP.passageTime (fun e => τ e ω) p q ∂P) ∧
       (∫ ω, FiniteLocal.passageTime (fun e => τ e ω) p q R ∂P) -
         (∫ ω, PlanarFPP.passageTime (fun e => τ e ω) p q ∂P) ≤
         Real.sqrt (pathSecondMomentConstant shape rate * (latticeDistance p q : ℝ)^2) *
         Real.sqrt ((1 / 2 : ℝ)^R + 2 * Real.exp (-(rate / 4) *
           (cheapSlope shape rate * (R : ℝ) -
             coordinateAllowance shape rate * (latticeDistance p q : ℝ)))) := by
   …

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