setToL1SCLM_add_left' — Mathlib

English

If T, T', T'' satisfy T'' s = T s + T' s with a_add, then L1-transfer for hT'', on f, equals sum of transfers for hT and hT'.

Русский

Если T'', T и T' удовлетворяют T'' s = T s + T' s, то преобразование L1 на hT'' даёт сумму преобразований для hT и hT'.

LaTeX

$$$setToL1SCLM\;α\;E\;μ\;hT''\;f = setToL1SCLM\;α\;E\;μ\;hT\;f + setToL1SCLM\;α\;E\;μ\;hT'\;f$$$

Lean4

theorem setToL1SCLM_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) : setToL1SCLM α E μ hT'' f = setToL1SCLM α E μ hT f + setToL1SCLM α E μ hT' f :=
  setToL1S_add_left' T T' T'' h_add f

Похожие утверждения