setIntegral_toReal_rnDeriv_eq_withDensity

English

Equality between the ν-weighted real integral of μ.rnDeriv ν over s and the real-valued μ.real(s) when using a density transformation.

Русский

Равенство между ν-взвешенным реальным интегралом μ.rnDeriv ν над s и реальным μ.real(s) при преобразовании плотности.

LaTeX

$$$\\int_{s} (μ.rnDeriv ν(x))^{\\toReal} dν(x) = μ.real(s)$$$

Lean4

theorem setIntegral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ] [SFinite ν] (s : Set α) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s :=
  by
  rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]
  · rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]
    simp
  · exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

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