Real sine/cosine modes for symmetric Fourier cutoffs

The integer frequency box is split into the zero frequency and one representative from each pair {k, -k}. Each nonzero representative contributes its real and imaginary character. This module builds the concrete real-valued modes and their smooth periodic ambient representatives.

@[instance_reducible]

noncomputable def realModesMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem realModesMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem realModesProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyPair (p : ℤ × ℤ) : Prop

The lexicographically positive half of the nonzero integer pairs.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyPair p = (0 < p.1 ∨ p.1 = 0 ∧ 0 < p.2)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyRepresentatives (N : ℕ) : Finset (ℤ × ℤ)

One representative from each pair {p,-p} in the symmetric frequency box.

Equations

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

def AVenhance.Infra.Parabolic.FourierGalerkin.frequencyPair (k : Fin 2 → ℤ) : ℤ × ℤ

The unique ordered pair corresponding to a two-coordinate integer frequency.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.frequencyPair k = (k 0, k 1)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.pairFrequency_frequencyPair (k : Fin 2 → ℤ) : pairFrequency (frequencyPair k) = k

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumComplex (N : ℕ) (f : Torus → ℂ) (x : Torus) : ℂ

The complex partial sum applied to a complex-valued function.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.mem_positiveFrequencyRepresentatives {N : ℕ} {p : ℤ × ℤ} (hp : p ∈ positiveFrequencyRepresentatives N) : p ∈ symmetricFrequencyBox N ∧ positiveFrequencyPair p

theorem AVenhance.Infra.Parabolic.FourierGalerkin.symmetricFrequencyBox_subset {M N : ℕ} (hMN : M ≤ N) : symmetricFrequencyBox M ⊆ symmetricFrequencyBox N

A smaller symmetric frequency box is contained in every larger one.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyRepresentatives_subset {M N : ℕ} (hMN : M ≤ N) {p : ℤ × ℤ} (hp : p ∈ positiveFrequencyRepresentatives M) : p ∈ positiveFrequencyRepresentatives N

Positive frequency representatives are preserved by enlarging the cutoff.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyPair_ne_zero {p : ℤ × ℤ} (hp : positiveFrequencyPair p) : p ≠ (0, 0)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyPair_neg_not {p : ℤ × ℤ} (hp : positiveFrequencyPair p) : ¬positiveFrequencyPair (-p)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyRepresentatives_neg_not {N : ℕ} {p : ℤ × ℤ} (hp : p ∈ positiveFrequencyRepresentatives N) : -p ∉ positiveFrequencyRepresentatives N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frequencyBox_partition (N : ℕ) (p : ℤ × ℤ) : p ∈ symmetricFrequencyBox N ↔ p = (0, 0) ∨ p ∈ positiveFrequencyRepresentatives N ∨ -p ∈ positiveFrequencyRepresentatives N