norm — Mathlib

English

If f and g are identDistrib, then the identically distributed norms are themselves identDistrib.

Русский

Если f и g идентично распределены, то их нормы по отношению к некоторой нормированной группе γ также идентично распределены.

LaTeX

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

Lean4

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

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