Continuously differentiable functions with compact support

This file develops the basic theory of bundled n-times continuously differentiable functions with compact support contained in some open set Ω. More explicitly, given normed spaces E and F, an open set Ω : Opens E and n : ℕ∞, we are interested in the space 𝓓^{n}(Ω, F) of maps f : E → F such that:

• f is n-times continuously differentiable: ContDiff ℝ n f.
• f has compact support: HasCompactSupport f.
• the support of f is inside the open set Ω: tsupport f ⊆ Ω.

This exists as a bundled type to equip it with the canonical LF topology induced by the inclusions 𝓓_{K}^{n}(Ω, F) → 𝓓^{n}(Ω, F) (see ContDiffMapSupportedIn). The dual space is then the space of distributions, or "weak solutions" to PDEs, on Ω.

Main definitions

• TestFunction Ω F n: the type of bundled n-times continuously differentiable functions E → F with compact support contained in Ω.

Notation

• 𝓓^{n}(Ω, F): the space of bundled n-times continuously differentiable functions E → F with compact support contained in Ω.
• 𝓓(Ω, F): the space of bundled smooth (infinitely differentiable) functions E → F with compact support contained in Ω, i.e. 𝓓^{⊤}(Ω, F).

Tags

distributions, test function

structure TestFunction {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_3) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) : Type (max u_2 u_3)

The type of bundled n-times continuously differentiable maps with compact support

• toFun : E → F

  The underlying function. Use coercion instead.

• contDiff' : ContDiff ℝ (↑n) self.toFun
• hasCompactSupport' : HasCompactSupport self.toFun
• tsupport_subset' : tsupport self.toFun ⊆ ↑Ω

def Distributions.«term𝓓^{_}(_,_)» : Lean.ParserDescr

Notation for the space of bundled n-times continuously differentiable maps with compact support.

Equations

• One or more equations did not get rendered due to their size.

def Distributions.«term𝓓(_,_)» : Lean.ParserDescr

Notation for the space of "test functions", i.e. bundled smooth (infinitely differentiable) maps with compact support.

Equations

• One or more equations did not get rendered due to their size.

class TestFunctionClass (B : Type u_4) {E : outParam (Type u_5)} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : outParam (TopologicalSpace.Opens E)) (F : outParam (Type u_6)) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : outParam ℕ∞) extends DFunLike B E fun (x : E) => F : Type (max (max u_4 u_5) u_6)

TestFunctionClass B Ω F n states that B is a type of n-times continously differentiable functions E → F with compact support contained in Ω : Opens E.

• coe : B → (a : E) → F
• coe_injective' : Function.Injective coe
• map_contDiff (f : B) : ContDiff ℝ ↑n ⇑f
• map_hasCompactSupport (f : B) : HasCompactSupport ⇑f
• tsupport_map_subset (f : B) : tsupport ⇑f ⊆ ↑Ω

instance TestFunctionClass.instContinuousMapClass (B : Type u_4) {E : outParam (Type u_5)} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : outParam (TopologicalSpace.Opens E)) (F : outParam (Type u_6)) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : outParam ℕ∞) [TestFunctionClass B Ω F n] : ContinuousMapClass B E F

instance TestFunctionClass.instBoundedContinuousMapClass (B : Type u_4) {E : outParam (Type u_5)} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : outParam (TopologicalSpace.Opens E)) (F : outParam (Type u_6)) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : outParam ℕ∞) [TestFunctionClass B Ω F n] : BoundedContinuousMapClass B E F

instance TestFunction.toTestFunctionClass {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : TestFunctionClass (TestFunction Ω F n) Ω F n

Equations

• TestFunction.toTestFunctionClass = { coe := fun (f : TestFunction Ω F n) => f.toFun, coe_injective' := ⋯, map_contDiff := ⋯, map_hasCompactSupport := ⋯, tsupport_map_subset := ⋯ }

theorem TestFunction.contDiff {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : ContDiff ℝ ↑n ⇑f

theorem TestFunction.hasCompactSupport {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : HasCompactSupport ⇑f

theorem TestFunction.tsupport_subset {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : tsupport ⇑f ⊆ ↑Ω

@[simp]

theorem TestFunction.toFun_eq_coe {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {f : TestFunction Ω F n} : f.toFun = ⇑f

def TestFunction.Simps.coe {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : E → F

See note [custom simps projection].

Equations

• TestFunction.Simps.coe f = ⇑f

theorem TestFunction.ext {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {f g : TestFunction Ω F n} (h : ∀ (a : E), f a = g a) : f = g

theorem TestFunction.ext_iff {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {f g : TestFunction Ω F n} : f = g ↔ ∀ (a : E), f a = g a

def TestFunction.copy {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) (f' : E → F) (h : f' = ⇑f) : TestFunction Ω F n

Copy of a TestFunction with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toFun := f', contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }

@[simp]

theorem TestFunction.coe_copy {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) (f' : E → F) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem TestFunction.copy_eq {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) (f' : E → F) (h : f' = ⇑f) : f.copy f' h = f

@[simp]

theorem TestFunction.coe_toBoundedContinuousFunction {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : ⇑{ toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } = ⇑f

instance TestFunction.instZero {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : Zero (TestFunction Ω F n)

Equations

• TestFunction.instZero = { zero := { toFun := 0, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ } }

@[simp]

theorem TestFunction.coe_zero {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : ⇑0 = 0

instance TestFunction.instAdd {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : Add (TestFunction Ω F n)

Equations

• TestFunction.instAdd = { add := fun (f g : TestFunction Ω F n) => { toFun := ⇑f + ⇑g, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ } }

@[simp]

theorem TestFunction.coe_add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f g : TestFunction Ω F n) : ⇑(f + g) = ⇑f + ⇑g

instance TestFunction.instNeg {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : Neg (TestFunction Ω F n)

Equations

• TestFunction.instNeg = { neg := fun (f : TestFunction Ω F n) => { toFun := -⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ } }

@[simp]

theorem TestFunction.coe_neg {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : ⇑(-f) = -⇑f

instance TestFunction.instSub {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : Sub (TestFunction Ω F n)

Equations

• TestFunction.instSub = { sub := fun (f g : TestFunction Ω F n) => { toFun := ⇑f - ⇑g, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ } }

@[simp]

theorem TestFunction.coe_sub {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f g : TestFunction Ω F n) : ⇑(f - g) = ⇑f - ⇑g

instance TestFunction.instSMulOfSMulCommClassRealOfContinuousConstSMul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F] : SMul R (TestFunction Ω F n)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TestFunction.coe_smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F] (c : R) (f : TestFunction Ω F n) : ⇑(c • f) = c • ⇑f

instance TestFunction.instAddCommGroup {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} : AddCommGroup (TestFunction Ω F n)

Equations

• One or more equations did not get rendered due to their size.

def TestFunction.coeFnAddMonoidHom {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_3) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) : TestFunction Ω F n →+ E → F

Coercion as an additive homomorphism.

Equations

• TestFunction.coeFnAddMonoidHom Ω F n = { toFun := fun (f : TestFunction Ω F n) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TestFunction.coeFnAddMonoidHom_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_3) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) : ⇑(coeFnAddMonoidHom Ω F n) = fun (f : TestFunction Ω F n) => ⇑f

instance TestFunction.instModuleOfSMulCommClassRealOfContinuousConstSMul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F] : Module R (TestFunction Ω F n)

Equations

• One or more equations did not get rendered due to their size.