English
If μ × ν has zero measure on s, then ν fibers vanish almost everywhere and vice versa under measurability assumptions.
Русский
Если μ × ν имеет ноль на s, то волокна ν почти surely нулевые и наоборот при измеримости.
LaTeX
$$$(μ × ν) s = 0 \Leftrightarrow (fun x => ν(Prod.mk x^{-1} s)) =^{μ}_{μ} 0$$$
Lean4
/-- A measurable set `s` has `μ.prod ν` measure zero, where `ν` is an s-finite measure,
if and only if `μ`-a.e. section `{y | (x, y) ∈ s}` of `s` have `ν` measure zero.
See `measure_ae_null_of_prod_null` for the forward implication without the measurability assumption
and `measure_prod_null_of_ae_null` for the reverse implication without the s-finiteness assumption.
Note: the assumption `hs` cannot be dropped. For a counterexample, see
Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9. -/
theorem measure_prod_null {s : Set (α × β)} (hs : MeasurableSet s) :
μ.prod ν s = 0 ↔ (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0 := by
rw [prod_apply hs, lintegral_eq_zero_iff (measurable_measure_prodMk_left hs)]
