ofReal_condCDF_ae_eq — Mathlib

English

For finite ρ and rational r, ENNReal.ofReal(condCDF ρ a r) is almost everywhere equal to preCDF ρ r a (i.e., a.e. equality after casting to ENNReal).

Русский

Для конечной меры ρ и рационального r отображение ENNReal.ofReal(condCDF ρ a r) почти везде равно preCDF ρ r a (после приведения к ENNReal).

LaTeX

$$$(a \\mapsto \\mathrm{ENNReal.ofReal}(condCDF(ρ,a,r))) =^\\mathrm{a.e.}_{ρ.fst} a \\mapsto preCDF(ρ,r,a)$$$

Lean4

theorem ofReal_condCDF_ae_eq (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (r : ℚ) :
    (fun a ↦ ENNReal.ofReal (condCDF ρ a r)) =ᵐ[ρ.fst] preCDF ρ r :=
  by
  filter_upwards [condCDF_ae_eq ρ r, preCDF_le_one ρ] with a ha ha_le_one
  rw [ha, ENNReal.ofReal_toReal]
  exact ((ha_le_one r).trans_lt ENNReal.one_lt_top).ne

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