Pairings for the double Riesz transform on test functions

The operator in this file is the inverse Fourier integral from Comparison.rieszTest. Its even, real multiplier gives both the bilinear transpose identity and the Hermitian Fourier pairing. No extension to an operator on all of L² is used.

theorem NavierStokesR3.RieszTestOperators.integrable_rieszTest_mul (i j : Fin 3) (ψ : Comparison.ComplexTest) {f : ProblemStatement.Space → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => Comparison.rieszTest i j ψ x * f x) MeasureTheory.volume

The transformed test can be paired with any integrable complex function.

theorem NavierStokesR3.RieszTestOperators.integrable_mul_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) {f : ProblemStatement.Space → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f x * Comparison.rieszTest i j ψ x) MeasureTheory.volume

The integrable input may also be placed on the left of the pairing.

theorem NavierStokesR3.RieszTestOperators.integrable_rieszTest_mul_conj (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => Comparison.rieszTest i j ψ x * (starRingEnd ℂ) (φ x)) MeasureTheory.volume

The Hermitian pairing with a Schwartz test is integrable.

theorem NavierStokesR3.RieszTestOperators.integral_fourierInv_mul {f g : ProblemStatement.Space → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (x : ProblemStatement.Space), FourierTransformInv.fourierInv f x * g x = ∫ (ξ : ProblemStatement.Space), f ξ * FourierTransform.fourier g (-ξ)

Fourier duality with the inverse Fourier kernel.

theorem NavierStokesR3.RieszTestOperators.fourierInv_conj_apply (f : ProblemStatement.Space → ℂ) (ξ : ProblemStatement.Space) : FourierTransformInv.fourierInv (fun (x : ProblemStatement.Space) => (starRingEnd ℂ) (f x)) ξ = (starRingEnd ℂ) (FourierTransform.fourier f ξ)

Conjugation changes the inverse Fourier kernel into the Fourier kernel.

theorem NavierStokesR3.RieszTestOperators.rieszTest_pairing_fourier (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : ∫ (x : ProblemStatement.Space), Comparison.rieszTest i j ψ x * φ x = ∫ (ξ : ProblemStatement.Space), ↑(Comparison.rieszSymbol i j ξ) * FourierTransform.fourier (⇑ψ) ξ * FourierTransform.fourier (⇑φ) (-ξ)

Pair the actual double Riesz transform with a Schwartz function in Fourier space.

theorem NavierStokesR3.RieszTestOperators.rieszTest_pairing_fourier_conj (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : ∫ (x : ProblemStatement.Space), Comparison.rieszTest i j ψ x * (starRingEnd ℂ) (φ x) = ∫ (ξ : ProblemStatement.Space), ↑(Comparison.rieszSymbol i j ξ) * FourierTransform.fourier (⇑ψ) ξ * (starRingEnd ℂ) (FourierTransform.fourier (⇑φ) ξ)

Hermitian Fourier pairing for the actual double Riesz transform.

theorem NavierStokesR3.RieszTestOperators.rieszTest_selfAdjoint (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : ∫ (x : ProblemStatement.Space), Comparison.rieszTest i j ψ x * φ x = ∫ (x : ProblemStatement.Space), ψ x * Comparison.rieszTest i j φ x

The even Riesz multiplier makes the bilinear pairing symmetric.