Coefficients of finite real Fourier expansions

The real Fourier coefficient map is a left inverse to finite synthesis for an orthonormal mode family. This gives the coefficient-side part of the Galerkin initial projection bridge.

@[instance_reducible]

noncomputable def projectionMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• projectionMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem projectionMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem projectionProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.modeProjectionCoefficients_modeExpansion {n : ℕ} (mode : Fin n → Torus → ℝ) (horth : ∀ (i j : Fin n), ∫ (x : Torus), mode i x * mode j x = if i = j then 1 else 0) (c : Coefficients n) (hprod : ∀ (i j : Fin n), MeasureTheory.Integrable (fun (x : Torus) => mode i x * mode j x) MeasureTheory.volume) : modeProjectionCoefficients n mode (modeExpansion n mode c) = c

Projecting a finite linear combination onto an orthonormal family recovers its coefficients. The explicit integrability premise keeps this lemma independent of the topology chosen for the mode family.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionCoefficients_expansion (N : ℕ) (c : Coefficients (RealFourierDimension N)) : modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) (modeExpansion (RealFourierDimension N) (realFourierModeFin N) c) = c

In particular the positive real Fourier frame has an exact coefficient reconstruction on its own finite span.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.mFourierCoeff_modeExpansion (n : ℕ) (mode : Fin n → Torus → ℝ) (c : Coefficients n) (l : Fin 2 → ℤ) (hmode : ∀ (i : Fin n), Continuous (mode i)) : UnitAddTorus.mFourierCoeff (fun (x : Torus) => ↑(modeExpansion n mode c x)) l = ∑ i : Fin n, ↑(c.ofLp i) * UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(mode i x)) l

Complex Fourier coefficients commute with finite real-mode synthesis.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierFrameCoefficientContribution (N : ℕ) (c : Coefficients (RealFourierDimension N)) (l : Fin 2 → ℤ) (p : ↥(positiveFrequencyRepresentatives N)) : ℂ

Reindex the Fourier coefficient of a real frame expansion by its constant, cosine, and sine modes.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProjectionCoefficients.realFourierFrameContribution_zero_of_positive_other (N : ℕ) (c : Coefficients (RealFourierDimension N)) (p q : ↥(positiveFrequencyRepresentatives N)) (hpq : q ≠ p) : realFourierFrameCoefficientContribution N c (representativeFrequency p) q = 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProjectionCoefficients.realFourierFrameContribution_zero_of_negative_other (N : ℕ) (c : Coefficients (RealFourierDimension N)) (p q : ↥(positiveFrequencyRepresentatives N)) (hpq : q ≠ p) : realFourierFrameCoefficientContribution N c (-representativeFrequency p) q = 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_mFourierCoeff_expansion (N : ℕ) (c : Coefficients (RealFourierDimension N)) (l : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) c x)) l = (↑(c.ofLp ((realFourierIndexEquivFin N) none)) * if l = 0 then 1 else 0) + ∑ p : ↥(positiveFrequencyRepresentatives N), realFourierFrameCoefficientContribution N c l p

Reindex the Fourier coefficient of a real frame expansion by its constant, cosine, and sine modes.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProjectionCoefficients.integrable_mFourier_mul_of_integrable_real {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (k : Fin 2 → ℤ) : MeasureTheory.Integrable (fun (x : Torus) => (UnitAddTorus.mFourier (-k)) x * ↑(f x)) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_projectionCoefficient_cos (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (p : ↥(positiveFrequencyRepresentatives N)) : ∫ (x : Torus), f x * realFourierMode N (some (p, false)) x = √2 * (UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(f y)) (representativeFrequency p)).re

The cosine coefficient of real data is the real part of its complex Fourier coefficient.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_projectionCoefficient_sin (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (p : ↥(positiveFrequencyRepresentatives N)) : ∫ (x : Torus), f x * realFourierMode N (some (p, true)) x = -√2 * (UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(f y)) (representativeFrequency p)).im

The sine coefficient of real data is minus the imaginary part of its complex Fourier coefficient.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionCoefficient_const (N : ℕ) {f : Torus → ℝ} (_hf : MeasureTheory.Integrable f MeasureTheory.volume) : (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f).ofLp ((realFourierIndexEquivFin N) none) = ∫ (x : Torus), f x

The coefficient assigned to the constant mode is the mean of the initial datum.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionCoefficient_cos (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (p : ↥(positiveFrequencyRepresentatives N)) : (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f).ofLp ((realFourierIndexEquivFin N) (some (p, false))) = √2 * (UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(f y)) (representativeFrequency p)).re

The cosine coefficient assigned by real projection agrees with the real part of the complex Fourier coefficient.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionCoefficient_sin (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (p : ↥(positiveFrequencyRepresentatives N)) : (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f).ofLp ((realFourierIndexEquivFin N) (some (p, true))) = -√2 * (UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(f y)) (representativeFrequency p)).im

The sine coefficient assigned by real projection agrees with minus the imaginary part of the complex Fourier coefficient.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.mFourierCoeff_real_zero_integral {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) 0 = ↑(∫ (x : Torus), f x)

The zero Fourier coefficient of real data is its real integral.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionExpansion_fourierCoeff_zero (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f) x)) 0 = UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) 0

For integrable real data, the real sine/cosine projection has the same Fourier coefficients as the datum throughout its cutoff. This is the finite-dimensional initial trace identity used by the positive-cutoff Galerkin ODE.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionExpansion_fourierCoeff_positive (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (p : ↥(positiveFrequencyRepresentatives N)) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f) x)) (representativeFrequency p) = UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) (representativeFrequency p)

The real sine/cosine projection preserves each positive representative's complex Fourier coefficient.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionExpansion_fourierCoeff_negative (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (p : ↥(positiveFrequencyRepresentatives N)) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f) x)) (-representativeFrequency p) = UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) (-representativeFrequency p)

The real sine/cosine projection preserves the negative-frequency coefficient by conjugation.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionExpansion_fourierCoeff (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (l : Fin 2 → ℤ) (hl : frequencyPair l ∈ symmetricFrequencyBox N) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f) x)) l = UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) l

Every Fourier coefficient in the symmetric cutoff is preserved by the real-mode projection.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionExpansion_eq_projection (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : modeExpansion (RealFourierDimension N) (realFourierModeFin N) (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f) = realFourierProjection N f

The real projection coefficients reconstruct the finite Fourier projection of arbitrary integrable real data. The proof identifies every coefficient in the symmetric cutoff, including both signs of each nonzero frequency.