Differential identities for the Riesz test operators

The operators here are the actual inverse Fourier integrals from ComparisonFourierSetup. Differentiation uses their integrable Fourier moments.

The L² bound for Riesz operators on Schwartz tests

The Fourier pairing and Schwartz Parseval imply a dual bound. Testing it against a compact smooth cutoff times the output bounds every truncated energy. Fatou's lemma then proves both square integrability and the global bound, without extending the Fourier transform to arbitrary L² functions.

theorem NavierStokesR3.RieszTestOperators.norm_rieszTest_pairing_le (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : ‖∫ (x : ProblemStatement.Space), Comparison.rieszTest i j ψ x * (starRingEnd ℂ) (φ x)‖ ≤ √(∫ (x : ProblemStatement.Space), ‖ψ x‖ ^ 2) * √(∫ (x : ProblemStatement.Space), ‖φ x‖ ^ 2)

Cauchy--Schwarz and the multiplier bound give the test-function dual estimate.

theorem NavierStokesR3.RieszTestOperators.memLp_two_and_integral_le_of_pairing_bound {f : ProblemStatement.Space → ℂ} (hf : ContDiff ℝ (↑⊤) f) {C : ℝ} (hC : 0 ≤ C) (hpair : ∀ (φ : Comparison.ComplexTest), ‖∫ (x : ProblemStatement.Space), f x * (starRingEnd ℂ) (φ x)‖ ≤ √C * √(∫ (x : ProblemStatement.Space), ‖φ x‖ ^ 2)) : MeasureTheory.MemLp f 2 MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖f x‖ ^ 2 ≤ C

A smooth function satisfying the L² dual estimate on Schwartz tests is square integrable with the corresponding bound.

theorem NavierStokesR3.RieszTestOperators.rieszTest_memLp_and_l2_bound (i j : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.MemLp (Comparison.rieszTest i j ψ) 2 MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖Comparison.rieszTest i j ψ x‖ ^ 2 ≤ ∫ (x : ProblemStatement.Space), ‖ψ x‖ ^ 2

The Riesz test operator is an L² contraction, including square integrability.

theorem NavierStokesR3.RieszTestOperators.memLp_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.MemLp (Comparison.rieszTest i j ψ) 2 MeasureTheory.volume

theorem NavierStokesR3.RieszTestOperators.integral_norm_sq_rieszTest_le (i j : Fin 3) (ψ : Comparison.ComplexTest) : ∫ (x : ProblemStatement.Space), ‖Comparison.rieszTest i j ψ x‖ ^ 2 ≤ ∫ (x : ProblemStatement.Space), ‖ψ x‖ ^ 2

@[reducible, inline]

noncomputable abbrev NavierStokesR3.RieszTestOperators.partialTest (k : Fin 3) (ψ : Comparison.ComplexTest) : Comparison.ComplexTest

A coordinate derivative, retained as a Schwartz function.

Equations

• NavierStokesR3.RieszTestOperators.partialTest k ψ = (LineDeriv.lineDerivOpCLM ℂ NavierStokesR3.Comparison.ComplexTest (NavierStokes.ProblemStatement.coordinateVector k)) ψ

theorem NavierStokesR3.RieszTestOperators.partialTest_apply (k : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : (partialTest k ψ) x = Comparison.partialD k (fun (y : ProblemStatement.Space) => ψ y) x

theorem NavierStokesR3.RieszTestOperators.fourier_pderivTest (ψ : Comparison.ComplexTest) (d ξ : ProblemStatement.Space) : (EulerSobolev.schwartzFourier ((LineDeriv.lineDerivOpCLM ℂ Comparison.ComplexTest d) ψ)) ξ = 2 * ↑Real.pi * Complex.I * ↑(inner ℝ ξ d) * (EulerSobolev.schwartzFourier ψ) ξ

The Fourier transform of a directional derivative of a Schwartz function.

theorem NavierStokesR3.RieszTestOperators.fourier_partialTest (ψ : Comparison.ComplexTest) (k : Fin 3) (ξ : ProblemStatement.Space) : (EulerSobolev.schwartzFourier (partialTest k ψ)) ξ = 2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp k) * (EulerSobolev.schwartzFourier ψ) ξ

theorem NavierStokesR3.RieszTestOperators.fderiv_fourierInv_apply {f : ProblemStatement.Space → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf1 : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => ‖ξ‖ * ‖f ξ‖) MeasureTheory.volume) (x d : ProblemStatement.Space) : (fderiv ℝ (FourierTransformInv.fourierInv f) x) d = FourierTransformInv.fourierInv (fun (ξ : ProblemStatement.Space) => 2 * ↑Real.pi * Complex.I * ↑(inner ℝ ξ d) * f ξ) x

An integrable first Fourier moment permits differentiation of the inverse Fourier integral in every direction.

theorem NavierStokesR3.RieszTestOperators.pderiv_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) (d x : ProblemStatement.Space) : (fderiv ℝ (Comparison.rieszTest i j ψ) x) d = Comparison.rieszTest i j ((LineDeriv.lineDerivOpCLM ℂ Comparison.ComplexTest d) ψ) x

