stieltjesOfMeasurableRat — Mathlib

English

If f is a measurable function, then for all a and rational r we have stieltjesOfMeasurableRat f hf a r = toRatCDF f a r; i.e., the constructed Stieltjes object agrees with the Rat-CDF.

Русский

Пусть f измерима; тогда для всех a и рационального r выполняется равенство stieltjesOfMeasurableRat f hf a r = toRatCDF f a r: построенная функция Стильтьджеса совпадает с Rat-CDF.

LaTeX

$$$\forall a \in \alpha, \forall r \in \mathbb{Q},\; \text{stieltjesOfMeasurableRat}(f, hf, a)(r) = \text{toRatCDF}(f, a, r)$$$

Lean4

/-- Turn a measurable function `f : α → ℚ → ℝ` into a measurable function `α → StieltjesFunction`.
Composition of `toRatCDF` and `IsMeasurableRatCDF.stieltjesFunction`. -/
noncomputable def stieltjesOfMeasurableRat (f : α → ℚ → ℝ) (hf : Measurable f) : α → StieltjesFunction :=
  (isMeasurableRatCDF_toRatCDF hf).stieltjesFunction

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