setToL1 — Mathlib

English

If h_smul describes T' s = c • T s for all s, then the L1-transfer scales by c.

Русский

Если h_smul задаёт T' s = c • T s, то преобразование L1 масштабируется на c.

LaTeX

$$$setToL1SCLM\;α\;E\;μ\;hT' f = c \cdot setToL1SCLM\;α\;E\;μ\;hT f$$$

Lean4

/-- Extend `Set α → E →L[ℝ] F` to `(α →₁[μ] E) →L[ℝ] F`. -/
def setToL1 (hT : DominatedFinMeasAdditive μ T C) : (α →₁[μ] E) →L[ℝ] F :=
  (setToL1SCLM α E μ hT).extend (coeToLp α E ℝ) (simpleFunc.denseRange one_ne_top) simpleFunc.isUniformInducing

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