English
For a function f : α → ℚ → ℝ, the transformed function (a, q) ↦ toRatCDF f a q equals f a q when a has the Rat-Stieltjes point property, and equals the default RatCDF q otherwise.
Русский
Для функции f : α → ℚ → ℝ преобразование (a, q) ↦ toRatCDF f a q даёт f a q, если a имеет свойство Rat-StieltjesPoint, иначе — defaultRatCDF q.
LaTeX
$$$$\\mathrm{toRatCDF}(f)(a)(q) = \\begin{cases} f(a,q), & \\text{если } \\mathrm{IsRatStieltjesPoint}(f,a), \\\\[2pt] \\mathrm{defaultRatCDF}(q), & \\text{иначе.} \\end{cases}$$$$
Lean4
/-- Turn a function `f : α → ℚ → ℝ` into another with the property `IsRatStieltjesPoint f a`
everywhere. At `a` that does not satisfy that property, `f a` is replaced by an arbitrary suitable
function.
Mainly useful when `f` satisfies the property `IsRatStieltjesPoint f a` almost everywhere with
respect to some measure. -/
noncomputable def toRatCDF (f : α → ℚ → ℝ) : α → ℚ → ℝ := fun a ↦ if IsRatStieltjesPoint f a then f a else defaultRatCDF
