Lemmas about integrable functions #
theorem
MeasureTheory.Integrable.congr_identDistrib
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{μ : Measure Ω}
{μ' : Measure Ω'}
{X : Ω → ℝ}
{Y : Ω' → ℝ}
(hX : Integrable X μ)
(hXY : ProbabilityTheory.IdentDistrib X Y μ μ')
:
Integrable Y μ'