setToL1SCLM_congr_measure — Mathlib

English

If T and T' dominate with C, C' and T s = T' s almost everywhere for finite μ, then setToL1SCLM respects this pointwise equality on simple functions.

Русский

Если T и T' доминируют с константами C, C' и T s совпадает почти всюду с T' s для μ с конечной массой, то setToL1SCLM respects это точностепенное равенство на простых функциях.

LaTeX

$$$\forall s\, (\text{MeasurableSet } s),\; μ s < ∞ \Rightarrow T s = T' s \\Rightarrow setToL1SCLM α E μ hT f = setToL1SCLM α E μ hT' f$$$

Lean4

theorem setToL1SCLM_congr_measure {μ' : Measure α} (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ' T C') (hμ : μ ≪ μ') (f : α →₁ₛ[μ] E) (f' : α →₁ₛ[μ'] E)
    (h : (f : α → E) =ᵐ[μ] f') : setToL1SCLM α E μ hT f = setToL1SCLM α E μ' hT' f' :=
  setToL1S_congr_measure T (fun _ => hT.eq_zero_of_measure_zero) hT.1 hμ _ _ h

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