English
Let T be a family of linear maps on measurable sets such that T(s) = 0 whenever μ(s) < ∞ for all measurable s. Then for any integrable simple function f, the setToSimpleFunc construction yields the zero element in the codomain, i.e., setToSimpleFunc T f = 0.
Русский
Пусть T — семейство линейных отображений, удовлетворяющее условию T(s) = 0 при μ(s) < ∞ для всех измеримых множеств s. Тогда для любой интегрируемой простой функции f оператор setToSimpleFunc возвращает нуль, то есть setToSimpleFunc T f = 0.
LaTeX
$$$\forall \alpha, E, F', T:\ Set\alpha \to L_{\mathbb{R}} E F'\,\Big( \forall s\,(MeasurableSet s)\to(\mu s < \infty) \to T s = 0 \Big) \Big( f : \alpha \to_{s} E \Big) \Big( hf : Integrable f \mu \Big) \;:\; setToSimpleFunc T f = 0$$$
Lean4
theorem setToSimpleFunc_zero' {T : Set α → E →L[ℝ] F'} (h_zero : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0) (f : α →ₛ E)
(hf : Integrable f μ) : setToSimpleFunc T f = 0 :=
by
simp_rw [setToSimpleFunc]
refine sum_eq_zero fun x _ => ?_
by_cases hx0 : x = 0
· simp [hx0]
rw [h_zero (f ⁻¹' ({ x } : Set E)) (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable f hf hx0),
ContinuousLinearMap.zero_apply]