Riesz transforms commute with directional derivatives on Schwartz inputs.

theorem NavierStokesR3.RieszTestOperators.partial_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) (k : Fin 3) (x : ProblemStatement.Space) : Comparison.partialD k (Comparison.rieszTest i j ψ) x = Comparison.rieszTest i j (partialTest k ψ) x

theorem NavierStokesR3.RieszTestOperators.partial_rieszTest_eq (i j : Fin 3) (ψ : Comparison.ComplexTest) (k : Fin 3) : Comparison.partialD k (Comparison.rieszTest i j ψ) = Comparison.rieszTest i j (partialTest k ψ)

theorem NavierStokesR3.RieszTestOperators.memLp_partial_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) (k : Fin 3) : MeasureTheory.MemLp (Comparison.partialD k (Comparison.rieszTest i j ψ)) 2 MeasureTheory.volume

theorem NavierStokesR3.RieszTestOperators.integral_norm_sq_partial_rieszTest_le (i j : Fin 3) (ψ : Comparison.ComplexTest) (k : Fin 3) : ∫ (x : ProblemStatement.Space), ‖Comparison.partialD k (Comparison.rieszTest i j ψ) x‖ ^ 2 ≤ ∫ (x : ProblemStatement.Space), ‖Comparison.partialD k (fun (y : ProblemStatement.Space) => ψ y) x‖ ^ 2

theorem NavierStokesR3.RieszTestOperators.lpNorm_two_partial_rieszTest_le (i j : Fin 3) (ψ : Comparison.ComplexTest) (k : Fin 3) : Comparison.comparisonLpNorm 2 (Comparison.partialD k (Comparison.rieszTest i j ψ)) ≤ Comparison.comparisonLpNorm 2 (Comparison.partialD k fun (y : ProblemStatement.Space) => ψ y)

theorem NavierStokesR3.RieszTestOperators.norm_clm_le_sum_coordinate_norms {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ProblemStatement.Space →L[ℝ] E) : ‖A‖ ≤ ∑ k : Fin 3, ‖A (NavierStokes.ProblemStatement.coordinateVector k)‖

The three coordinate columns control the operator norm of a real-linear map.

theorem NavierStokesR3.RieszTestOperators.memLp_fderiv_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.MemLp (fderiv ℝ (Comparison.rieszTest i j ψ)) 2 MeasureTheory.volume

The complete spatial derivative has a finite L² norm.

theorem NavierStokesR3.RieszTestOperators.lpNorm_two_fderiv_rieszTest_le (i j : Fin 3) (ψ : Comparison.ComplexTest) : Comparison.comparisonLpNorm 2 (fderiv ℝ (Comparison.rieszTest i j ψ)) ≤ 3 * Comparison.comparisonLpNorm 2 (fderiv ℝ fun (y : ProblemStatement.Space) => ψ y)

theorem NavierStokesR3.RieszTestOperators.memLp_rieszTest_six (i j : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.MemLp (Comparison.rieszTest i j ψ) 6 MeasureTheory.volume

theorem NavierStokesR3.RieszTestOperators.lpNorm_six_rieszTest_le (i j : Fin 3) (ψ : Comparison.ComplexTest) : Comparison.comparisonLpNorm 6 (Comparison.rieszTest i j ψ) ≤ 3 * ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst MeasureTheory.volume 2) * Comparison.comparisonLpNorm 2 (fderiv ℝ fun (y : ProblemStatement.Space) => ψ y)

The homogeneous L⁶ estimate needed in the pressure flux. Both the output and its derivative have genuine finite norms by the membership theorems above.

theorem NavierStokesR3.RieszTestOperators.rieszTest_laplacianCLM (i j : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : Comparison.rieszTest i j (HarmonicTestFunctionals.laplacianCLM ψ) x = -((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM j) ψ)) x

Applying the test operator to the ordinary Laplacian recovers the negative mixed derivative. The multiplier identity is valid also at frequency zero.

theorem NavierStokesR3.RieszTestOperators.pressurePair_laplacianCLM (i j : Fin 3) (g : ProblemStatement.Space → ℝ) (ψ : Comparison.ComplexTest) : Comparison.pressurePair i j g (HarmonicTestFunctionals.laplacianCLM ψ) = -∫ (x : ProblemStatement.Space), ↑(g x) * ((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM j) ψ)) x

The canonical pressure functional solves the test-function Poisson equation.

theorem NavierStokesR3.RieszTestOperators.laplacian_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ∑ k : Fin 3, Comparison.partialD k (Comparison.partialD k (Comparison.rieszTest i j ψ)) x = -Comparison.partialD i (Comparison.partialD j fun (y : ProblemStatement.Space) => ψ y) x

The actual smooth Riesz test function satisfies the classical Poisson identity.