norm_one_sub_charFun_le_two — Mathlib

English

For IsProbabilityMeasure μ, the bound |1 − χ_μ(t)| ≤ 2 holds for all t, hence ‖1 − χ_μ(t)‖ ≤ 2.

Русский

Для вероятностной меры μ верно |1 − χ_μ(t)| ≤ 2 для всех t, откуда ‖1 − χ_μ(t)‖ ≤ 2.

LaTeX

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

Lean4

theorem norm_one_sub_charFun_le_two [IsProbabilityMeasure μ] : ‖1 - charFun μ t‖ ≤ 2 :=
  calc
    ‖1 - charFun μ t‖
    _ ≤ ‖(1 : ℂ)‖ + ‖charFun μ t‖ := (norm_sub_le _ _)
    _ ≤ 1 + 1 := by simp [norm_charFun_le_one]
    _ = 2 := by norm_num

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