-- Mathlib/Probability/Integration.lean
theorem IndepFun.integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β}
    [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (hX : Integrable X μ)
    (hY : Integrable Y μ) : Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
⊢ Integrable (X * Y) μ

Tactic:
let nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
⊢ Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), ‖X a‖ₑ * ‖Y a‖ₑ ∂μ = (∫⁻ (a : Ω), ‖X a‖ₑ ∂μ) * ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ∂μ) * ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ < ⊤

Tactic:
exact ENNReal.mul_lt_top hX.2 hY.2

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
⊢ Integrable (X * Y) μ

Tactic:
have hnX : AEMeasurable nX μ := hX.1.aemeasurable.enorm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
⊢ Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), ‖X a‖ₑ * ‖Y a‖ₑ ∂μ = (∫⁻ (a : Ω), ‖X a‖ₑ ∂μ) * ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ
⊢ HasFiniteIntegral (X * Y) μ

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, Pi.mul_apply, enorm_mul, hmul]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), ‖X a‖ₑ * ‖Y a‖ₑ ∂μ = (∫⁻ (a : Ω), ‖X a‖ₑ ∂μ) * ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ∂μ) * ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
⊢ Integrable (X * Y) μ

Tactic:
have hnY : AEMeasurable nY μ := hY.1.aemeasurable.enorm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
⊢ Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ Integrable (X * Y) μ

Tactic:
refine ⟨hX.1.mul hY.1, ?_⟩

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ HasFiniteIntegral (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
⊢ Integrable (X * Y) μ

Tactic:
let nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
⊢ Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
⊢ Integrable (X * Y) μ

Tactic:
have hXY' : IndepFun nX nY μ := hXY.comp measurable_enorm measurable_enorm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
⊢ Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
⊢ Integrable (X * Y) μ

Tactic:
have hmul : ∫⁻ a, nX a * nY a ∂μ = (∫⁻ a, nX a ∂μ) * ∫⁻ a, nY a ∂μ :=
  lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' hnX hnY hXY'

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ Integrable (X * Y) μ