condCDF_ae_eq — Mathlib

English

For each rational r, the function a ↦ condCDF ρ a r is almost everywhere equal to a ↦ (preCDF ρ r a).toReal with respect to ρ.fst.

Русский

Для каждого рационального r функция a ↦ condCDF ρ a r равна почти наверняка функции a ↦ (preCDF ρ r a)^{toReal} по мере ρ.fst.

LaTeX

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

Lean4

theorem condCDF_ae_eq (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (r : ℚ) :
    (fun a ↦ condCDF ρ a r) =ᵐ[ρ.fst] fun a ↦ (preCDF ρ r a).toReal :=
  by
  simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]
  exact stieltjesOfMeasurableRat_ae_eq (isRatCondKernelCDF_preCDF ρ) () r

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