setLIntegral_piecewise — Mathlib

English

With a fixed t, the restricted lintegral over t for the piecewise kernel equals the corresponding lintegral over t ∩ s with κ or η depending on a.

Русский

При фиксированном t интеграл над t для кусочно-ядра равен соответствующему линегралу над t ∩ s относительно κ или η в зависимости от a.

LaTeX

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

Lean4

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

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