setLIntegral_condDistrib_of_measurableSet

English

For measurable X, Y AE-measurable, s, t measurable, the lintegral over the preimage X⁻¹ t of condDistrib equals μ of the intersection t ∩ Y⁻¹ s after appropriate identifications.

Русский

Для измеримых X, Y AE-измеримой, s и t измеримы, линтеграл по X⁻¹ t от condDistrib равен мере пересечения t ∩ Y⁻¹ s после соответствующих преобразований.

LaTeX

$$$\\int_{X^{-1} t}^{-} condDistrib(Y,X,μ)(X a)(s) \\, dμ(a) = μ(X^{-1}(t) ∩ Y^{-1}(s)).$$$

Lean4

theorem setLIntegral_condDistrib_of_measurableSet (hX : Measurable X) (hY : AEMeasurable Y μ) (hs : MeasurableSet s)
    {t : Set α} (ht : MeasurableSet[mβ.comap X] t) : ∫⁻ a in t, condDistrib Y X μ (X a) s ∂μ = μ (t ∩ Y ⁻¹' s) :=
  by
  obtain ⟨t', ht', rfl⟩ := ht
  rw [setLIntegral_preimage_condDistrib hX hY hs ht']

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