Fourier spectral facts for the finite radial cutoff

@[instance_reducible]

noncomputable def avInfraSection5RelativeErrorTraceProjectionSpectrumMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraSection5RelativeErrorTraceProjectionSpectrumMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraSection5RelativeErrorTraceProjectionSpectrumIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.periodicL2FourierCoeff_smooth {f : Homogenization.Vec 2 → ℂ} (hf : Continuous f) (k : Fin 2 → ℤ) : Torus.periodicL2FourierCoeff (Torus.periodicToTorusL2 f hf) k = Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.smoothFourier_inner_hasSum {f g : Homogenization.Vec 2 → ℂ} (hf : Continuous f) (hg : Continuous g) : HasSum (fun (k : Fin 2 → ℤ) => star (Torus.smoothFourierCoeff f k) * Torus.smoothFourierCoeff g k) (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, star (f x) * g x)

def AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.closedUnitCell (d : ℕ) : Set (Homogenization.Vec d)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.closedUnitCell d = Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.continuous_integrableOn_complex_unitCell {f : Homogenization.Vec 2 → ℂ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.smoothFourierCoeff_finsetSum {ι : Type u_1} (s : Finset ι) (f : ι → Homogenization.Vec 2 → ℂ) (hf : ∀ i ∈ s, Continuous (f i)) (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ∑ i ∈ s, f i x) k = ∑ i ∈ s, Torus.smoothFourierCoeff (f i) k

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.smoothFourierCoeff_neg {f : Homogenization.Vec 2 → ℂ} (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => -f x) k = -Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.spaceGrad_component_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 3 f) (i : Fin 2) : ContDiff ℝ 2 fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.negativeSpaceLap_fourierCoeff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 3 f) (hper : IsZ2Periodic f) (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (Torus.realToComplex fun (x : Homogenization.Vec 2) => -spaceLap f x) k = 4 * ↑Real.pi ^ 2 * ↑(∑ i : Fin 2, ↑(k i) ^ 2) * Torus.smoothFourierCoeff (Torus.realToComplex f) k

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

theorem AVenhance.Infra.Section5.RelativeError.TraceProjectionSpectrum.gradientFourierTerm_eq_frequency {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) (k : Fin 2 → ℤ) : ∑ i : Fin 2, ‖Torus.smoothFourierCoeff (Torus.coordDeriv i (Torus.realToComplex f)) k‖ ^ 2 = (4 * Real.pi ^ 2 * ∑ i : Fin 2, ↑(k i) ^ 2) * ‖Torus.smoothFourierCoeff (Torus.realToComplex f) k‖ ^ 2

theorem AVenhance.Infra.Section5.RelativeError.lowProjection_initialPairing_eq_gradientEnergy {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ 3 g) (hper : IsZ2Periodic g) (M : ℕ) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x * -spaceLap (Ergodic.lowProjection g M) x = gradNormSq (spaceGrad (Ergodic.lowProjection g M))

The initial pairing against the negative Laplacian of the radial Fourier cutoff is exactly the squared gradient norm of that cutoff.

theorem AVenhance.Infra.Section5.RelativeError.lowProjection_laplacianGradient_energy_le {g : Homogenization.Vec 2 → ℝ} (M : ℕ) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad (fun (y : Homogenization.Vec 2) => -spaceLap (Ergodic.lowProjection g M) y) x) ≤ (2 * Real.pi * √2 * ↑M) ^ 4 * gradNormSq (spaceGrad (Ergodic.lowProjection g M))

The square cutoff lowProjection g M has Euclidean Fourier support in the ball of radius 2π√2 M. Consequently its differentiated negative Laplacian costs at most the square of that spectral radius.