Linearity and decay of Riesz test operators

The integrable Fourier multipliers defining the test operators respect complex linear combinations. Their inverse Fourier integrals vanish at spatial infinity.

theorem NavierStokesR3.RieszTestOperators.rieszTest_add (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : Comparison.rieszTest i j (ψ + φ) = Comparison.rieszTest i j ψ + Comparison.rieszTest i j φ

theorem NavierStokesR3.RieszTestOperators.rieszTest_smul (i j : Fin 3) (c : ℂ) (ψ : Comparison.ComplexTest) : Comparison.rieszTest i j (c • ψ) = c • Comparison.rieszTest i j ψ

noncomputable def NavierStokesR3.RieszTestOperators.rieszTestLinear (i j : Fin 3) : Comparison.ComplexTest →ₗ[ℂ] ProblemStatement.Space → ℂ

The Riesz test operator as a complex linear map into ordinary functions.

Equations

• NavierStokesR3.RieszTestOperators.rieszTestLinear i j = { toFun := NavierStokesR3.Comparison.rieszTest i j, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NavierStokesR3.RieszTestOperators.rieszTestLinear_apply (i j : Fin 3) (ψ : Comparison.ComplexTest) : (rieszTestLinear i j) ψ = Comparison.rieszTest i j ψ

@[simp]

theorem NavierStokesR3.RieszTestOperators.rieszTest_zero (i j : Fin 3) : Comparison.rieszTest i j 0 = 0

theorem NavierStokesR3.RieszTestOperators.rieszTest_neg (i j : Fin 3) (ψ : Comparison.ComplexTest) : Comparison.rieszTest i j (-ψ) = -Comparison.rieszTest i j ψ

theorem NavierStokesR3.RieszTestOperators.rieszTest_sub (i j : Fin 3) (ψ φ : Comparison.ComplexTest) : Comparison.rieszTest i j (ψ - φ) = Comparison.rieszTest i j ψ - Comparison.rieszTest i j φ

theorem NavierStokesR3.RieszTestOperators.rieszTest_sum (i j : Fin 3) {ι : Type u_1} (s : Finset ι) (ψ : ι → Comparison.ComplexTest) : Comparison.rieszTest i j (∑ a ∈ s, ψ a) = ∑ a ∈ s, Comparison.rieszTest i j (ψ a)

theorem NavierStokesR3.RieszTestOperators.rieszTest_tendsto_zero (i j : Fin 3) (ψ : Comparison.ComplexTest) : Filter.Tendsto (Comparison.rieszTest i j ψ) (Filter.cocompact ProblemStatement.Space) (nhds 0)