English
The same Fourier integral representation holds with a variant normalization: χ_μ(t) = VectorFourier.fourierIntegral fourierChar μ bilinFormOfRealInner 1 (−(2π)^{-1} t).
Русский
Тот же вид представления через четыреier-интеграл с другой нормализацией: χ_μ(t) = VectorFourier.fourierIntegral fourierChar μ bilinFormOfRealInner 1 (−(2π)^{-1} t).
LaTeX
$$$$\\chi_{\\mu}(t) = \\mathrm{VectorFourier.fourierIntegral}(fourierChar, \\mu, bilinFormOfRealInner, 1, -(2 \\cdot \\pi)^{-1} \\cdot t).$$$$
Lean4
/-- `charFun` is a Fourier integral for the inner product and the character `fourierChar`. -/
theorem charFun_eq_fourierIntegral' (t : E) :
charFun μ t = VectorFourier.fourierIntegral fourierChar μ bilinFormOfRealInner 1 (-(2 * π)⁻¹ • t) :=
by
simp only [charFun_apply, VectorFourier.fourierIntegral, neg_smul, bilinFormOfRealInner_apply_apply, inner_neg_right,
inner_smul_right, neg_neg, fourierChar_apply', Pi.ofNat_apply, Circle.smul_def, Circle.coe_exp, ofReal_mul,
ofReal_ofNat, ofReal_inv, smul_eq_mul, mul_one]
congr with x
rw [← mul_assoc, mul_inv_cancel₀ (by simp [pi_ne_zero]), one_mul]
