Pointwise identities and estimates for the Fourier monomials

Mathlib's lemmas about fourier n : C(AddCircle T, ℂ) mostly record its behaviour in the index n. This file records the facts about the dependence on the point that translation-invariant Fourier arguments use: the monomial turns a sum of points into a product, differentiating it produces the frequency factor 2πin/T of norm 2π|n|/T, and consequently it is Lipschitz in a real parameter with that constant. Integrating by parts over one period moves this frequency factor across a monomial reparametrized by the lift of a degree-one circle map.

Main statements

• TauCeti.fourier_apply_add: fourier n (x + y) = fourier n x * fourier n y.
• TauCeti.norm_two_pi_I_mul_intCast_div: ‖2πin/T‖ = 2π/T |n| for T > 0.
• TauCeti.norm_fourier_coe_sub_le: ‖e_n φ - e_n ψ‖ ≤ ‖2πin/T‖ |φ - ψ| for real φ, ψ.
• TauCeti.norm_fourier_sub_one_le: ‖e_n h - 1‖ ≤ ‖2πin/T‖ ‖h‖ on the circle, where ‖h‖ is the distance from h to 0.
• TauCeti.one_le_norm_fourier_sub_one: 1 ≤ ‖e_n x - 1‖ for T / (6 |n|) ≤ x ≤ T / (3 |n|).
• TauCeti.integral_fourier_mul_deriv_fourier_comp: for a C¹ lift F with F (x + T) = F x + T, ∫₀ᵀ e_{-n} (e_m ∘ F)' = (2πin/T) ∫₀ᵀ e_{-n} (e_m ∘ F).
• UnitAddTorus.mFourier_apply_add, TauCeti.UnitAddTorus.mFourier_coe_apply and UnitAddTorus.norm_mFourier_apply: the same pointwise facts for the multivariate monomials mFourier n on the torus UnitAddTorus d, whose value at the image of x : d → ℝ is exp (2πi ∑ i, n i * x i).
• TauCeti.UnitAddTorus.contDiff_mFourier_coe and TauCeti.UnitAddTorus.norm_iteratedFDeriv_mFourier_coe_le: this lift of mFourier n is smooth, and its k-th derivative is bounded by (2π ∑ i, |n i|) ^ k.

theorem TauCeti.fourier_apply_add {T : ℝ} (n : ℤ) (x y : AddCircle T) : (fourier n) (x + y) = (fourier n) x * (fourier n) y

A Fourier monomial turns a sum of points into a product: fourier n (x + y) = fourier n x * fourier n y.

theorem TauCeti.norm_two_pi_I_mul_intCast_div {T : ℝ} (hT : 0 < T) (n : ℤ) : ‖2 * ↑Real.pi * Complex.I * ↑n / ↑T‖ = 2 * Real.pi / T * |↑n|

The frequency factor 2πin/T by which differentiation multiplies the Fourier monomial fourier n (hasDerivAt_fourier) has norm 2π/T |n|.

theorem TauCeti.norm_fourier_coe_sub_le {T : ℝ} (n : ℤ) (φ ψ : ℝ) : ‖(fourier n) ↑φ - (fourier n) ↑ψ‖ ≤ ‖2 * ↑Real.pi * Complex.I * ↑n / ↑T‖ * |φ - ψ|

The Fourier monomial x ↦ e^{2πinx/T} is Lipschitz in a real parameter with constant ‖2πin/T‖.

theorem TauCeti.norm_fourier_sub_one_le {T : ℝ} (n : ℤ) (h : AddCircle T) : ‖(fourier n) h - 1‖ ≤ ‖2 * ↑Real.pi * Complex.I * ↑n / ↑T‖ * ‖h‖

The Fourier monomial is Lipschitz on the circle with constant ‖2πin/T‖, measured from 0: ‖e_n h - 1‖ ≤ ‖2πin/T‖ ‖h‖, where ‖h‖ is the distance from h to 0.

theorem TauCeti.one_le_norm_fourier_sub_one {T : ℝ} (hT : 0 < T) {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx₁ : T / (6 * |↑n|) ≤ x) (hx₂ : x ≤ T / (3 * |↑n|)) : 1 ≤ ‖(fourier n) ↑x - 1‖

1 ≤ ‖e_n x - 1‖ for T / (6 |n|) ≤ x ≤ T / (3 |n|), where the half angle π n x / T lies between π / 6 and π / 3 in absolute value.

theorem TauCeti.integral_fourier_mul_deriv_fourier_comp {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hF'c : Continuous F') (m n : ℤ) : ∫ (y : ℝ) in 0..T, (fourier (-n)) ↑y * (↑(F' y) * (2 * ↑Real.pi * Complex.I * ↑m / ↑T * (fourier m) ↑(F y))) = 2 * ↑Real.pi * Complex.I * ↑n / ↑T * ∫ (y : ℝ) in 0..T, (fourier (-n)) ↑y * (fourier m) ↑(F y)

Integration by parts against a reparametrized monomial. For a C¹ lift F with F (x + T) = F x + T, ∫₀ᵀ e_{-n}(y) F'(y) (2πim/T) e_m(F y) dy = (2πin/T) ∫₀ᵀ e_{-n}(y) e_m(F y) dy: the boundary terms of the integration by parts cancel because y ↦ e_{-n}(y) e_m(F y) is T-periodic.

theorem UnitAddTorus.mFourier_apply_add {d : Type u_1} [Fintype d] (n : d → ℤ) (x y : UnitAddTorus d) : (mFourier n) (x + y) = (mFourier n) x * (mFourier n) y

A multivariate Fourier monomial turns a sum of points into a product: mFourier n (x + y) = mFourier n x * mFourier n y.

@[simp]

theorem UnitAddTorus.norm_mFourier_apply {d : Type u_1} [Fintype d] (n : d → ℤ) (z : UnitAddTorus d) : ‖(mFourier n) z‖ = 1

Multivariate Fourier monomials take values in the unit circle.

theorem TauCeti.UnitAddTorus.mFourier_coe_apply {d : Type u_1} [Fintype d] (n : d → ℤ) (x : d → ℝ) : ((UnitAddTorus.mFourier n) fun (i : d) => ↑(x i)) = Complex.exp (2 * ↑Real.pi * Complex.I * ∑ i : d, ↑(n i) * ↑(x i))

The value of the multivariate Fourier monomial mFourier n at the image of x : d → ℝ is exp (2πi ∑ i, n i * x i).

theorem TauCeti.UnitAddTorus.contDiff_mFourier_coe {d : Type u_1} [Fintype d] (n : d → ℤ) : ContDiff ℝ ↑⊤ fun (y : d → ℝ) => (UnitAddTorus.mFourier n) fun (i : d) => ↑(y i)

The lift of the Fourier mode mFourier n to d → ℝ is smooth.

theorem TauCeti.UnitAddTorus.norm_iteratedFDeriv_mFourier_coe_le {d : Type u_1} [Fintype d] (n : d → ℤ) (k : ℕ) (x : d → ℝ) : ‖iteratedFDeriv ℝ k (fun (y : d → ℝ) => (UnitAddTorus.mFourier n) fun (i : d) => ↑(y i)) x‖ ≤ (2 * Real.pi * ∑ i : d, |↑(n i)|) ^ k

The lift of the Fourier mode mFourier n has k-th derivative bounded by (2π ∑ i, |n i|) ^ k.