Fourier test expressions used in pressure recovery

@[reducible, inline]

abbrev NavierStokesR3.Comparison.ComplexTest : Type

Complex test: an abbreviation for SchwartzMap Space ℂ.

Equations

• NavierStokesR3.Comparison.ComplexTest = SchwartzMap NavierStokesR3.ProblemStatement.Space ℂ

noncomputable def NavierStokesR3.Comparison.rieszSymbol (i j : Fin 3) (ξ : ProblemStatement.Space) : ℝ

Riesz symbol, given by -(ξ i * ξ j) / ‖ξ‖ ^ 2.

Equations

• NavierStokesR3.Comparison.rieszSymbol i j ξ = -(ξ.ofLp i * ξ.ofLp j) / ‖ξ‖ ^ 2

noncomputable def NavierStokesR3.Comparison.rieszTest (i j : Fin 3) (ψ : ComplexTest) : ProblemStatement.Space → ℂ

Riesz test, given by `FourierTransform.fourierInv (fun ξ : Space => (rieszSymbol i j ξ : ℂ)

• (EulerSobolev.schwartzFourier ψ) ξ)`.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokesR3.Comparison.pressurePair (i j : Fin 3) (g : ProblemStatement.Space → ℝ) (ψ : ComplexTest) : ℂ

Pressure pair, given by ∫ x : Space, (g x : ℂ) * rieszTest i j ψ x.

Equations

• NavierStokesR3.Comparison.pressurePair i j g ψ = ∫ (x : NavierStokesR3.ProblemStatement.Space), ↑(g x) * NavierStokesR3.Comparison.rieszTest i j ψ x

noncomputable def NavierStokesR3.Comparison.fourierHNormSq (s : ℕ) (ψ : ComplexTest) : ℝ

Fourier H norm sq, given by ∫ ξ : Space, (1 + ‖ξ‖ ^ 2) ^ s * ‖(FourierTransform.fourierCLE ℂ ComplexTest ψ) ξ‖ ^ 2.

Equations

• NavierStokesR3.Comparison.fourierHNormSq s ψ = ∫ (ξ : NavierStokesR3.ProblemStatement.Space), (1 + ‖ξ‖ ^ 2) ^ s * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2