Lean4
/-- In a topological vector space, the addition of a measurable function and a simple function is
measurable. -/
theorem _root_.Measurable.add_simpleFunc {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E]
[MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable (g + (f : α → E)) := by
classical
induction f using SimpleFunc.induction with
| @const c s
hs =>
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero]
rw [← s.piecewise_same g, ← piecewise_add]
exact Measurable.piecewise hs (hg.add_const _) (hg.add_const _)
| @add f f' hff' hf
hf' =>
have : (g + ↑(f + f')) = (Function.support f).piecewise (g + (f : α → E)) (g + f') :=
by
ext x
by_cases hx : x ∈ Function.support f
·
simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_right_inj, add_eq_left] using Set.disjoint_left.1 hff' hx
·
simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
Set.piecewise_eq_of_notMem _ _ _ hx, _root_.add_right_inj, add_eq_right] using hx
rw [this]
exact Measurable.piecewise f.measurableSet_support hf hf'
