lintegral_piecewise — Mathlib

English

For a fixed a and a function g, the lintegral over the piecewise kernel equals the appropriate lintegral of either κ or η depending on whether a ∈ s.

Русский

Для фиксированного a и функции g интеграл по кусочно-ядру равен линегралу κ или η в зависимости от принадлежности a s.

LaTeX

$$$\\int^{\\! -}_{b} g(b) \\, d(\\text{piecewise}(hs,\\kappa,\\eta))(a)(b) = \\begin{cases} \\int^{\\! -}_{b} g(b) \\, d\\kappa(a)(b) & a \\in s \\\\ \\int^{\\! -}_{b} g(b) \\, d\\eta(a)(b) & a \\notin s \\end{cases}$$$

Lean4

theorem lintegral_piecewise (a : α) (g : β → ℝ≥0∞) :
    ∫⁻ b, g b ∂piecewise hs κ η a = if a ∈ s then ∫⁻ b, g b ∂κ a else ∫⁻ b, g b ∂η a := by simp_rw [piecewise_apply];
  split_ifs <;> rfl

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