lmarginal_eq_of_subset — Mathlib

English

If e is injective, and s is a finite set in δ', then a natural equality holds relating marginal over image and pullback along e.

Русский

Если e инъективно отображает δ' в δ и s — конечное множество в δ', существует тождество между маргиналом по изображению и вытяжкой по e.

LaTeX

$$$(\\int⋯∫⁻_{s.image e} (f \\circ (· ∘' e)) ∂μ) x = (\\int⋯∫⁻_s f ∂μ \\circ' e)(x \\circ' e)$$$

Lean4

theorem lmarginal_eq_of_subset {f g : (∀ i, X i) → ℝ≥0∞} (hst : s ⊆ t) (hf : Measurable f) (hg : Measurable g)
    (hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ) : ∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_t, g ∂μ := by
  rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff, lmarginal_union' μ g hg disjoint_sdiff, hfg]

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