norm_charFun_le — Mathlib

English

For any t, the magnitude of the characteristic function is bounded by the total mass of μ: |χ_μ(t)| ≤ μ(E).

Русский

Для любого t модуль χ_μ(t) не превосходит массы всей меры: |χ_μ(t)| ≤ μ(E).

LaTeX

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

Lean4

theorem norm_charFun_le (t : E) : ‖charFun μ t‖ ≤ μ.real Set.univ :=
  by
  rw [charFun_eq_fourierIntegral]
  exact (VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ _ _).trans_eq (by simp)

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