Compact smooth test functions as Schwartz functions

Compact support is preserved by iterated derivatives. Consequently each polynomially weighted derivative norm is continuous with compact support and is bounded, giving a Schwartz map with the original function as its coercion.

theorem NavierStokesR3.CompactSchwartz.weighted_derivative_bound (f : ProblemStatement.Space → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ProblemStatement.Space), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

Polynomially weighted derivative norms of compact smooth functions are bounded on all of space.

def NavierStokesR3.CompactSchwartz.ofCompactSupport (f : ProblemStatement.Space → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : SchwartzMap ProblemStatement.Space ℂ

A compactly supported smooth function defines a Schwartz function.

Equations

• NavierStokesR3.CompactSchwartz.ofCompactSupport f hf hc = { toFun := f, smooth' := hf, decay' := ⋯ }

@[simp]

theorem NavierStokesR3.CompactSchwartz.coe_ofCompactSupport (f : ProblemStatement.Space → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : ⇑(ofCompactSupport f hf hc) = f

@[simp]

theorem NavierStokesR3.CompactSchwartz.ofCompactSupport_apply (f : ProblemStatement.Space → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (x : ProblemStatement.Space) : (ofCompactSupport f hf hc) x = f x

@[simp]

theorem NavierStokesR3.CompactSchwartz.tsupport_ofCompactSupport (f : ProblemStatement.Space → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : tsupport ⇑(ofCompactSupport f hf hc) = tsupport f

Passing to the Schwartz wrapper preserves topological support exactly.

theorem NavierStokesR3.CompactSchwartz.tsupport_iteratedFDeriv_subset (f : ProblemStatement.Space → ℂ) (n : ℕ) : tsupport (iteratedFDeriv ℝ n f) ⊆ tsupport f

Each iterated derivative remains supported inside the original support.

theorem NavierStokesR3.CompactSchwartz.hasCompactSupport_iteratedFDeriv (f : ProblemStatement.Space → ℂ) (hc : HasCompactSupport f) (n : ℕ) : HasCompactSupport (iteratedFDeriv ℝ n f)

Each iterated derivative of a compactly supported test has compact support.