nnnorm — Mathlib

English

Similar statement for the nonnegative norm: identDistrib is preserved for nnnorm.

Русский

Аналогично для nn-нормы: identDistrib сохраняется для nnnorm.

LaTeX

$$$\text{IdentDistrib } f g μ ν \Rightarrow \text{IdentDistrib } (\lambda x, \|f x\|_{+}) (\lambda x, \|g x\|_{+}) μ ν$$$

Lean4

protected theorem nnnorm [NormedAddCommGroup γ] [OpensMeasurableSpace γ] (h : IdentDistrib f g μ ν) :
    IdentDistrib (fun x => ‖f x‖₊) (fun x => ‖g x‖₊) μ ν :=
  h.comp measurable_nnnorm

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