EndpointRecords.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.gamma_arbitraryEndpoint_record_scales line 14

Source documentation

Lemma gr:variable-endpoints on characteristic record scales, chosen independently of the box parameters, deficit, and sign.

theorem gamma_arbitraryEndpoint_record_scales (henv : GammaEnvironment shape rate P τ)
    (hshape : 0 < shape) (hrate : 0 < rate)
    (b q₀ : ℝ) (hb : |b| ≤ 1) (hq : 0 < q₀) (hq1 : q₀ < 1) :
    ∃ k₀ : ℕ, ∃ k : ℕ → ℕ, Tendsto k atTop atTop ∧
      (∀ n, n < k n ∧ k₀ ≤ k n ∧
        ∀ j, j ≤ k n-k₀ → (1/16 : ℝ)^j*(characteristicLength P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ (k n) : ℝ) ≤
          (characteristicLength P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ (k n-j) : ℝ)) ∧
      ∀ A R ε : ℝ, 0 < A → 0 < R → 0 < ε → ∀ plus : Bool,
        Tendsto (fun n => P.real {ω | (fun e => τ e ω) ∈ arbitraryEndpointEvent b ((gammaMeanNorm henv hshape hrate) (direction b))
          (extremeSlope (gammaMeanNorm henv hshape hrate) b plus) A R ε (k n) (characteristicExponent P τ shape rate (gammaMeanNorm henv hshape hrate) b q₀ (k n))}) atTop (𝓝 0) := by
…

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