setToL1_const — Mathlib

English

If μ is finite and hT is dominated, then setToL1 hT on the constant indicator function of the whole space equals T univ acting on x.

Русский

Если μ — конечна и hT доминируется, тогда setToL1 hT на константной функции индикатора всего пространства даёт T(универсум) на x.

LaTeX

$$$setToL1\, h_T\, (\mathbf{1}_{\text{univ}}) = T\,\text{univ}.$$$

Lean4

theorem setToL1_const [IsFiniteMeasure μ] (hT : DominatedFinMeasAdditive μ T C) (x : E) :
    setToL1 hT (indicatorConstLp 1 MeasurableSet.univ (measure_ne_top _ _) x) = T univ x :=
  setToL1_indicatorConstLp hT MeasurableSet.univ (measure_ne_top _ _) x

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