lmarginal_univ — Mathlib

English

For an injective map e: δ' → δ, and appropriate s, there is a commuting relation between lmarginal under image and pullback along e.

Русский

Для инъективного отображения e: δ' → δ существует коммутативное соотношение между lmarginal по образу и вытяжкой через e.

LaTeX

$$$(\\int⋯∫⁻_s.image e\, f \\circ (· \\circ' e) ∂μ) x = (\\int⋯∫⁻_s f ∂μ \\circ' e) (x \\circ' e)$$$

Lean4

@[simp]
theorem lmarginal_univ [Fintype δ] {f : (∀ i, X i) → ℝ≥0∞} : ∫⋯∫⁻_univ, f ∂μ = fun _ => ∫⁻ x, f x ∂Measure.pi μ :=
  by
  let e : { j // j ∈ Finset.univ } ≃ δ := Equiv.subtypeUnivEquiv mem_univ
  ext1 x
  simp_rw [lmarginal, measurePreserving_piCongrLeft μ e |>.lintegral_map_equiv, updateFinset_def]
  simp
  rfl

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