Fourier coefficients of smooth transport terms as L² pairings.

theorem classicalTransportCoefficientOneLeTwo : Fact (1 ≤ 2)

@[instance_reducible]

noncomputable def classicalTransportCoefficientMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalTransportCoefficientAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalTransportCoefficientProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalTransportCoefficientTorusProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.GalerkinSmoothTransportCoefficient.classicalTransportCoefficientDriftSlice_contDiff (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) : ContDiff ℝ (↑⊤) (streamVel φ t)

theorem AVenhance.Infra.Classical.GalerkinSmoothTransportCoefficient.classicalTransportCoefficientWord_periodic (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarMap_eq_periodicL2 (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (w : List (Fin 2)) : (Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N w) c) = MeasureTheory.MemLp.toLp (Torus.periodicToTorus (classicalWordDerivative w (realFourierModeAmbientExpansion N c))) ⋯

A synthesized word derivative is represented by the corresponding smooth periodic field in the scalar torus L² space.

theorem AVenhance.Infra.Classical.classicalRealPeriodicFourierCoeff_eq_clm (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (hper : IsZ2Periodic f) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus f x)) k = (classicalComplexFourierCoeffCLM k) (MeasureTheory.MemLp.toLp (Torus.periodicToTorus f) ⋯)

The Fourier coefficient of a smooth real periodic field is the coefficient of its complexification in torus L².

theorem AVenhance.Infra.Classical.GalerkinSmoothTransportCoefficient.classicalRealPeriodicFourierIntegrand_integrable (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (hper : IsZ2Periodic f) (k : Fin 2 → ℤ) : MeasureTheory.Integrable (fun (x : Parabolic.FourierGalerkin.Torus) => (UnitAddTorus.mFourier (-k)) x • ↑(Torus.periodicToTorus f x)) MeasureTheory.volume

theorem AVenhance.Infra.Classical.classicalRealPeriodicFourierCoeff_add (f g : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (hg : Continuous g) (hfp : IsZ2Periodic f) (hgp : IsZ2Periodic g) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => f y + g y) x)) k = UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus f x)) k + UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus g x)) k

Fourier coefficients of sums of smooth real periodic fields add.

theorem AVenhance.Infra.Classical.classicalRealPeriodicFourierCoeff_const_mul (a : ℝ) (f : Homogenization.Vec 2 → ℝ) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => a * f y) x)) k = ↑a * UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus f x)) k

Multiplication of a smooth real periodic field by a scalar multiplies its Fourier coefficient by the complexified scalar.

theorem AVenhance.Infra.Classical.classicalRealPeriodicFourierCoeff_sub (f g : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (hg : Continuous g) (hfp : IsZ2Periodic f) (hgp : IsZ2Periodic g) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => f y - g y) x)) k = UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus f x)) k - UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus g x)) k

Fourier coefficients of differences of smooth real periodic fields subtract.

theorem AVenhance.Infra.Classical.classicalGalerkinTransportComponent_fourierCoeff_eq_inner (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (j : Fin 2) (t : ℝ) (u : Homogenization.Vec 2 → ℝ) (hu : ContDiff ℝ (↑⊤) u) (huper : IsZ2Periodic u) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => streamVel φ t y j * spaceGrad u y j) x)) k = inner ℂ (classicalRealToComplexTorusCLM (MeasureTheory.MemLp.toLp (Torus.periodicToTorus (classicalWordDerivative [j] u)) ⋯)) (classicalGalerkinTransportFourierTest φ hφ k j t)

One component of the Fourier coefficient of b · ∇u is the L² pairing of the corresponding gradient with the matching smooth transport test.

theorem AVenhance.Infra.Classical.classicalGalerkinTransport_fourierCoeff_eq_sum_inner (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (t : ℝ) (u : Homogenization.Vec 2 → ℝ) (hu : ContDiff ℝ (↑⊤) u) (huper : IsZ2Periodic u) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (streamVel φ t y) (spaceGrad u y)) x)) k = ∑ j : Fin 2, inner ℂ (classicalRealToComplexTorusCLM (MeasureTheory.MemLp.toLp (Torus.periodicToTorus (classicalWordDerivative [j] u)) ⋯)) (classicalGalerkinTransportFourierTest φ hφ k j t)

The full divergence-free drift term pairs as the sum of its componentwise gradient tests.

theorem AVenhance.Infra.Classical.classicalGalerkinTransport_fourierCoeff_diff_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (t B : ℝ) (hB : 0 ≤ B) (hb : ∀ (s : ℝ) (x : Homogenization.Vec 2), ‖streamVel φ s x‖ ≤ B) (N M : ℕ) (cN : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (cM : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)) : ‖UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (streamVel φ t y) (spaceGrad (realFourierModeAmbientExpansion N cN) y)) x)) k - UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (streamVel φ t y) (spaceGrad (realFourierModeAmbientExpansion M cM) y)) x)) k‖ ≤ ∑ j : Fin 2, B * ‖(Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N [j]) cN) - (Parabolic.FourierGalerkin.realFourierScalarMap M) ((realFourierWordDerivativeMap M [j]) cM)‖

The Fourier coefficient difference of two finite Galerkin transport terms is controlled by the differences of their first derivative paths.