Fourier coefficients of smooth periodic functions and their derivatives.

@[instance_reducible]

noncomputable def avInfraTorusFourierCalculusMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraTorusFourierCalculusMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraTorusFourierCalculusIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.Torus.torusCharacter {d : ℕ} (k : Fin d → ℤ) (x : Homogenization.Vec d) : ℂ

The Euclidean representative of the torus character with frequency k, using the sign convention in mFourierCoeff.

Equations

• AVenhance.Infra.Torus.torusCharacter k x = (UnitAddTorus.mFourier (-k)) (AVenhance.Infra.Torus.toUnitTorus d x)

noncomputable def AVenhance.Infra.Torus.smoothFourierCoeff {d : ℕ} (f : Homogenization.Vec d → ℂ) (k : Fin d → ℤ) : ℂ

The Fourier coefficient of a periodic Euclidean function over its unit cell.

Equations

• AVenhance.Infra.Torus.smoothFourierCoeff f k = ∫ (x : Homogenization.Vec d) in AVenhance.Infra.Torus.unitCell d, AVenhance.Infra.Torus.torusCharacter k x * f x

def AVenhance.Infra.Torus.FourierCalculus.closedCell (d : ℕ) : Set (Homogenization.Vec d)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Torus.FourierCalculus.closedCell d = Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Torus.FourierCalculus.isCompact_closedCell (d : ℕ) : IsCompact (closedCell d)

theorem AVenhance.Infra.Torus.FourierCalculus.unitTorusRepresentative_mem_closedCell {d : ℕ} (x : UnitAddTorus (Fin d)) : unitTorusRepresentative d x ∈ closedCell d

theorem AVenhance.Infra.Torus.measurable_unitTorusRepresentative (d : ℕ) : Measurable (unitTorusRepresentative d)

The canonical torus representative is measurable as a map to Euclidean coordinates.

theorem AVenhance.Infra.Torus.measurable_periodicToTorus {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) : Measurable (periodicToTorus f)

theorem AVenhance.Infra.Torus.memLp_periodicToTorus {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) : MeasureTheory.MemLp (periodicToTorus f) 2 MeasureTheory.volume

A continuous periodic transfer belongs to torus L². Its boundedness follows from continuity on the compact closed unit cell and the canonical representative.

noncomputable def AVenhance.Infra.Torus.periodicToTorusL2 {d : ℕ} (f : Homogenization.Vec d → ℂ) (hf : Continuous f) : ↥(TorusL2 d)

Put a continuous periodic transfer into the torus L² space.

Equations

• AVenhance.Infra.Torus.periodicToTorusL2 f hf = MeasureTheory.MemLp.toLp (AVenhance.Infra.Torus.periodicToTorus f) ⋯

theorem AVenhance.Infra.Torus.continuous_coordDeriv {d : ℕ} (i : Fin d) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ 1 f) : Continuous (coordDeriv i f)

theorem AVenhance.Infra.Torus.torusCharacter_contDiff {d : ℕ} (k : Fin d → ℤ) : ContDiff ℝ ⊤ (torusCharacter k)

theorem AVenhance.Infra.Torus.torusCharacter_periodic {d : ℕ} (k : Fin d → ℤ) : IsZdPeriodic (torusCharacter k)

theorem AVenhance.Infra.Torus.FourierCalculus.periodicToTorusL2_fourierCoeff_eq {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) (k : Fin d → ℤ) : periodicL2FourierCoeff (periodicToTorusL2 f hf) k = smoothFourierCoeff f k

theorem AVenhance.Infra.Torus.FourierCalculus.integral_periodicToTorusL2_normSq_eq {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) : ∫ (y : UnitAddTorus (Fin d)), ‖↑↑(periodicToTorusL2 f hf) y‖ ^ 2 = ∫ (x : Homogenization.Vec d) in unitCell d, ‖f x‖ ^ 2

theorem AVenhance.Infra.Torus.hasSum_sq_smoothFourierCoeff {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) : HasSum (fun (k : Fin d → ℤ) => ‖smoothFourierCoeff f k‖ ^ 2) (∫ (x : Homogenization.Vec d) in unitCell d, ‖f x‖ ^ 2)

Parseval for a continuous periodic Euclidean representative.

