Fourier atoms

This file records the spatial Fourier atom used by the positive-definite and Bochner APIs. It uses Mathlib's 2π Fourier convention.

Main declarations

• TauCeti.fourierAtom: the spatial atom v ↦ exp (-2πi⟪v, q⟫).
• TauCeti.posSemidef_fourierAtom: the subtraction kernel attached to a Fourier atom is positive definite.
• TauCeti.continuous_fourierAtom: Fourier atoms are continuous in the spatial variable.
• TauCeti.norm_fourierAtom: Fourier atoms have unit norm.
• TauCeti.integrable_fourierAtom: Fourier atoms are integrable against a finite measure.
• TauCeti.fourierAtom_zero_left and TauCeti.fourierAtom_zero_right: a Fourier atom is 1 when either argument is 0.

noncomputable def TauCeti.fourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q v : V) : ℂ

The Fourier atom at frequency q, using Mathlib's 2π Fourier convention.

Equations

• TauCeti.fourierAtom q v = ↑(Real.fourierChar (-inner ℝ v q))

theorem TauCeti.fourierAtom_eq_fourierChar {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q v : V) : fourierAtom q v = ↑(Real.fourierChar (-inner ℝ v q))

The Real.fourierChar form of a Fourier atom.

@[simp]

theorem TauCeti.fourierAtom_apply {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q v : V) : fourierAtom q v = Complex.exp (-2 * ↑Real.pi * Complex.I * ↑(inner ℝ v q))

The raw exponential form of a Fourier atom.

theorem TauCeti.fourierAtom_zero_left {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (v : V) : fourierAtom 0 v = 1

A Fourier atom at the zero frequency is 1.

Not a @[simp] lemma: simp already proves it through fourierAtom_apply, and the simpNF linter reports the tagged form as a duplicate.

theorem TauCeti.fourierAtom_zero_right {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q : V) : fourierAtom q 0 = 1

A Fourier atom evaluated at the zero point is 1. Not a @[simp] lemma, for the same reason as fourierAtom_zero_left.

theorem TauCeti.fourierAtom_sub {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q v w : V) : fourierAtom q (v - w) = (starRingEnd ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v q))) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ w q))

Fourier atoms turn spatial subtraction into a rank-one positive-definite kernel.

theorem TauCeti.posSemidef_fourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q : V) : Matrix.PosSemidef fun (v w : V) => fourierAtom q (v - w)

The spatial subtraction kernel supplied by a Fourier atom is positive definite.

theorem TauCeti.norm_fourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q v : V) : ‖fourierAtom q v‖ = 1

Fourier atoms take values on the unit circle.

Not a @[simp] lemma: simp rewrites the atom through fourierAtom_apply first, and the simpNF linter reports the tagged form as unusable for the same reason as fourierAtom_zero_left.

theorem TauCeti.continuous_fourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (q : V) : Continuous (fourierAtom q)

Fourier atoms are continuous in the spatial variable.

theorem TauCeti.integrable_fourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ] (q : V) : MeasureTheory.Integrable (fourierAtom q) μ

A Fourier atom, having unit norm and being continuous, is integrable against a finite measure.