FiniteWaypoints.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.IntervalTravelBridge.gamma_finite_waypoint_failure_bound line 13

Source documentation

A location-uniform finite union estimate. The common shape-test error is at the fixed origin, while every tested location may be different.

theorem gamma_finite_waypoint_failure_bound
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    {ι : Type*} (J : Finset ι) (a : ι → Vertex) (C n : ℕ) (η δ : ℝ) :
    P.real {ω | ∃ j ∈ J, ¬GoodOrigin (gammaMeanNorm h hs hr)
      (cheapSlope shape rate) C η δ n (fun e => τ (shiftEdge (a j) e) ω)} ≤
      (J.card : ℝ) * P.real {ω | ¬GoodOrigin (gammaMeanNorm h hs hr)
        (cheapSlope shape rate) C η δ n (fun e => τ e ω)} := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.IntervalTravelBridge.GoodOrigin, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.cheapSlope

theorem OAI.GammaFPP.IntervalTravelBridge.gamma_finite_waypoint_failure_tendsto line 48

Source documentation

With a fixed finite number of tests, simultaneous success has failure probability tending to zero even at arbitrary deterministic moving locations.

theorem gamma_finite_waypoint_failure_tendsto
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    {ι : Type*} (J : Finset ι) (a : ℕ → ι → Vertex)
    (C : ℕ) (hC : 0 < C) (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) :
    Tendsto (fun n => P.real {ω | ∃ j ∈ J, ¬GoodOrigin (gammaMeanNorm h hs hr)
      (cheapSlope shape rate) C η δ n (fun e => τ (shiftEdge (a n j) e) ω)})
      atTop (𝓝 0) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.IntervalTravelBridge.GoodOrigin, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.cheapSlope