norm_charFun_le_one — Mathlib

English

If μ is a probability measure, then the modulus of the characteristic function is bounded by 1: |χ_μ(t)| ≤ 1 for all t.

Русский

Если μ — распределенная по вероятностям мера, то для всех t выполняется |χ_μ(t)| ≤ 1.

LaTeX

$$$$\\|\\chi_{\\mu}(t)\\| \\le 1.$$$$

Lean4

theorem norm_charFun_le_one [IsProbabilityMeasure μ] (t : E) : ‖charFun μ t‖ ≤ 1 :=
  (norm_charFun_le _).trans_eq (by simp)

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