setToL1' — Mathlib

English

If T ≤ T' holds pointwise on all s with finite μ, then for f ≤ g we have setToL1SCLM(hT) f ≤ setToL1SCLM(hT') g.

Русский

Если T ≤ T' при любом s с конечной мерой, то для f ≤ g выполняется неравенство преобразований.

LaTeX

$$$\forall f,g\; (f \le g)\Rightarrow setToL1SCLM(hT) f \le setToL1SCLM(hT') g$$$

Lean4

/-- Extend `Set α → (E →L[ℝ] F)` to `(α →₁[μ] E) →L[𝕜] F`. -/
def setToL1' (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) :
    (α →₁[μ] E) →L[𝕜] F :=
  (setToL1SCLM' α E 𝕜 μ hT h_smul).extend (coeToLp α E 𝕜) (simpleFunc.denseRange one_ne_top)
    simpleFunc.isUniformInducing

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