English
Conversely, if fiberwise ν fibers are almost everywhere zero with respect to μ, then μ × ν assigns zero to s for measurable s.
Русский
Обратно, если меры ν по волокнам почти всюду нули, то μ × ν придаются нулю на измеримые множества s.
LaTeX
$$$\text{measure_ae_null_of_prod_null}$$$
Lean4
/-- Note: the converse is not true without assuming that `s` is measurable. For a counterexample,
see Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9. -/
theorem measure_ae_null_of_prod_null {s : Set (α × β)} (h : μ.prod ν s = 0) : (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0 :=
by
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
rw [measure_prod_null mt] at ht
rw [eventuallyLE_antisymm_iff]
exact
⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst)) ht,
Eventually.of_forall fun x => zero_le _⟩
