norm_setToFun_le — Mathlib

English

Under a DominatedFinMeasAdditive hypothesis, the L1 norm of setToFun composed with an integrable f is bounded by the L1 norm of f itself scaled by C or a similar bound.

Русский

При условии DominatedFinMeasAdditive неравенство норм SetToFun относительно норм L1 функции f.

LaTeX

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

Lean4

theorem norm_setToFun_le (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hC : 0 ≤ C) :
    ‖setToFun μ T hT f‖ ≤ C * ‖hf.toL1 f‖ := by rw [setToFun_eq hT hf]; exact L1.norm_setToL1_le_mul_norm hT hC _

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