Test functions

Definition of test function, smooth and compactly supported function, and theorems about them.

structure IsTestFunction {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] (f : X → U) : Prop

A test function is a smooth function with compact support.

• smooth : ContDiff ℝ (↑⊤) f
• supp : HasCompactSupport f

theorem IsTestFunction.integrable {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [MeasurableSpace X] [OpensMeasurableSpace X] {f : X → U} (hf : IsTestFunction f) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.Integrable f μ

theorem IsTestFunction.differentiable {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → U} (hf : IsTestFunction f) : Differentiable ℝ f

theorem IsTestFunction.contDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → U} (hf : IsTestFunction f) : ContDiff ℝ (↑⊤) f

theorem IsTestFunction.deriv {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : ℝ → U} (hf : IsTestFunction f) : IsTestFunction fun (x : ℝ) => _root_.deriv f x

theorem IsTestFunction.zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] : IsTestFunction fun (x : X) => 0

theorem IsTestFunction.add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f g : X → U} (hf : IsTestFunction f) (hg : IsTestFunction g) : IsTestFunction fun (x : X) => f x + g x

theorem IsTestFunction.neg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → U} (hf : IsTestFunction f) : IsTestFunction fun (x : X) => -f x

theorem IsTestFunction.sub {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f g : X → U} (hf : IsTestFunction f) (hg : IsTestFunction g) : IsTestFunction (f - g)

theorem IsTestFunction.mul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {f g : X → ℝ} (hf : IsTestFunction f) (hg : IsTestFunction g) : IsTestFunction fun (x : X) => f x * g x

theorem IsTestFunction.inner {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {f g : X → V} (hf : IsTestFunction f) (hg : IsTestFunction g) : IsTestFunction fun (x : X) => Inner.inner ℝ (f x) (g x)

theorem IsTestFunction.mul_left {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {f g : X → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : IsTestFunction g) : IsTestFunction fun (x : X) => f x * g x

theorem IsTestFunction.mul_right {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {f g : X → ℝ} (hf : IsTestFunction f) (hg : ContDiff ℝ (↑⊤) g) : IsTestFunction fun (x : X) => f x * g x

theorem IsTestFunction.smul_left {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → ℝ} {g : X → U} (hf : ContDiff ℝ (↑⊤) f) (hg : IsTestFunction g) : IsTestFunction fun (x : X) => f x • g x

theorem IsTestFunction.smul_right {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → ℝ} {g : X → U} (hf : IsTestFunction f) (hg : ContDiff ℝ (↑⊤) g) : IsTestFunction fun (x : X) => f x • g x