English
The value of setToSimpleFunc on a piecewise function equals applying T to the corresponding chunk, provided the chunk has finite measure, and the function values are taken from the chunk.
Русский
Значение setToSimpleFunc на разбиении по кускам равно применению T к соответствующему куску, если кусок имеет конечную меру, и значения функции соответствуют этому куску.
LaTeX
$$$ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = T s x $$$
Lean4
theorem setToSimpleFunc_indicator (T : Set α → F →L[ℝ] F') (hT_empty : T ∅ = 0) {m : MeasurableSpace α} {s : Set α}
(hs : MeasurableSet s) (x : F) :
SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0)) = T s x := by
classical
obtain rfl | hs_empty := s.eq_empty_or_nonempty
· simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero, setToSimpleFunc_zero_apply]
simp_rw [setToSimpleFunc]
obtain rfl | hs_univ := eq_or_ne s univ
· haveI hα := hs_empty.to_type
simp [← Function.const_def]
rw [range_indicator hs hs_empty hs_univ]
by_cases hx0 : x = 0
· simp_rw [hx0]; simp
rw [sum_insert]
swap; · rw [Finset.mem_singleton]; exact hx0
rw [sum_singleton, (T _).map_zero, add_zero]
congr
simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero, piecewise_eq_indicator]
rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
swap; · exact Set.mem_singleton x
rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
simp
