withDensity_preCDF — Mathlib

English

The first marginal of ρ with density preCDF ρ r equals IicSnd r.

Русский

Первая маргинальная мера ρ с плотностью preCDF ρ r равна IicSnd r.

LaTeX

$$$\rho.fst.withDensity (preCDF ρ r) = ρ.IicSnd r$$$

Lean4

theorem withDensity_preCDF (ρ : Measure (α × ℝ)) (r : ℚ) [IsFiniteMeasure ρ] :
    ρ.fst.withDensity (preCDF ρ r) = ρ.IicSnd r :=
  Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq.mp (Measure.IicSnd_ac_fst ρ r)

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