English
For any sets s ⊆ α and t ⊆ β, the real-valued measure of their product equals the product of their real measures: (μ × ν).real (s × t) = μ.real(s) · ν.real(t).
Русский
Для любых множеств s ⊆ α, t ⊆ β действительная мера произведения равна произведению действительных мер: (μ × ν).real (s × t) = μ.real(s) · ν.real(t).
LaTeX
$$$(\mu \mathrm{.prod} ν).\mathrm{real}(s \timesˢ t) = (μ.real s) \cdot (ν.real t)$$$
Lean4
/-- The product measure of the product of two sets is the product of their measures. Note that we
do not need the sets to be measurable. -/
@[simp]
theorem prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t :=
by
apply (prod_prod_le s t).antisymm
set ST := toMeasurable (μ.prod ν) (s ×ˢ t)
have hSTm : MeasurableSet ST := measurableSet_toMeasurable _ _
have hST : s ×ˢ t ⊆ ST := subset_toMeasurable _ _
set f : α → ℝ≥0∞ := fun x => ν (Prod.mk x ⁻¹' ST)
have hfm : Measurable f := measurable_measure_prodMk_left hSTm
set s' : Set α := {x | ν t ≤ f x}
have hss' : s ⊆ s' := fun x hx => measure_mono fun y hy => hST <| mk_mem_prod hx hy
calc
μ s * ν t ≤ μ s' * ν t := by gcongr
_ = ∫⁻ _ in s', ν t ∂μ := by rw [setLIntegral_const, mul_comm]
_ ≤ ∫⁻ x in s', f x ∂μ := (setLIntegral_mono hfm fun x => id)
_ ≤ ∫⁻ x, f x ∂μ := (lintegral_mono' restrict_le_self le_rfl)
_ = μ.prod ν ST := (prod_apply hSTm).symm
_ = μ.prod ν (s ×ˢ t) := measure_toMeasurable _
