A polynomially weighted Fourier embedding

The weight is constructed by coordinate multiplication on Schwartz space. Consequently the resulting Fourier expressions belong to ordinary L².

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

Multiplication by a real coordinate, acting complex linearly on tests.

Equations

• NavierStokesR3.FourierSobolevWeights.coordinateMul i = SchwartzMap.bilinLeftCLM (ContinuousLinearMap.mul ℂ ℂ) ⋯

@[simp]

theorem NavierStokesR3.FourierSobolevWeights.coordinateMul_apply (i : Fin 3) (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : ((coordinateMul i) ψ) ξ = ↑(ξ.ofLp i) * ψ ξ

noncomputable def NavierStokesR3.FourierSobolevWeights.oneAddNormSqMul : Comparison.ComplexTest →L[ℂ] Comparison.ComplexTest

Multiplication by 1 + ‖ξ‖², preserving Schwartz space.

Equations

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

@[simp]

theorem NavierStokesR3.FourierSobolevWeights.oneAddNormSqMul_apply (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : (oneAddNormSqMul ψ) ξ = ↑(1 + ‖ξ‖ ^ 2) * ψ ξ

noncomputable def NavierStokesR3.FourierSobolevWeights.weightedSchwartz : Comparison.ComplexTest →L[ℂ] Comparison.ComplexTest

Multiplication by the fourth-order Sobolev weight on Schwartz space.

Equations

• NavierStokesR3.FourierSobolevWeights.weightedSchwartz = NavierStokesR3.FourierSobolevWeights.oneAddNormSqMul ∘SL NavierStokesR3.FourierSobolevWeights.oneAddNormSqMul

@[simp]

theorem NavierStokesR3.FourierSobolevWeights.weightedSchwartz_apply (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : (weightedSchwartz ψ) ξ = ↑((1 + ‖ξ‖ ^ 2) ^ 2) * ψ ξ

theorem NavierStokesR3.FourierSobolevWeights.weightedSchwartz_injective : Function.Injective ⇑weightedSchwartz

noncomputable def NavierStokesR3.FourierSobolevWeights.BCLM : Comparison.ComplexTest →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Weighted Fourier embedding of tests into ordinary complex L².

Equations

• NavierStokesR3.FourierSobolevWeights.BCLM = SchwartzMap.toLpCLM ℂ ℂ 2 MeasureTheory.volume ∘SL NavierStokesR3.FourierSobolevWeights.weightedSchwartz ∘SL EulerSobolev.schwartzFourierCLM

noncomputable def NavierStokesR3.FourierSobolevWeights.B : Comparison.ComplexTest →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The linear map underlying the continuous weighted Fourier embedding.

Equations

• NavierStokesR3.FourierSobolevWeights.B = ↑NavierStokesR3.FourierSobolevWeights.BCLM

theorem NavierStokesR3.FourierSobolevWeights.continuous_B : Continuous ⇑B

theorem NavierStokesR3.FourierSobolevWeights.B_ae_eq (ψ : Comparison.ComplexTest) : ↑↑(B ψ) =ᵐ[MeasureTheory.volume] fun (ξ : ProblemStatement.Space) => ↑((1 + ‖ξ‖ ^ 2) ^ 2) * (EulerSobolev.schwartzFourier ψ) ξ

theorem NavierStokesR3.FourierSobolevWeights.B_injective : Function.Injective ⇑B

theorem NavierStokesR3.FourierSobolevWeights.norm_weightedSchwartz_apply_sq (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : ‖(weightedSchwartz ψ) ξ‖ ^ 2 = (1 + ‖ξ‖ ^ 2) ^ 4 * ‖ψ ξ‖ ^ 2

theorem NavierStokesR3.FourierSobolevWeights.integrable_fourierHNormSq_four (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 4 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume

theorem NavierStokesR3.FourierSobolevWeights.fourierHNormSq_three_integrand_le_four (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2 ≤ (1 + ‖ξ‖ ^ 2) ^ 4 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2

theorem NavierStokesR3.FourierSobolevWeights.integrable_fourierHNormSq_three (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume

theorem NavierStokesR3.FourierSobolevWeights.norm_B_eq_sqrt (ψ : Comparison.ComplexTest) : ‖B ψ‖ = √(Comparison.fourierHNormSq 4 ψ)

theorem NavierStokesR3.FourierSobolevWeights.norm_B_sq (ψ : Comparison.ComplexTest) : ‖B ψ‖ ^ 2 = Comparison.fourierHNormSq 4 ψ

theorem NavierStokesR3.FourierSobolevWeights.fourierHNormSq_three_le_norm_B_sq (ψ : Comparison.ComplexTest) : Comparison.fourierHNormSq 3 ψ ≤ ‖B ψ‖ ^ 2

theorem NavierStokesR3.FourierSobolevWeights.sqrt_fourierHNormSq_three_le_norm_B (ψ : Comparison.ComplexTest) : √(Comparison.fourierHNormSq 3 ψ) ≤ ‖B ψ‖

theorem NavierStokesR3.FourierSobolevWeights.inner_B_eq_integral (q : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ψ : Comparison.ComplexTest) : inner ℂ q (B ψ) = ∫ (ξ : ProblemStatement.Space), star (↑↑q ξ) * ↑((1 + ‖ξ‖ ^ 2) ^ 2) * (EulerSobolev.schwartzFourier ψ) ξ