lmarginal_empty — Mathlib

English

If s is empty, then the marginal integral reduces to the original function: for all x, (∫⋯∫⁻_∅ f ∂μ)(x) = f(x).

Русский

Если множество маргинала пусто, то маргинальное интегрирование дает исходную функцию: для всех x выполняется (∫⋯∫⁻_∅ f ∂μ)(x) = f(x).

LaTeX

$$$(\\int⋯∫⁻_\\emptyset f ∂μ)(x) = f(x) \\quad \\text{для всех } x$$$

Lean4

@[simp]
theorem lmarginal_empty (f : (∀ i, X i) → ℝ≥0∞) : ∫⋯∫⁻_∅, f ∂μ = f :=
  by
  ext1 x
  simp_rw [lmarginal, Measure.pi_of_empty fun i : (∅ : Finset δ) => μ i]
  apply lintegral_dirac'
  exact Subsingleton.measurable

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