English
If f is used inside a piecewise construction with a zero tail, the integral over μ equals the integral of f over the restricted measure μ|s.
Русский
Если в конструкции piecewise используется нулевая часть, интеграл по μ равен интегралу по ограниченной мере μ|s.
LaTeX
$$$$ \\big(\\mathrm{piecewise}\\; s\\; hs\\; f\\; 0\\big)_{\\text{integral}}\\; \\mu = f_{\\text{integral}} (\\mu\\restriction s) $$$$
Lean4
@[simp]
theorem integral_piecewise_zero {m : MeasurableSpace α} (f : α →ₛ F) (μ : Measure α) {s : Set α}
(hs : MeasurableSet s) : (piecewise s hs f 0).integral μ = f.integral (μ.restrict s) := by
classical
refine (integral_eq_sum_of_subset ?_).trans ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)
· intro y hy
simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator, mem_range_indicator] at *
rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩
exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]
· dsimp
rw [Set.piecewise_eq_indicator, indicator_preimage_of_notMem,
measureReal_restrict_apply (f.measurableSet_preimage _)]
exact fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)
