OAI/Probability/GammaPassage/RecordGridProbability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.gridConnectionsEvent_failure_bound line 15

   Source documentation

   Simultaneous finite-grid probability bound from subcharacteristic crossing bounds.

   theorem gridConnectionsEvent_failure_bound (henv : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (b m₀ K A R q₀ : ℝ) (hA : 0 < A) (hR : 0 < R) (hq : 0 < q₀) (hq1 : q₀ ≤ 1)
       (k m J : ℕ) (hJ : 1 ≤ J) (hlast : gridLastLevel m ≤ k)
       (htrial : ∀ j, J ≤ j → j ≤ gridLastLevel m →
         q₀ ≤ P.real {ω | (fun e => τ e ω) ∈ crossingEvent b m₀ K (gridWidth k j) (gridMesh m j) 0}) :
       P.real {ω | (fun e => τ e ω) ∉ gridConnectionsEvent shape rate b m₀ K A R k m J} ≤
         Grid.gridFailureTail shape (gridIndexConstant A R) q₀ J := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.CrossingBridge.gridWidth, OAI.GammaFPP.CrossingBridge.gridMesh, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.Grid.gridFailureTail, OAI.GammaFPP.CrossingBridge.gridIndexConstant

2. theorem OAI.GammaFPP.CrossingBridge.gamma_grid_connections line 74

   Source documentation

   Lemma gr:grid-tools for characteristic lengths satisfying the record-scale comparison.

   theorem gamma_grid_connections (henv : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (b q₀ A R : ℝ) (hb : |b| ≤ 1) (hq : 0 < q₀) (hq1 : q₀ < 1) (hA : 0 < A) (hR : 0 < R)
       (J : ℕ) (hJ : 1 ≤ J) :
       ∀ᶠ k : ℕ in atTop,
         (∀ j, j ≤ gridLastLevel (characteristicExponent P τ shape rate (gammaMeanNorm henv hs hr) b q₀ k) →
           (1/16 : ℝ)^j*(characteristicLength P τ shape rate (gammaMeanNorm henv hs hr) b q₀ k : ℝ) ≤
             (characteristicLength P τ shape rate (gammaMeanNorm henv hs hr) b q₀ (k-j) : ℝ)) →
         P.real {ω | (fun e => τ e ω) ∉ gridConnectionsEvent shape rate b ((gammaMeanNorm henv hs hr) (direction b))
           (sourceCrossingK shape rate (gammaMeanNorm henv hs hr) b) A R k (characteristicExponent P τ shape rate (gammaMeanNorm henv hs hr) b q₀ k) J} ≤
           Grid.gridFailureTail shape (gridIndexConstant A R) q₀ J := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.characteristicExponent, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.sourceCrossingK, OAI.GammaFPP.Grid.gridFailureTail, OAI.GammaFPP.CrossingBridge.gridIndexConstant

3. theorem OAI.GammaFPP.CrossingBridge.gamma_simultaneous_grid_scales line 98

   Source documentation

   Arbitrarily large characteristic record scales carry simultaneous grid bounds, independently of the box parameters and initial level.

   theorem gamma_simultaneous_grid_scales (henv : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (b q₀ : ℝ) (hb : |b| ≤ 1) (hq : 0 < q₀) (hq1 : q₀ < 1) :
       ∃ k₀ : ℕ, ∀ N : ℕ, ∃ k : ℕ, N < k ∧ k₀ ≤ k ∧
         (∀ j, j ≤ k-k₀ → (1/16 : ℝ)^j*(characteristicLength P τ shape rate (gammaMeanNorm henv hs hr) b q₀ k : ℝ) ≤
           (characteristicLength P τ shape rate (gammaMeanNorm henv hs hr) b q₀ (k-j) : ℝ)) ∧
         ∀ A R : ℝ, 0 < A → 0 < R → ∀ J : ℕ, 1 ≤ J →
           P.real {ω | (fun e => τ e ω) ∉ gridConnectionsEvent shape rate b ((gammaMeanNorm henv hs hr) (direction b))
             (sourceCrossingK shape rate (gammaMeanNorm henv hs hr) b) A R k (characteristicExponent P τ shape rate (gammaMeanNorm henv hs hr) b q₀ k) J} ≤
             Grid.gridFailureTail shape (gridIndexConstant A R) q₀ J := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.gridConnectionsEvent, OAI.GammaFPP.CrossingBridge.sourceCrossingK, OAI.GammaFPP.CrossingBridge.characteristicExponent, OAI.GammaFPP.Grid.gridFailureTail, OAI.GammaFPP.CrossingBridge.gridIndexConstant