Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ HasFiniteIntegral Y
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ Integrable Y
refine' ⟨hY, _⟩
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
⊢ HasFiniteIntegral Y
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ HasFiniteIntegral Y
have I : (∫⁻ ω, ‖X ω‖₊ ∂μ) ≠ 0 := fun H ↦ by
  have I : (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hX.ennnorm).1 H
  apply h'X
  filter_upwards [I] with ω hω
  simpa using hω
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
⊢ False
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
⊢ HasFiniteIntegral Y
refine lt_top_iff_ne_top.2 fun H => ?_
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
⊢ False
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
⊢ False
have J : IndepFun (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) (fun ω => ‖Y ω‖₊ : Ω → ℝ≥0∞) μ := by
  have M : Measurable fun x : β => (‖x‖₊ : ℝ≥0∞) := measurable_nnnorm.coe_nnreal_ennreal
  apply IndepFun.comp hXY M M
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω * Y ω‖₊ ∂μ) < ⊤
⊢ False
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
⊢ False
have A : (∫⁻ ω, ‖X ω * Y ω‖₊ ∂μ) < ∞ := h'XY.2
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω‖₊ * ↑‖Y ω‖₊ ∂μ) < ⊤
⊢ False
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω * Y ω‖₊ ∂μ) < ⊤
⊢ False
simp only [nnnorm_mul, ENNReal.coe_mul] at A
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) * ⊤ < ⊤
⊢ False
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω‖₊ * ↑‖Y ω‖₊ ∂μ) < ⊤
⊢ False
rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.ennnorm hY.ennnorm J, H] at A
no goals
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) * ⊤ < ⊤
⊢ False
simp only [ENNReal.mul_top I] at A
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
⊢ False
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
⊢ False
have I : (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hX.ennnorm).1 H
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
⊢ X =ᵐ[μ] 0
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
⊢ False
apply h'X
case h
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
ω : Ω
hω : ↑‖X ω‖₊ = OfNat.ofNat 0 ω
⊢ X ω = OfNat.ofNat 0 ω
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
⊢ X =ᵐ[μ] 0
filter_upwards [I] with ω hω
no goals
case h
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
ω : Ω
hω : ↑‖X ω‖₊ = OfNat.ofNat 0 ω
⊢ X ω = OfNat.ofNat 0 ω
simpa using hω
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
M : Measurable fun x => ↑‖x‖₊
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
have M : Measurable fun x : β => (‖x‖₊ : ℝ≥0∞) := measurable_nnnorm.coe_nnreal_ennreal
no goals
Ω : Type u_2
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_1
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) ≠ 0
H : (∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ) = ⊤
M : Measurable fun x => ↑‖x‖₊
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
apply IndepFun.comp hXY M M