prod_apply — Mathlib

English

For any measurable s ⊆ α × β, (μ.prod ν)(s) equals the NNReal of the integral ∫⁻ y μ.toMeasure ((fun x ↦ ⟨x, y⟩)⁻¹' s) dν.

Русский

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

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s) = \operatorname{toNNReal}\left(\int^{-} y\, \mu.toMeasure ((\mathrm{fun} x \mapsto \langle x, y \rangle)^{-1} s) \partial \nu\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]

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