English
A variant of the left-additivity: setToSimpleFunc (T+T') f = setToSimpleFunc T f + setToSimpleFunc T' f when h_add holds for all finite μ-s sets.
Русский
Вариант левого сложения: setToSimpleFunc (T+T') f = setToSimpleFunc T f + setToSimpleFunc T' f при условии, что h_add выполняется для всех конечных μ-сетов.
LaTeX
$$$ setToSimpleFunc (T+T') f = setToSimpleFunc T f + setToSimpleFunc T' f $$$
Lean4
theorem setToSimpleFunc_add_left' (T T' T'' : Set α → E →L[ℝ] F)
(h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s) {f : α →ₛ E} (hf : Integrable f μ) :
setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f := by
classical
simp_rw [setToSimpleFunc_eq_sum_filter]
suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' { x }) = T (f ⁻¹' { x }) + T' (f ⁻¹' { x })
by
rw [← sum_add_distrib]
refine Finset.sum_congr rfl fun x hx => ?_
rw [this x hx]
push_cast
rw [Pi.add_apply]
intro x hx
refine h_add (f ⁻¹' { x }) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
rw [mem_filter] at hx
exact hx.2
