Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ :=
  ENNReal.measurable_ofReal.comp_aemeasurable hXm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ :=
  ENNReal.measurable_ofReal.comp_aemeasurable hYm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have h3 : AEMeasurable (X * Y) μ := hXm.mul hYm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have h4 : 0 ≤ᵐ[μ] X * Y := ae_of_all _ fun ω => mul_nonneg (hXp ω) (hYp ω)
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal ((X * Y) a) ∂μ) =
    ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ)
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ hXp) hXm.aestronglyMeasurable,
  integral_eq_lintegral_of_nonneg_ae (ae_of_all _ hYp) hYm.aestronglyMeasurable,
  integral_eq_lintegral_of_nonneg_ae h4 h3.aestronglyMeasurable]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ) =
    ENNReal.toReal ((∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ)
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal ((X * Y) a) ∂μ) =
    ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ)
simp_rw [← ENNReal.toReal_mul, Pi.mul_apply, ENNReal.ofReal_mul (hXp _)]
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ) =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ) =
    ENNReal.toReal ((∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ)
congr
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ IndepFun (fun a => ENNReal.ofReal (X a)) fun a => ENNReal.ofReal (Y a)
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ) =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' h1 h2
no goals
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ IndepFun (fun a => ENNReal.ofReal (X a)) fun a => ENNReal.ofReal (Y a)
exact hXY.comp ENNReal.measurable_ofReal ENNReal.measurable_ofReal