prod_apply_symm — Mathlib

English

For every measurable set s ⊆ α × β, the product measure μ.prod ν assigns to s the value given by the symmetric integral: μ.prod ν (s) = toNNReal (∫⁻ y μ.toMeasure ((fun x ↦ ⟨x, y⟩)⁻¹' s) ∂ν).

Русский

Для любого измеримого множества s в α × β произведение мер μ.prod ν равно значению toNNReal от интеграла по ν: μ.prod ν (s) = toNNReal (∫⁻ y μ.toMeasure ((fun x ↦ ⟨x, y⟩)⁻¹' s) ∂ν).

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s) = \operatorname{toNNReal}\left(\int^{-} y\, \mu.toMeasure ((\mathrm{fun}\ x \mapsto \langle x, y \rangle)^{-1} s) \, d\nu \right)$$$

Lean4

theorem prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ y, μ.toMeasure ((fun x ↦ ⟨x, y⟩) ⁻¹' s) ∂ν) := by
  simp [coeFn_def, Measure.prod_apply_symm s_mble]

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