tendsto_atBot_zero — Mathlib

English

If hf is IsRatCondKernelCDF, then for each a, almost surely in b, f(a,b) tends to 0 as its real argument goes to -∞.

Русский

Если hf — IsRatCondKernelCDF, то для каждого a почти наверняка по b, f(a,b) стремится к 0 при устремлении аргумента к -∞.

LaTeX

$$$\\forall a,\\, \\text{ae}_{b\\sim ν(a)}\\;\\ Tendsto\\left(f(a,b)\\right)_{\\to -\\infty} = 0$$$

Lean4

theorem tendsto_atBot_zero (hf : IsRatCondKernelCDF f κ ν) (a : α) : ∀ᵐ b ∂(ν a), Tendsto (f (a, b)) atBot (𝓝 0) := by
  filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atBot_zero

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