theorem AVenhance.Infra.Torus.FourierCalculus.torusCharacter_line_eq {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : torusCharacter k (i.insertNth t z) = (fourier (-k i)) ↑t * ∏ j : Fin n, (fourier (-k (i.succAbove j))) ↑(z j)

theorem AVenhance.Infra.Torus.FourierCalculus.torusCharacter_line_hasDerivAt {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : HasDerivAt (fun (s : ℝ) => torusCharacter k (i.insertNth s z)) (-2 * ↑Real.pi * Complex.I * ↑(k i) * torusCharacter k (i.insertNth t z)) t

theorem AVenhance.Infra.Torus.FourierCalculus.coordDeriv_torusCharacter {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (x : Homogenization.Vec (n + 1)) : coordDeriv i (torusCharacter k) x = -2 * ↑Real.pi * Complex.I * ↑(k i) * torusCharacter k x

theorem AVenhance.Infra.Torus.smoothFourierCoeff_coordDeriv {n : ℕ} (i : Fin (n + 1)) {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) (hpf : IsZdPeriodic f) (k : Fin (n + 1) → ℤ) : smoothFourierCoeff (coordDeriv i f) k = 2 * ↑Real.pi * Complex.I * ↑(k i) * smoothFourierCoeff f k

The Fourier multiplier identity for a coordinate derivative.

theorem AVenhance.Infra.Torus.FourierCalculus.hasSum_finset_sum {ι : Type u_1} {κ : Type u_2} {E : Type u_3} [NormedAddCommGroup E] (s : Finset ι) (F : ι → κ → E) (a : ι → E) (hF : ∀ i ∈ s, HasSum (F i) (a i)) : HasSum (fun (k : κ) => ∑ i ∈ s, F i k) (∑ i ∈ s, a i)

theorem AVenhance.Infra.Torus.hasSum_sq_smoothGradientFourierCoeff {n : ℕ} {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) : HasSum (fun (k : Fin (n + 1) → ℤ) => ∑ i : Fin (n + 1), ‖smoothFourierCoeff (coordDeriv i f) k‖ ^ 2) (∑ i : Fin (n + 1), ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ‖coordDeriv i f x‖ ^ 2)

Parseval for the full coordinate gradient, with the Euclidean cell energy written as the sum of its coordinate energies.

theorem AVenhance.Infra.Torus.FourierCalculus.continuous_integrableOn_closedCell {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : Homogenization.Vec d → E} (hf : Continuous f) : MeasureTheory.IntegrableOn f (closedCell d) MeasureTheory.volume

theorem AVenhance.Infra.Torus.FourierCalculus.cell_integral_coordinate_sum {n : ℕ} {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) : ∑ i : Fin (n + 1), ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ‖coordDeriv i f x‖ ^ 2 = ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ∑ i : Fin (n + 1), ‖coordDeriv i f x‖ ^ 2

theorem AVenhance.Infra.Torus.integral_unitCell_gradSq_eq_sum_coord {n : ℕ} {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) : ∑ i : Fin (n + 1), ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ‖coordDeriv i f x‖ ^ 2 = ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ∑ i : Fin (n + 1), ‖coordDeriv i f x‖ ^ 2

theorem AVenhance.Infra.Torus.FourierCalculus.normSq_fourierMultiplier (m : ℤ) (z : ℂ) : ‖2 * ↑Real.pi * Complex.I * ↑m * z‖ ^ 2 = 4 * Real.pi ^ 2 * ↑m ^ 2 * ‖z‖ ^ 2

theorem AVenhance.Infra.Torus.FourierCalculus.smoothGradientFourierCoeff_eq_frequency {n : ℕ} {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) (hpf : IsZdPeriodic f) (k : Fin (n + 1) → ℤ) : ∑ i : Fin (n + 1), ‖smoothFourierCoeff (coordDeriv i f) k‖ ^ 2 = (4 * Real.pi ^ 2 * ∑ i : Fin (n + 1), ↑(k i) ^ 2) * ‖smoothFourierCoeff f k‖ ^ 2

theorem AVenhance.Infra.Torus.FourierCalculus.intFrequencySq_ge_one {n : ℕ} {k : Fin (n + 1) → ℤ} (hk : k ≠ 0) : 1 ≤ ∑ i : Fin (n + 1), ↑(k i) ^ 2

theorem AVenhance.Infra.Torus.FourierCalculus.smoothFourierCoeff_zero_eq_integral {n : ℕ} (f : Homogenization.Vec (n + 1) → ℂ) : smoothFourierCoeff f 0 = ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), f x

theorem AVenhance.Infra.Torus.meanZero_smoothPeriodic_poincare {n : ℕ} {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) (hpf : IsZdPeriodic f) (hmean : ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), f x = 0) : ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ‖f x‖ ^ 2 ≤ (4 * Real.pi ^ 2)⁻¹ * ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), ∑ i : Fin (n + 1), ‖coordDeriv i f x‖ ^ 2

Mean-zero Poincaré inequality for smooth periodic complex functions on (0,1]^(n+1), with the sharp first nonzero Fourier frequency 2π.