English
The setToSimpleFunc translates addition of simple functions: setToSimpleFunc T (f + g) = setToSimpleFunc T f + setToSimpleFunc T g.
Русский
SetToSimpleFunc переносит сложение простых функций: setToSimpleFunc T (f+g) = setToSimpleFunc T f + setToSimpleFunc T g.
LaTeX
$$$ setToSimpleFunc T (f + g) = setToSimpleFunc T f + setToSimpleFunc T g $$$
Lean4
theorem setToSimpleFunc_add (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f g : α →ₛ E} (hf : Integrable f μ)
(hg : Integrable g μ) : setToSimpleFunc T (f + g) = setToSimpleFunc T f + setToSimpleFunc T g :=
have hp_pair : Integrable (f.pair g) μ := integrable_pair hf hg
calc
setToSimpleFunc T (f + g) = ∑ x ∈ (pair f g).range, T (pair f g ⁻¹' { x }) (x.fst + x.snd) := by
rw [add_eq_map₂, map_setToSimpleFunc T h_add hp_pair]; simp
_ = ∑ x ∈ (pair f g).range, (T (pair f g ⁻¹' { x }) x.fst + T (pair f g ⁻¹' { x }) x.snd) :=
(Finset.sum_congr rfl fun _ _ => ContinuousLinearMap.map_add _ _ _)
_ = (∑ x ∈ (pair f g).range, T (pair f g ⁻¹' { x }) x.fst) + ∑ x ∈ (pair f g).range, T (pair f g ⁻¹' { x }) x.snd :=
by rw [Finset.sum_add_distrib]
_ = ((pair f g).map Prod.fst).setToSimpleFunc T + ((pair f g).map Prod.snd).setToSimpleFunc T := by
rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero, map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]
