fourier_norm — Mathlib

English

Assume 0 < T. Then every Fourier monomial has unit L2-norm with respect to the normalized Haar measure: ||f_n||_{L^2(haarAddCircle)} = 1.

Русский

Пусть 0 < T. Тогда у всех мономиал Фурье норма в пространстве L^2 по нормализованной мере Хаара равна 1.

LaTeX

$$$\\| f_n \\|_{L^2(haarAddCircle)} = 1 \\quad (n \\in \\mathbb{Z}).$$$

Lean4

theorem fourier_norm [Fact (0 < T)] (n : ℤ) : ‖@fourier T n‖ = 1 :=
  by
  rw [ContinuousMap.norm_eq_iSup_norm]
  have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => Circle.norm_coe _
  simp_rw [this]
  exact ciSup_const

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