OAI/Probability/GammaPassage/GridMeshes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Integer meshes with a final unit interval, and their comparison with characteristic lengths at record indices.

  1. def OAI.GammaFPP.CrossingBridge.gridMeshExponent line 12
  2. def OAI.GammaFPP.CrossingBridge.gridLastLevel line 13
  3. def OAI.GammaFPP.CrossingBridge.gridMesh line 14
  4. def OAI.GammaFPP.CrossingBridge.gridWidth line 15
  5. lemma OAI.GammaFPP.CrossingBridge.gridMesh_pos line 17
  6. lemma OAI.GammaFPP.CrossingBridge.gridWidth_pos line 18
  7. lemma OAI.GammaFPP.CrossingBridge.gridLastLevel_unit line 19
  8. lemma OAI.GammaFPP.CrossingBridge.gridMesh_antitone line 25
  9. lemma OAI.GammaFPP.CrossingBridge.gridMesh_ratio_le line 31
  10. lemma OAI.GammaFPP.CrossingBridge.gridMesh_divides line 36
  11. lemma OAI.GammaFPP.CrossingBridge.gridMesh_level_bound line 41
  12. lemma OAI.GammaFPP.CrossingBridge.gridMesh_count_ratio line 46
  13. lemma OAI.GammaFPP.CrossingBridge.gridWidth_ratio line 55
  14. lemma OAI.GammaFPP.CrossingBridge.gridMesh_below_record_length line 62
  15. theorem OAI.GammaFPP.CrossingBridge.gamma_grid_trial_probabilities line 88

    Source documentation

    Crossing trial probabilities at every allowed level of each sufficiently large characteristic record index.

    theorem gamma_grid_trial_probabilities (henv : GammaEnvironment shape rate P τ)
    (hs : 0 < shape) (hr : 0 < rate)
    (b q₀ : ℝ) (hb : |b| ≤ 1) (hq : 0 < q₀) (hq1 : q₀ < 1) :
    ∀ᶠ 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) : ℝ)) →
      q₀ < P.real {ω | (fun e => τ e ω) ∈ crossingEvent b ((gammaMeanNorm henv hs hr) (direction b))
        (sourceCrossingK shape rate (gammaMeanNorm henv hs hr) b) (gridWidth k j) (gridMesh (characteristicExponent P τ shape rate (gammaMeanNorm henv hs hr) b q₀ k) j) 0} := by
…

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.gridLastLevel, OAI.GammaFPP.CrossingBridge.characteristicExponent, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.CrossingBridge.sourceCrossingK, OAI.GammaFPP.CrossingBridge.gridWidth, OAI.GammaFPP.CrossingBridge.gridMesh