norm_setToFun_le' — Mathlib

English

A refined version of norm bound for setToFun with a prime variant, using max(C,0).

Русский

Уточнение неравенства норм для setToFun с модификацией prime.

LaTeX

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

Lean4

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

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