English
Symmetric statement: If the product XY is integrable and X is not zero almost surely, then Y is integrable.
Русский
Симметрично: если XY интегрируемо и X не равна нулю почти где-либо, то Y интегрируема.
LaTeX
$$$\text{IndepFun } X Y μ \land XY \in L^1(μ) \Rightarrow Y \in L^1(μ)$$$
Lean4
/-- If the product of two independent real-valued random variables is integrable and the
first one is not almost everywhere zero, then the second one is integrable. -/
theorem integrable_right_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'X : ¬X =ᵐ[μ] 0) : Integrable Y μ :=
by
refine ⟨hY, ?_⟩
have I : ∫⁻ ω, ‖X ω‖ₑ ∂μ ≠ 0 := fun H ↦
by
have I : ((‖X ·‖ₑ) : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hX.enorm).1 H
apply h'X
filter_upwards [I] with ω hω
simpa using hω
refine lt_top_iff_ne_top.2 fun H => ?_
have J : IndepFun (fun ω => ‖X ω‖ₑ : Ω → ℝ≥0∞) (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) μ :=
IndepFun.comp hXY 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.mul_top I, lt_self_iff_false] at A
