isRatStieltjesPoint_ae — Mathlib

English

Same as above: almost surely, for all q, iInf over r>I q of f(a,t) r equals f(a,t) q.

Русский

То же самое: почти наверняка для каждого q верхний инфимум равен f(a,t) q.

LaTeX

$$$\forall a,\; \text{ae}_{t\sim ν(a)}(\forall q, \; \iInf_{r>I q} f(a,t) r = f(a,t) q).$$$

Lean4

theorem isRatStieltjesPoint_ae (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) :
    ∀ᵐ t ∂(ν a), IsRatStieltjesPoint f (a, t) :=
  by
  filter_upwards [hf.tendsto_atTop_one a, hf.tendsto_atBot_zero a, hf.iInf_rat_gt_eq a, hf.mono a] with t ht_top ht_bot
    ht_iInf h_mono
  exact ⟨h_mono, ht_top, ht_bot, ht_iInf⟩

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