norm_setToFun_le_mul_norm — Mathlib

English

For hT dominated, and f integrable, the norm of setToFun is bounded by C times the L1 norm of f, i.e., ≤ C ∥f∥1.

Русский

Для ограниченной SetToFun норма не выше C умножить на норму f в L1.

LaTeX

$$$\\|\\mathrm{setToFun}\\;\\mu\\; T\\; hT\\; f\\| \\le C \\cdot \\|f\\|_{L^1}$$$

Lean4

theorem norm_setToFun_le_mul_norm (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) (hC : 0 ≤ C) :
    ‖setToFun μ T hT f‖ ≤ C * ‖f‖ := by rw [L1.setToFun_eq_setToL1]; exact L1.norm_setToL1_le_mul_norm hT hC f

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