English
If three dominated finite-measurability linear maps T, T', T'' satisfy T'' = T + T' on all measurable sets of finite μ-measure and if T'' decomposes additively as T and T' on every measurable set, then for every integrable f the L1-set map distributes over the sum: setToL1(hT'') f = setToL1(hT) f + setToL1(hT') f.
Русский
Если три линейных отображения T, T' и T'' удовлетворяют условиям dominated finite-meas additive и для каждой измеримой множества с конечной мерой μ выполняется T'' s = T s + T' s, а f ∈ L1(μ; E) интегрируем, то отображение setToL1 распределяет сложение: setToL1 hT'' f = setToL1 hT f + setToL1 hT' f.
LaTeX
$$$setToL1\, h_T''\, f = setToL1\, h_T\, f + setToL1\, h_T'\, f,$$$
Lean4
theorem setToL1_add_left' (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
(hT'' : DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s)
(f : α →₁[μ] E) : setToL1 hT'' f = setToL1 hT f + setToL1 hT' f :=
by
suffices setToL1 hT'' = setToL1 hT + setToL1 hT' by rw [this, ContinuousLinearMap.add_apply]
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT'') _ _ _ _ ?_
ext1 f
suffices setToL1 hT f + setToL1 hT' f = setToL1SCLM α E μ hT'' f by rw [← this]; simp [coeToLp]
rw [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left' hT hT' hT'' h_add]
