OAI/Probability/GammaPassage/CharacteristicLengths.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.firstDyadicExponent line 10
2. theorem OAI.GammaFPP.CrossingBridge.firstDyadicExponent_spec line 15
3. theorem OAI.GammaFPP.CrossingBridge.firstDyadicExponent_le line 19
4. theorem OAI.GammaFPP.CrossingBridge.firstDyadicExponent_min line 24
5. def OAI.GammaFPP.CrossingBridge.sourceDyadicCrossingProbability line 32
6. def OAI.GammaFPP.CrossingBridge.characteristicExponent line 36
7. def OAI.GammaFPP.CrossingBridge.characteristicLength line 39
8. theorem OAI.GammaFPP.CrossingBridge.characteristicLength_pos line 44
9. theorem OAI.GammaFPP.CrossingBridge.gamma_characteristic_lengths_exist line 48

   Source documentation

   The first dyadic crossing threshold exists and occurs by 2^(3*k).

   theorem gamma_characteristic_lengths_exist (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b q : ℝ) (hb : |b| ≤ 1) (hq : 0 < q) :
       ∀ᶠ k : ℕ in atTop,
         characteristicExponent P τ shape rate (gammaMeanNorm h hshape hrate) b q k ≤ 3*k ∧
         P.real {ω | (fun e => τ e ω) ∈ crossingEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (sourceCrossingK shape rate (gammaMeanNorm h hshape hrate) b)
           ((2 : ℝ)^k) (characteristicLength P τ shape rate (gammaMeanNorm h hshape hrate) b q k) 0} ≤ q := by
   …

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

10. theorem OAI.GammaFPP.CrossingBridge.characteristicLength_minimal line 60

    Source documentation

    Every smaller dyadic size has crossing probability strictly above q.

    theorem characteristicLength_minimal (shape rate : ℝ) (μ : Plane → ℝ) (b q : ℝ) (k j : ℕ)
        (hj : (2 : ℤ)^j < characteristicLength P τ shape rate μ b q k) :
        q < sourceDyadicCrossingProbability P τ shape rate μ b k j := by
    …

    Mentions: OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.CrossingBridge.sourceDyadicCrossingProbability

11. theorem OAI.GammaFPP.CrossingBridge.gamma_characteristic_lengths_ratio line 71

    Source documentation

    The characteristic lengths grow faster than the transverse scale: L_k / 2^k → ∞.

    theorem gamma_characteristic_lengths_ratio (h : GammaEnvironment shape rate P τ)
        (hshape : 0 < shape) (hrate : 0 < rate)
        (b q : ℝ) (hb : |b| ≤ 1) (hq : 0 < q) (hq1 : q < 1) :
        Tendsto (fun k : ℕ => (characteristicLength P τ shape rate (gammaMeanNorm h hshape hrate) b q k : ℝ)/(2 : ℝ)^k) atTop atTop := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.gammaMeanNorm

12. theorem OAI.GammaFPP.CrossingBridge.gamma_characteristic_record_scales line 93

    Source documentation

    Characteristic lengths have arbitrarily large record scales satisfying the dyadic comparison bound.

    theorem gamma_characteristic_record_scales (h : GammaEnvironment shape rate P τ)
        (hshape : 0 < shape) (hrate : 0 < rate)
        (b q : ℝ) (hb : |b| ≤ 1) (hq : 0 < q) :
        ∃ k0 : ℕ, ∀ N, ∃ k, N < k ∧ k0 ≤ k ∧
          ∀ j, j ≤ k-k0 → (1/16 : ℝ)^j*(characteristicLength P τ shape rate (gammaMeanNorm h hshape hrate) b q k : ℝ) ≤
            (characteristicLength P τ shape rate (gammaMeanNorm h hshape hrate) b q (k-j) : ℝ) := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.characteristicLength, OAI.GammaFPP.gammaMeanNorm