English
The binary product of measures is defined; in particular, it is defined for arbitrary measures with the caveat that at least one factor is s-finite for many properties.
Русский
Две меры образуют произведение; определение действует для произвольных мер при условии, что хотя бы одна из них s-фарнитна для большинства свойств.
LaTeX
$$$\\text{prod}(\\mu, \\nu) = \\mu \\otimes \\nu$ (defined under s-finite conditions).$$
Lean4
/-- If `μ` is an s-finite measure, and `s ⊆ α × β` is measurable, then `y ↦ μ { x | (x, y) ∈ s }` is
a measurable function. -/
theorem measurable_measure_prodMk_right {μ : Measure α} [SFinite μ] {s : Set (α × β)} (hs : MeasurableSet s) :
Measurable fun y => μ ((fun x => (x, y)) ⁻¹' s) :=
measurable_measure_prodMk_left (measurableSet_swap_iff.mpr hs)
