stieltjesOfMeasurableRat_nonneg

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.stieltjesOfMeasurableRat_nonneg

← MathLib Explorer

English

For all a and r, stieltjesOfMeasurableRat f hf a r is nonnegative.

Русский

Для любых a и r функция Стильтьджеса неотрицательна: stieltjesOfMeasurableRat f hf a r ≥ 0.

LaTeX

$$$0 \le stieltjesOfMeasurableRat(f,hf,a)(r)$$$

Lean4

theorem stieltjesOfMeasurableRat_nonneg (hf : Measurable f) (a : α) (r : ℝ) : 0 ≤ stieltjesOfMeasurableRat f hf a r :=
  IsMeasurableRatCDF.stieltjesFunction_nonneg _ a r

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru