SpatialRareProbability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.gamma_spatial_rare_scales line 13

Source documentation

A single actual scale works simultaneously for every spatial index, and can also exceed any requested transverse scale and longitudinal aspect ratio.

theorem gamma_spatial_rare_scales (henv : GammaEnvironment shape rate P τ)
    (hshape : 0 < shape) (hrate : 0 < rate)
    (b q₀ η : ℝ) (hb : |b| ≤ 1) (hq : 0 < q₀) (hq1 : q₀ < 1) (hη : 0 < η)
    (N : ℕ) (S D : ℝ) :
    ∃ k : ℕ, N < k ∧ S ≤ (2 : ℝ)^k ∧
      D*(2 : ℝ)^k ≤ (characteristicLength P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ k : ℝ) ∧
      ∀ ih : ℤ×ℤ, P.real {ω | (fun e => τ e ω) ∈ spatialRareEvent b
        ((gammaMeanNorm henv hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm henv hshape hrate) b false)
        (extremeSlope (gammaMeanNorm henv hshape hrate) b true) (sourceCrossingK shape rate (gammaMeanNorm henv hshape hrate) b) η k
        (characteristicExponent P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ k) ih} ≤ 2*q₀ := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.spatialRareEvent, OAI.GammaFPP.CrossingBridge.sourceCrossingK, OAI.GammaFPP.CrossingBridge.characteristicExponent