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

def IsTestFunction.toCompactlySupportedContinuousMap {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → U} (hf : IsTestFunction f) : CompactlySupportedContinuousMap X U

A compactly supported continuous map from a test function.

Equations

• hf.toCompactlySupportedContinuousMap = { toFun := f, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }

theorem IsTestFunction.of_compactlySupportedContinuousMap {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : CompactlySupportedContinuousMap X U} (hf : ContDiff ℝ ↑⊤ ⇑f) : IsTestFunction f.toFun

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.zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] : IsTestFunction fun (x : X) => 0

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

theorem IsTestFunction.pi {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] {ι : Type u_1} [Fintype ι] {φ : X → ι → U} (hφ : ∀ (i : ι), IsTestFunction fun (x : X) => φ x i) : IsTestFunction fun (x : X) (i : ι) => φ x i

theorem IsTestFunction.space_component {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} {i : Fin d} {φ : X → Space d} (hφ : IsTestFunction φ) : IsTestFunction fun (x : X) => φ x i

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

theorem IsTestFunction.prod_fst {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : X → U × V} (hf : IsTestFunction f) : IsTestFunction fun (x : X) => (f x).1

theorem IsTestFunction.prod_snd {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : X → U × V} (hf : IsTestFunction f) : IsTestFunction fun (x : X) => (f x).2

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.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.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 fun (x : X) => f x - g x

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.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.inner {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_1} [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.inner_left {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {f g : X → V} (hf : ContDiff ℝ (↑⊤) f) (hg : IsTestFunction g) : IsTestFunction fun (x : X) => Inner.inner ℝ (f x) (g x)

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

theorem IsTestFunction.smul {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 : IsTestFunction 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

theorem IsTestFunction.sum {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] {ι : Type u_1} [Fintype ι] {φ : X → ι → U} {hφ : ∀ (i : ι), IsTestFunction fun (x : X) => φ x i} : IsTestFunction fun (x : X) => ∑ i : ι, φ x i

theorem IsTestFunction.coord {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} {φ : X → Space d} (hφ : IsTestFunction φ) (i : Fin d) : IsTestFunction fun (x : X) => Space.coord i (φ x)

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

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

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.of_fderiv {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) => fderiv ℝ f x

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

theorem IsTestFunction.adjFDeriv {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {f : X → U} [InnerProductSpace' ℝ X] [InnerProductSpace' ℝ U] [CompleteSpace X] [CompleteSpace U] (dy : U) (hf : IsTestFunction f) : IsTestFunction fun (x : X) => _root_.adjFDeriv ℝ f x dy

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

theorem IsTestFunction.gradient {d : ℕ} (φ : Space d → ℝ) (hφ : IsTestFunction φ) : IsTestFunction (_root_.gradient φ)

theorem IsTestFunction.of_div {d : ℕ} (φ : Space d → Space d) (hφ : IsTestFunction φ) : IsTestFunction (Space.div φ)