setToL1SCLM_congr_left' — Mathlib

English

If μ ≪ μ' and T, T' dominate with possibly different measures, then f and f' that are ae-equivalent give equal L1-transforms.

Русский

Если μ приблизительно эквивалентна μ' и T, T' доминируют с возможными разными мерами, то f и f', эквивалентные почти всюду, дают равные преобразования L1.

LaTeX

$$$setToL1SCLM\;\alpha\;E\;\mu\;hT\;f = setToL1SCLM\;\alpha\;E\;\mu'\;hT'\;f'\quad\text{при}\;f =_{{\text{ae}}}\, f'\;\text{и}\;\mu \ll\mu' $$$

Lean4

theorem setToL1SCLM_congr_left' (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
    (h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s) (f : α →₁ₛ[μ] E) :
    setToL1SCLM α E μ hT f = setToL1SCLM α E μ hT' f :=
  setToL1S_congr_left T T' h f

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