lintegral_swapRight — Mathlib

English

For a measurable g: γ × β → ENNReal, the lintegral with respect to swapRight κ a equals the lintegral of g after precomposing with swap with respect to κ a: ∫ g d(swapRight κ a) = ∫ g ∘ swap d(κ a).

Русский

Для измеримой функции g: γ × β → ENNReal выполняется: лин-интеграл по swapRight κ a равен лин-интегралу g ∘ swap по κ a.

LaTeX

$$$$\\int^- c\\, g(c) \\\\partial (swapRight \\kappa a) = \\int^- (bc) : \\beta \\times \\gamma,\\; g(bc.swap) \\\\partial \\kappa a$$$$

Lean4

theorem lintegral_swapRight (κ : Kernel α (β × γ)) (a : α) {g : γ × β → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂swapRight κ a = ∫⁻ bc : β × γ, g bc.swap ∂κ a := by
  rw [swapRight_eq, lintegral_map _ measurable_swap a hg]

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