English
Equality of setwise L-integrals with preCDF against ρ.IicSnd on s.
Русский
Равенство линтеграла по множеству с preCDF против IicSnd на s.
LaTeX
$$$\int^{\! -} x \in s, preCDF ρ r x \partial ρ.fst = ρ.IicSnd r s$$$
Lean4
/-- `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)`. -/
noncomputable def preCDF (ρ : Measure (α × ℝ)) (r : ℚ) : α → ℝ≥0∞ :=
Measure.rnDeriv (ρ.IicSnd r) ρ.fst
