English
For a given T and a simple function f, the value of setToSimpleFunc T f equals the finite sum over the nonzero values of f, where each term uses the preimage of the corresponding value and applies T to that preimage paired with the value.
Русский
Для данного T и простой функции f значение setToSimpleFunc T f раскладывается в конечную сумму по ненулевым значениям f, где каждая слагаемая берется по предобразу соответствующего значения и применяется T к этому предобразу вместе с этим значением.
LaTeX
$$$ setToSimpleFunc T f = \sum_{x \in f.range,\; x \neq 0} T(f^{-1}(\{x\}))\, x$$$
Lean4
theorem setToSimpleFunc_eq_sum_filter [DecidablePred fun x ↦ x ≠ (0 : F)] {m : MeasurableSpace α}
(T : Set α → F →L[ℝ] F') (f : α →ₛ F) : setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, T (f ⁻¹' { x }) x :=
by
symm
refine sum_filter_of_ne fun x _ => mt fun hx0 => ?_
rw [hx0]
exact ContinuousLinearMap.map_zero _
