Spatial derivatives of Fourier test functions

These operators use the same coordinate vectors and spatial partial derivatives as the equation. Their Fourier identities include the 2π normalization of Mathlib's Fourier transform.

noncomputable def NavierStokesR3.HarmonicTestFunctionals.partialCLM (i : Fin 3) : Comparison.ComplexTest →L[ℂ] Comparison.ComplexTest

Coordinate differentiation on Schwartz tests.

Equations

• NavierStokesR3.HarmonicTestFunctionals.partialCLM i = LineDeriv.lineDerivOpCLM ℂ NavierStokesR3.Comparison.ComplexTest (NavierStokes.ProblemStatement.coordinateVector i)

noncomputable def NavierStokesR3.HarmonicTestFunctionals.laplacianCLM : Comparison.ComplexTest →L[ℂ] Comparison.ComplexTest

The ordinary spatial Laplacian acting on Schwartz tests.

Equations

• NavierStokesR3.HarmonicTestFunctionals.laplacianCLM = ∑ i : Fin 3, NavierStokesR3.HarmonicTestFunctionals.partialCLM i ∘SL NavierStokesR3.HarmonicTestFunctionals.partialCLM i

@[simp]

theorem NavierStokesR3.HarmonicTestFunctionals.partialCLM_apply (i : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ((partialCLM i) ψ) x = NavierStokes.SolutionDifference.spatialPartial i (⇑ψ) x

@[simp]

theorem NavierStokesR3.HarmonicTestFunctionals.laplacianCLM_apply (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : (laplacianCLM ψ) x = ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => NavierStokes.SolutionDifference.spatialPartial i (⇑ψ) y) x

theorem NavierStokesR3.HarmonicTestFunctionals.fourier_partialCLM_apply (i : Fin 3) (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : (EulerSobolev.schwartzFourier ((partialCLM i) ψ)) ξ = 2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp i) * (EulerSobolev.schwartzFourier ψ) ξ

Fourier transform of a coordinate derivative.

theorem NavierStokesR3.HarmonicTestFunctionals.fourier_laplacianCLM_apply (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : (EulerSobolev.schwartzFourier (laplacianCLM ψ)) ξ = -(4 * ↑Real.pi ^ 2) * ↑(‖ξ‖ ^ 2) * (EulerSobolev.schwartzFourier ψ) ξ

The ordinary Laplacian has Fourier multiplier -4π²‖ξ‖².