lmarginal_union' — Mathlib

English

If two inputs x and y agree on all coordinates outside s, then lmarginal μ s f evaluated at x equals lmarginal μ s f evaluated at y.

Русский

Если x и y совпадают во всех координатах вне s, то lmarginal μ s f (x) = lmarginal μ s f (y).

LaTeX

$$$\\forall x,y,\\ (\\forall i \\notin s, x_i = y_i) \\Rightarrow (\\mathrm{lmarginal}_{μ} s f)(x) = (\\mathrm{lmarginal}_{μ} s f)(y)$$$

Lean4

theorem lmarginal_union' (f : (∀ i, X i) → ℝ≥0∞) (hf : Measurable f) {s t : Finset δ} (hst : Disjoint s t) :
    ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ := by rw [Finset.union_comm, lmarginal_union μ f hf hst.symm]

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