setToL1SCLM_mono_left' — Mathlib

English

If μ ≪ μ' and T s = T' s a.e. and for all s, then the left-congruence holds in the L1-transfer.

Русский

Если μ ≪ μ' и T s совпадает с T' s почти всюду, то выполняется левое конгруэнтное равенство в L1-преобразовании.

LaTeX

$$$setToL1SCLM α E μ hT f = setToL1SCLM α E μ' hT' f$$$

Lean4

theorem setToL1SCLM_mono_left' {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x)
    (f : α →₁ₛ[μ] E) : setToL1SCLM α E μ hT f ≤ setToL1SCLM α E μ hT' f :=
  SimpleFunc.setToSimpleFunc_mono_left' T T' hTT' _ (SimpleFunc.integrable f)

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