English
Various compatibility properties of product measures with respect to maps, measurability, and finite/absolute continuity carry over from the factors to the product.
Русский
Различные свойства произведённых мер в отношении отображений, измеримости и конечности переносятся из факторов в произведение.
LaTeX
$$$\text{prod}$-related equalities and inequalities extend from μ, ν to μ × ν$$
Lean4
/-- If `μ`-a.e. section `{y | (x, y) ∈ s}` of a measurable set have `ν` measure zero,
then `s` has `μ.prod ν` measure zero.
This implication requires `s` to be measurable but does not require `ν` to be s-finite.
See also `measure_prod_null` and `measure_ae_null_of_prod_null` below. -/
theorem measure_prod_null_of_ae_null {s : Set (α × β)} (hsm : MeasurableSet s)
(hs : (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0) : μ.prod ν s = 0 :=
by
rw [← nonpos_iff_eq_zero]
calc
μ.prod ν s ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := prod_apply_le hsm
_ = 0 := by simp [lintegral_congr_ae hs]
