Bounded Riesz symbols and smooth Riesz transforms of test functions

The multiplier is defined at the origin by the ordinary totalized real quotient. Its bound by one gives integrability of every polynomial moment of a multiplied Schwartz transform, hence smoothness and boundedness of its inverse Fourier integral.

theorem NavierStokesR3.RieszTestOperators.norm_rieszSymbol_le (i j : Fin 3) (ξ : ProblemStatement.Space) : ‖Comparison.rieszSymbol i j ξ‖ ≤ 1

theorem NavierStokesR3.RieszTestOperators.abs_rieszSymbol_le (i j : Fin 3) (ξ : ProblemStatement.Space) : |Comparison.rieszSymbol i j ξ| ≤ 1

theorem NavierStokesR3.RieszTestOperators.norm_rieszSymbol_complex_le (i j : Fin 3) (ξ : ProblemStatement.Space) : ‖↑(Comparison.rieszSymbol i j ξ)‖ ≤ 1

theorem NavierStokesR3.RieszTestOperators.measurable_rieszSymbol (i j : Fin 3) : Measurable (Comparison.rieszSymbol i j)

@[simp]

theorem NavierStokesR3.RieszTestOperators.rieszSymbol_neg (i j : Fin 3) (ξ : ProblemStatement.Space) : Comparison.rieszSymbol i j (-ξ) = Comparison.rieszSymbol i j ξ

theorem NavierStokesR3.RieszTestOperators.rieszSymbol_mul_norm_sq (i j : Fin 3) (ξ : ProblemStatement.Space) : Comparison.rieszSymbol i j ξ * ‖ξ‖ ^ 2 = -(ξ.ofLp i * ξ.ofLp j)

theorem NavierStokesR3.RieszTestOperators.measurable_rieszMultiplier (i j : Fin 3) (ψ : Comparison.ComplexTest) : Measurable fun (ξ : ProblemStatement.Space) => ↑(Comparison.rieszSymbol i j ξ) * (EulerSobolev.schwartzFourier ψ) ξ

theorem NavierStokesR3.RieszTestOperators.norm_rieszMultiplier_le (i j : Fin 3) (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : ‖↑(Comparison.rieszSymbol i j ξ) * (EulerSobolev.schwartzFourier ψ) ξ‖ ≤ ‖(EulerSobolev.schwartzFourier ψ) ξ‖

theorem NavierStokesR3.RieszTestOperators.integrable_rieszMultiplier (i j : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => ↑(Comparison.rieszSymbol i j ξ) * (EulerSobolev.schwartzFourier ψ) ξ) MeasureTheory.volume

theorem NavierStokesR3.RieszTestOperators.integrable_pow_mul_norm_rieszMultiplier (i j : Fin 3) (ψ : Comparison.ComplexTest) (n : ℕ) : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => ‖ξ‖ ^ n * ‖↑(Comparison.rieszSymbol i j ξ) * (EulerSobolev.schwartzFourier ψ) ξ‖) MeasureTheory.volume

theorem NavierStokesR3.RieszTestOperators.contDiff_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) : ContDiff ℝ (↑⊤) (Comparison.rieszTest i j ψ)

theorem NavierStokesR3.RieszTestOperators.continuous_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) : Continuous (Comparison.rieszTest i j ψ)

theorem NavierStokesR3.RieszTestOperators.norm_rieszTest_le_integral_multiplier (i j : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ‖Comparison.rieszTest i j ψ x‖ ≤ ∫ (ξ : ProblemStatement.Space), ‖↑(Comparison.rieszSymbol i j ξ) * (EulerSobolev.schwartzFourier ψ) ξ‖

theorem NavierStokesR3.RieszTestOperators.norm_rieszTest_le_integral (i j : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ‖Comparison.rieszTest i j ψ x‖ ≤ ∫ (ξ : ProblemStatement.Space), ‖(EulerSobolev.schwartzFourier ψ) ξ‖

theorem NavierStokesR3.RieszTestOperators.exists_bound_rieszTest (i j : Fin 3) (ψ : Comparison.ComplexTest) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ProblemStatement.Space), ‖Comparison.rieszTest i j ψ x‖ ≤ C