tendsto_atTop_one — Mathlib

English

For a fixed a, almost every t, the limit of f(a,t) as t→∞ equals 1.

Русский

Для фиксированного a почти каждое t: предел f(a,t) при t→∞ равен 1.

LaTeX

$$$\forall a,\; \text{ae}_{t\sim ν(a)}(\lim_{t\to\infty} f(a,t)=1).$$$

Lean4

theorem tendsto_atTop_one (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν] (a : α) :
    ∀ᵐ t ∂(ν a), Tendsto (f (a, t)) atTop (𝓝 1) :=
  by
  suffices ∀ᵐ t ∂(ν a), Tendsto (fun (n : ℕ) ↦ f (a, t) n) atTop (𝓝 1)
    by
    filter_upwards [this, hf.mono a] with t ht h_mono
    rw [tendsto_iff_tendsto_subseq_of_monotone h_mono tendsto_natCast_atTop_atTop]
    exact ht
  filter_upwards [hf.tendsto_one_of_monotone a Nat.cast Nat.mono_cast tendsto_natCast_atTop_atTop] with x hx using hx

Похожие утверждения