Lemma U: cell coefficients of real Fourier modes

For a periodic function f on the unit cell, cellCoeff M f a = ∫_cell f ψ_a is its coefficient against the real mode ψ_a of the cutoff M. This file records Bessel's inequality in this form, the multiplier identity for gradients of periodic H¹ functions, and the resulting Σ_a λ_a c_a² ≤ ‖Df‖².

@[instance_reducible]

noncomputable def lemmaUMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem lemmaUMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem lemmaUProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem lemmaUProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.FullTheorem.LemmaU.cellCoeff (M : ℕ) (f : Homogenization.Vec 2 → ℝ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : ℝ

The cell coefficient of a function against the real mode a at cutoff M.

Equations

• AVenhance.Infra.FullTheorem.LemmaU.cellCoeff M f a = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, f x * AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient M a x

noncomputable def AVenhance.Infra.FullTheorem.LemmaU.modeLam (M : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : ℝ

The Laplace eigenvalue 4π²|k|² of the real mode a.

Equations

• AVenhance.Infra.FullTheorem.LemmaU.modeLam M a = ∑ i : Fin 2, AVenhance.Infra.Classical.realFourierModeDerivativeScale a i ^ 2

theorem AVenhance.Infra.FullTheorem.LemmaU.modeLam_nonneg (M : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : 0 ≤ modeLam M a

theorem AVenhance.Infra.FullTheorem.LemmaU.modeCoeff_torus (M : ℕ) (f : Homogenization.Vec 2 → ℝ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension M) (Parabolic.FourierGalerkin.realFourierModeFin M) (Torus.periodicToTorus f)).ofLp ((Parabolic.FourierGalerkin.realFourierIndexEquivFin M) a) = cellCoeff M f a

theorem AVenhance.Infra.FullTheorem.LemmaU.cellCoeff_bessel (M : ℕ) {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ∑ a : Parabolic.FourierGalerkin.RealFourierIndex M, cellCoeff M f a ^ 2 ≤ l2NormSq f

Bessel's inequality for the cell coefficients.

theorem AVenhance.Infra.FullTheorem.LemmaU.spaceGrad_mode (M : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (Parabolic.FourierGalerkin.realFourierModeAmbient M a) x i = Classical.realFourierModeDerivativeScale a i * Parabolic.FourierGalerkin.realFourierModeAmbient M (Classical.realFourierModeIndexSwap a) x

theorem AVenhance.Infra.FullTheorem.LemmaU.cellCoeff_grad {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hH : IsPeriodicH1With u Du) (M : ℕ) (i : Fin 2) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : cellCoeff M (fun (x : Homogenization.Vec 2) => Du x i) a = cellCoeff M u (Classical.realFourierModeIndexSwap a) * Classical.realFourierModeDerivativeScale (Classical.realFourierModeIndexSwap a) i

The Fourier multiplier identity for the coefficients of a weak gradient.

theorem AVenhance.Infra.FullTheorem.LemmaU.swap_sum {M : ℕ} (F : Parabolic.FourierGalerkin.RealFourierIndex M → ℝ) : ∑ a : Parabolic.FourierGalerkin.RealFourierIndex M, F (Classical.realFourierModeIndexSwap a) = ∑ a : Parabolic.FourierGalerkin.RealFourierIndex M, F a

theorem AVenhance.Infra.FullTheorem.LemmaU.gradNormSq_eq_sum (Du : Homogenization.Vec 2 → Homogenization.Vec 2) (hD : Homogenization.GradMemL2On unitCube Du) : gradNormSq Du = ∑ i : Fin 2, l2NormSq fun (x : Homogenization.Vec 2) => Du x i

theorem AVenhance.Infra.FullTheorem.LemmaU.modeLam_sum_le {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hH : IsPeriodicH1With u Du) (M : ℕ) : ∑ a : Parabolic.FourierGalerkin.RealFourierIndex M, modeLam M a * cellCoeff M u a ^ 2 ≤ gradNormSq Du

Σ λ_a c_a² ≤ ‖Du‖² for a periodic H¹ function.

theorem AVenhance.Infra.FullTheorem.LemmaU.vecDot_gradMode {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hH : IsPeriodicH1With u Du) (M : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (Du x) (spaceGrad (Parabolic.FourierGalerkin.realFourierModeAmbient M a) x) = modeLam M a * cellCoeff M u a

The diffusion pairing with a mode is the eigenvalue times the coefficient.