English
For any measurable sets s ⊆ α and t ⊆ β, the product measure of their rectangle is at most the product of their measures: μ × ν (s × t) ≤ μ(s) · ν(t). If ν is s-finite, equality holds.
Русский
Для любых измеримых множеств s ⊆ α и t ⊆ β выполняется μ × ν (s × t) ≤ μ(s) · ν(t); при условии s-finite ν равенство выполняется.
LaTeX
$$$\mu( s) \cdot ν(t) \ge μ \mathrm{prod} ν (s \timesˢ t).$$$
Lean4
/-- For any measures `μ` and `ν` and any sets `s` and `t`,
we have `μ.prod ν (s ×ˢ t) ≤ μ s * ν t`.
If `ν` is an s-finite measure (which is usually true),
then this inequality becomes an equality, see `prod_prod` below. -/
theorem prod_prod_le (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) ≤ μ s * ν t :=
by
set S := toMeasurable μ s
set T := toMeasurable ν t
calc
μ.prod ν (s ×ˢ t) ≤ μ.prod ν (S ×ˢ T) := by gcongr <;> apply subset_toMeasurable
_ ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' (S ×ˢ T)) ∂μ := (prod_apply_le (by measurability))
_ = μ S * ν T := by
classical
simp_rw [S, mk_preimage_prod_right_eq_if, measure_if, lintegral_indicator (measurableSet_toMeasurable _ _),
lintegral_const, restrict_apply_univ, mul_comm]
_ = μ s * ν t := by rw [measure_toMeasurable, measure_toMeasurable]
