prod_apply — Mathlib

English

For every measurable set s ⊆ α × β, the product measure μ.prod ν assigns to s the value given by the outer measure integral: μ.prod ν (s) = toNNReal (∫⁻ x ν.toMeasure (Prod.mk x⁻¹' s) ∂μ).

Русский

Для каждого измеримого множества s ⊆ α × β произведение мер μ.prod ν задаёт величину μ.prod ν (s) равную toNNReal от интеграла ∫⁻ x ν.toMeasure (Prod.mk x⁻¹' s) по μ.

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s) = \operatorname{toNNReal}\left(\int^{-} x\, \nu.toMeasure (\mathrm{Prod.mk}\ x^{-1} s) \, d\mu \right)$$$

Lean4

theorem prod_apply (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ x, ν.toMeasure (Prod.mk x ⁻¹' s) ∂μ) := by
  simp [coeFn_def, Measure.prod_apply s_mble]

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