nonneg — Mathlib

English

There exists almost surely that the Stieltjes point property holds: IsRatStieltjesPoint f(a,t) for almost every t with respect to ν a.

Русский

Почти наверняка выполняется свойство IsRatStieltjesPoint для f(a,t).

LaTeX

$$$\forall a,\; \text{ae}_{t\sim ν(a)}\; IsRatStieltjesPoint(f, (a,t)).$$$

Lean4

theorem nonneg (hf : IsCondKernelCDF f κ ν) (p : α × β) (x : ℝ) : 0 ≤ f p x :=
  Monotone.le_of_tendsto (f p).mono (hf.tendsto_atBot_zero p) x

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