case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y

case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y
by_cases h'X : X =ᵐ[μ] 0
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y

case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
by_cases h'Y : Y =ᵐ[μ] 0
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y

case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
by_cases h : Integrable (X * Y) μ
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
h' : X * Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have h' : X * Y =ᵐ[μ] 0 := by
  filter_upwards [h'X] with ω hω
  simp [hω]
no goals
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
h' : X * Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
simp only [integral_congr_ae h'X, integral_congr_ae h', Pi.zero_apply, integral_const,
  Algebra.id.smul_eq_mul, MulZeroClass.mul_zero, MulZeroClass.zero_mul]
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
ω : Ω
hω : X ω = OfNat.ofNat 0 ω
⊢ (X * Y) ω = OfNat.ofNat 0 ω
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
⊢ X * Y =ᵐ[μ] 0
filter_upwards [h'X] with ω hω
no goals
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
ω : Ω
hω : X ω = OfNat.ofNat 0 ω
⊢ (X * Y) ω = OfNat.ofNat 0 ω
simp [hω]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
h' : X * Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have h' : X * Y =ᵐ[μ] 0 := by
  filter_upwards [h'Y] with ω hω
  simp [hω]
no goals
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
h' : X * Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
simp only [integral_congr_ae h'Y, integral_congr_ae h', Pi.zero_apply, integral_const,
  Algebra.id.smul_eq_mul, MulZeroClass.mul_zero, MulZeroClass.zero_mul]
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
ω : Ω
hω : Y ω = OfNat.ofNat 0 ω
⊢ (X * Y) ω = OfNat.ofNat 0 ω
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
⊢ X * Y =ᵐ[μ] 0
filter_upwards [h'Y] with ω hω
no goals
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
ω : Ω
hω : Y ω = OfNat.ofNat 0 ω
⊢ (X * Y) ω = OfNat.ofNat 0 ω
simp [hω]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
HX : Integrable X
⊢ integral μ (X * Y) = integral μ X * integral μ Y
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have HX : Integrable X μ := hXY.integrable_left_of_integrable_mul h hX hY h'Y
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
HX : Integrable X
HY : Integrable Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
HX : Integrable X
⊢ integral μ (X * Y) = integral μ X * integral μ Y
have HY : Integrable Y μ := hXY.integrable_right_of_integrable_mul h hX hY h'X
no goals
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
HX : Integrable X
HY : Integrable Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
exact hXY.integral_mul_of_integrable HX HY
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ 0 = integral μ X * integral μ Y
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
rw [integral_undef h]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬(Integrable X ∧ Integrable Y)
⊢ 0 = integral μ X * integral μ Y
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ 0 = integral μ X * integral μ Y
have I : ¬(Integrable X μ ∧ Integrable Y μ) := by
  rintro ⟨HX, HY⟩
  exact h (hXY.integrable_mul HX HY)
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬Integrable X ∨ ¬Integrable Y
⊢ 0 = integral μ X * integral μ Y
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬(Integrable X ∧ Integrable Y)
⊢ 0 = integral μ X * integral μ Y
rw [not_and_or] at I
no goals
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬Integrable X ∨ ¬Integrable Y
⊢ 0 = integral μ X * integral μ Y
cases' I with I I <;> simp [integral_undef I]
case intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
HX : Integrable X
HY : Integrable Y
⊢ False
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ ¬(Integrable X ∧ Integrable Y)
rintro ⟨HX, HY⟩
no goals
case intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
HX : Integrable X
HY : Integrable Y
⊢ False
exact h (hXY.integrable_mul HX HY)