Theorems · Definition · probability

ProbabilityTheory.preCDF

{α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure (α × ℝ) → ℚ → α → ENNReal

preCDF is the Radon-Nikodym derivative of ρ.IicSnd with respect to ρ.fst at each r : ℚ. This function ℚ → α → ℝ≥0∞ is such that for almost all a : α, the function ℚ → ℝ≥0∞ satisfies the properties of a cdf (monotone with limit 0 at -∞ and 1 at +∞, right-continuous). We define this function on ℚ and not ℝ because ℚ is countable, which allows us to prove properties of the form ∀ᵐ a ∂ρ.fst, ∀ q, P (preCDF q a), instead of the weaker ∀ q, ∀ᵐ a ∂ρ.fst, P (preCDF q a).

Defined in

Mathlib.Probability.Kernel.Disintegration.CondCDF

Cited by

15 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound