setToFun — Mathlib

English

If hT is dominated, then the operator norm satisfies ||setToL1 hT|| ≤ max{C,0}.

Русский

Если hT доминируется, то ||setToL1 hT|| ≤ max{C,0}.

LaTeX

$$$\|setToL1\, h_T\| ≤ \max\{C,0\}$$$

Lean4

/-- Extend `T : Set α → E →L[ℝ] F` to `(α → E) → F` (for integrable functions `α → E`). We set it to
0 if the function is not integrable. -/
def setToFun (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F :=
  if hf : Integrable f μ then L1.setToL1 hT (hf.toL1 f) else 0

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