norm_setToL1_le_mul_norm — Mathlib

English

If hT is dominated and s is measurable with finite μ-measure, then the SetToL1 of indicatorConstLp yields T univ on x.

Русский

Если hT доминируется и s имеет конечную μ-мера, SetToL1(indicatorConstLp) давать T univ на x.

LaTeX

$$$setToL1\, h_T\, (indicatorConstLp\, 1\, s\, μ\, x) = T\, univ\, x,$$$

Lean4

theorem norm_setToL1_le_mul_norm (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) (f : α →₁[μ] E) :
    ‖setToL1 hT f‖ ≤ C * ‖f‖ :=
  calc
    ‖setToL1 hT f‖ ≤ ‖setToL1SCLM α E μ hT‖ * ‖f‖ :=
      ContinuousLinearMap.le_of_opNorm_le _ (norm_setToL1_le_norm_setToL1SCLM hT) _
    _ ≤ C * ‖f‖ := mul_le_mul (norm_setToL1SCLM_le hT hC) le_rfl (norm_nonneg _) hC

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