prod_apply_le — Mathlib

English

For any measurable set s ⊆ α × β, the product measure μ × ν of s is bounded above by the integral of fiber measures: μ × ν(s) ≤ ∫ ν( Prod.mk x⁻¹' s ) dμ.

Русский

Для любого измеримого множества s ⊆ α × β выполняется неравенство μ × ν(s) ≤ ∫ ν( Prod.mk x⁻¹' s ) dμ.

LaTeX

$$$\mu \mathrm{.prod} \nu (s) \le \int\!\nolimits⁻ x\, \nu(\mathrm{Prod.mk} \, x^{-1}'s) \\partial\mu(x)$ for every measurable set $s$.$$

Lean4

/-- For an s-finite measure `ν`, see `prod_apply` below. -/
theorem prod_apply_le {s : Set (α × β)} (hs : MeasurableSet s) : μ.prod ν s ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ :=
  by
  simp only [Measure.prod, ← map_apply measurable_prodMk_left hs]
  exact bind_apply_le _ hs

Похожие утверждения