English
If the product of two independent random variables is integrable and the second is not almost surely zero, then the first is integrable.
Русский
Если произведение независимых переменных интегрируемо и вторая величина почти нигде не равна нулю, то первая интегрируема.
LaTeX
$$$\text{IndepFun } X Y μ \Rightarrow \text{Integrable } (XY) μ \Rightarrow \text{Integrable } X μ$$$
Lean4
/-- If the product of two independent real-valued random variables is integrable and
the second one is not almost everywhere zero, then the first one is integrable. -/
theorem integrable_left_of_integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β} [NormedDivisionRing β]
[OpensMeasurableSpace β] (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ) (hX : AEStronglyMeasurable X μ)
(hY : AEStronglyMeasurable Y μ) (h'Y : ¬Y =ᵐ[μ] 0) : Integrable X μ :=
by
refine ⟨hX, ?_⟩
have I : (∫⁻ ω, ‖Y ω‖ₑ ∂μ) ≠ 0 := fun H ↦
by
have I : (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.enorm).1 H
apply h'Y
filter_upwards [I] with ω hω
simpa using hω
refine hasFiniteIntegral_iff_enorm.mpr <| lt_top_iff_ne_top.2 fun H => ?_
have J : IndepFun (‖X ·‖ₑ) (‖Y ·‖ₑ) μ := hXY.comp measurable_enorm measurable_enorm
have A : ∫⁻ ω, ‖X ω * Y ω‖ₑ ∂μ < ∞ := h'XY.2
simp only [enorm_mul] at A
rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.enorm hY.enorm J, H] at A
simp only [ENNReal.top_mul I, lt_self_iff_false] at A
