piecewise — Mathlib

English

If f is integrable on s and g is integrable on sᶜ with μ, then the piecewise function s.piecewise f g is integrable with μ.

Русский

Если f интегрируема на s, а g на дополнении к s, то функция piecewise f g интегрируема на всём пространстве по μ.

LaTeX

$$$\text{DecidablePred } \in s \; \Rightarrow \text{MeasurableSet } s \to \mathrm{IntegrableOn}(f,s,\mu) \to \mathrm{IntegrableOn}(g,s^c,\mu) \to \mathrm{Integrable}(s\!\text{piecewise } f g,\mu)$$$

Lean4

theorem piecewise {f g : α → ε'} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) (hf : IntegrableOn f s μ)
    (hg : IntegrableOn g sᶜ μ) : Integrable (s.piecewise f g) μ :=
  by
  rw [IntegrableOn] at hf hg
  rw [← memLp_one_iff_integrable] at hf hg ⊢
  exact MemLp.piecewise hs hf hg

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