Documentation

Mathlib.Analysis.Distribution.TestFunction

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 Ω.
TestFunction.topologicalSpace: the canonical LF topology on 𝓓^{n}(Ω, F). It is the locally convex inductive limit of the topologies on each 𝓓_{K}^{n}(Ω, F).

Main statements #

TestFunction.continuous_iff_continuous_comp: a linear map from 𝓓^{n}(E, F) to a locally convex space is continuous iff its restriction to 𝓓^{n}_{K}(E, F) is continuous for each compact set K. We will later translate this concretely in terms of seminorms.

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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) :

Type (max u_3 u_4)

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 ⊆ ↑Ω

Instances For

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.

Instances For

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.

Instances For

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

Type (max (max u_6 u_7) u_8)

TestFunctionClass B Ω F n states that B is a type of n-times continuously 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 ⊆ ↑Ω

Instances

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

ContinuousMapClass B E F

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

BoundedContinuousMapClass B E F

instance TestFunction.toTestFunctionClass {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) :

ContDiff ℝ ↑n ⇑f

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

HasCompactSupport ⇑f

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

tsupport ⇑f ⊆ ↑Ω

@[simp]

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

f.toFun = ⇑f

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

E → F

See note [custom simps projection].

Equations

TestFunction.Simps.coe f = ⇑f

Instances For

theorem TestFunction.ext {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {f g : TestFunction Ω F n} :

f = g ↔ ∀ (a : E), f a = g a

def TestFunction.copy {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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' := ⋯ }

Instances For

@[simp]

theorem TestFunction.coe_copy {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) :

⇑{ toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } = ⇑f

@[simp]

theorem TestFunction.coe_mk {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {f : E → F} {contDiff : ContDiff ℝ (↑n) f} {hasCompactSupport : HasCompactSupport f} {tsupport_subset : tsupport f ⊆ ↑Ω} :

⇑{ toFun := f, contDiff' := contDiff, hasCompactSupport' := hasCompactSupport, tsupport_subset' := tsupport_subset } = f

instance TestFunction.instZero {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

⇑0 = 0

instance TestFunction.instAdd {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f g : TestFunction Ω F n) :

⇑(f + g) = ⇑f + ⇑g

instance TestFunction.instNeg {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) :

⇑(-f) = -⇑f

instance TestFunction.instSub {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f g : TestFunction Ω F n) :

⇑(f - g) = ⇑f - ⇑g

instance TestFunction.instSMulOfSMulCommClassRealOfContinuousConstSMul {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_6} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_6} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [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_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_4) [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' := ⋯ }

Instances For

@[simp]

theorem TestFunction.coeFnAddMonoidHom_apply {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) :

⇑(coeFnAddMonoidHom Ω F n) = fun (f : TestFunction Ω F n) => ⇑f

instance TestFunction.instModuleOfSMulCommClassRealOfContinuousConstSMul {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_6} [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.

instance TestFunction.instIsScalarTower {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] [Module R F] [Module S F] [SMulCommClass ℝ R F] [SMulCommClass ℝ S F] [ContinuousConstSMul R F] [ContinuousConstSMul S F] [SMul R S] [IsScalarTower R S F] :

IsScalarTower R S (TestFunction Ω F n)

def TestFunction.ofSupportedIn {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) (f : ContDiffMapSupportedIn E F n K) :

TestFunction Ω F n

The natural inclusion 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F) when K ⊆ Ω.

Equations

TestFunction.ofSupportedIn K_sub_Ω f = { toFun := ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }

Instances For

@[simp]

theorem TestFunction.coe_ofSupportedIn {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) (f : ContDiffMapSupportedIn E F n K) :

⇑(ofSupportedIn K_sub_Ω f) = ⇑f

noncomputable def TestFunction.originalTop {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) :

TopologicalSpace (TestFunction Ω F n)

The "original topology" on 𝓓^{n}(Ω, F), defined as the supremum over all compacts K ⊆ Ω of the topology on 𝓓^{n}_{K}(E, F). In other words, this topology makes 𝓓^{n}(Ω, F) the inductive limit of the 𝓓^{n}_{K}(E, F)s in the category of topological spaces.

Note that this has no reason to be a locally convex (or even vector space) topology. For this reason, we actually endow 𝓓^{n}(Ω, F) with another topology, namely the finest locally convex topology which is coarser than this original topology. See TestFunction.topologicalSpace.

Equations

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

Instances For

noncomputable instance TestFunction.topologicalSpace {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) :

TopologicalSpace (TestFunction Ω F n)

The canonical LF topology on 𝓓^{n}(Ω, F). This makes 𝓓^{n}(Ω, F) the inductive limit of the 𝓓^{n}_{K}(E, F)s in the category of locally convex topological vector spaces (over ℝ). See TestFunction.continuous_iff_continuous_comp for the corresponding universal property.

More concretely, this is defined as the infimum of all locally convex topologies which are coarser than the "original topology" TestFunction.originalTop, which corresponds to taking the inductive limit in the category of topological spaces.

Equations

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

instance TestFunction.instIsTopologicalAddGroup {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

IsTopologicalAddGroup (TestFunction Ω F n)

noncomputable instance TestFunction.uniformSpace {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

UniformSpace (TestFunction Ω F n)

Equations

TestFunction.uniformSpace = IsTopologicalAddGroup.rightUniformSpace (TestFunction Ω F n)

instance TestFunction.instIsUniformAddGroup {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

IsUniformAddGroup (TestFunction Ω F n)

instance TestFunction.instContinuousSMulReal {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

ContinuousSMul ℝ (TestFunction Ω F n)

instance TestFunction.instLocallyConvexSpaceReal {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

LocallyConvexSpace ℝ (TestFunction Ω F n)

theorem TestFunction.originalTop_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

originalTop Ω F n ≤ topologicalSpace Ω F n

theorem TestFunction.topologicalSpace_le_iff {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {t : TopologicalSpace (TestFunction Ω F n)} [IsTopologicalAddGroup (TestFunction Ω F n)] [ContinuousSMul ℝ (TestFunction Ω F n)] [LocallyConvexSpace ℝ (TestFunction Ω F n)] :

topologicalSpace Ω F n ≤ t ↔ originalTop Ω F n ≤ t

Fix a locally convex topology t on 𝓓^{n}(Ω, F). t is coarser than the canonical topology on 𝓓^{n}(Ω, F) if and only if it is coarser than the "original topology" given by TestFunction.originalTop.

theorem TestFunction.continuous_ofSupportedIn {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) :

Continuous (ofSupportedIn K_sub_Ω)

For every compact K ⊆ Ω, the inclusion map 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F) is continuous. It is in fact a topological embedding, though this fact is not in Mathlib yet.

def TestFunction.ofSupportedInCLM (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) :

ContDiffMapSupportedIn E F n K →L[𝕜] TestFunction Ω F n

The natural inclusion 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F), when K ⊆ Ω, as a continuous linear map.

Equations

TestFunction.ofSupportedInCLM 𝕜 K_sub_Ω = { toFun := fun (f : ContDiffMapSupportedIn E F n K) => TestFunction.ofSupportedIn K_sub_Ω f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Instances For

@[deprecated TestFunction.ofSupportedInCLM (since := "2025-12-10")]

def TestFunction.ofSupportedInLM (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) :

ContDiffMapSupportedIn E F n K →L[𝕜] TestFunction Ω F n

Alias of TestFunction.ofSupportedInCLM.

The natural inclusion 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F), when K ⊆ Ω, as a continuous linear map.

Equations

TestFunction.ofSupportedInLM = TestFunction.ofSupportedInCLM

Instances For

@[simp]

theorem TestFunction.coe_ofSupportedInCLM {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) :

⇑(ofSupportedInCLM 𝕜 K_sub_Ω) = ofSupportedIn K_sub_Ω

@[deprecated TestFunction.coe_ofSupportedInCLM (since := "2025-12-10")]

theorem TestFunction.coe_ofSupportedInLM {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) :

⇑(ofSupportedInCLM 𝕜 K_sub_Ω) = ofSupportedIn K_sub_Ω

Alias of TestFunction.coe_ofSupportedInCLM.

theorem TestFunction.continuous_iff_continuous_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [AddCommGroup V] [Module ℝ V] [t : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] [Module 𝕜 V] [IsScalarTower ℝ 𝕜 V] (f : TestFunction Ω F n →ₗ[𝕜] V) :

Continuous ⇑f ↔ ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (⇑f ∘ ofSupportedIn K_sub_Ω)

The universal property of the topology on 𝓓^{n}(Ω, F): a linear map from 𝓓^{n}(Ω, F) to a locally convex topological vector space is continuous if and only if its precomposition with the inclusion ofSupportedIn K_sub_Ω : 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F) is continuous for every compact K ⊆ Ω.

def TestFunction.mkCLM (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [AddCommGroup V] [Module ℝ V] [t : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] [Module 𝕜 V] [IsScalarTower ℝ 𝕜 V] (toFun : TestFunction Ω F n → V) (map_add : ∀ (f g : TestFunction Ω F n), toFun (f + g) = toFun f + toFun g) (map_smul : ∀ (c : 𝕜) (f : TestFunction Ω F n), toFun (c • f) = c • toFun f) (cont : ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (toFun ∘ ofSupportedIn K_sub_Ω)) :

TestFunction Ω F n →L[𝕜] V

Reformulation of the universal property of the topology on 𝓓^{n}(Ω, F), in the form of a custom constructor for continuous linear maps 𝓓^{n}(Ω, F) →L[𝕜] V, where V is an arbitrary locally convex topological vector space.

Equations

TestFunction.mkCLM 𝕜 toFun map_add map_smul cont = { toFun := toFun, map_add' := map_add, map_smul' := map_smul, cont := ⋯ }

Instances For

@[simp]

theorem TestFunction.mkCLM_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [AddCommGroup V] [Module ℝ V] [t : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] [Module 𝕜 V] [IsScalarTower ℝ 𝕜 V] (toFun : TestFunction Ω F n → V) (map_add : ∀ (f g : TestFunction Ω F n), toFun (f + g) = toFun f + toFun g) (map_smul : ∀ (c : 𝕜) (f : TestFunction Ω F n), toFun (c • f) = c • toFun f) (cont : ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (toFun ∘ ofSupportedIn K_sub_Ω)) (a✝ : TestFunction Ω F n) :

(TestFunction.mkCLM 𝕜 toFun map_add map_smul cont) a✝ = toFun a✝

noncomputable def TestFunction.toBoundedContinuousFunctionCLM (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] :

TestFunction Ω F n →L[𝕜] BoundedContinuousFunction E F

The inclusion of the space 𝓓^{n}(Ω, F) into the space E →ᵇ F of bounded continuous functions as a continuous 𝕜-linear map.

Equations

TestFunction.toBoundedContinuousFunctionCLM 𝕜 = TestFunction.mkCLM 𝕜 (fun (x : TestFunction Ω F n) => { toFun := ⇑x, continuous_toFun := ⋯, map_bounded' := ⋯ }) ⋯ ⋯ ⋯

Instances For

@[simp]

theorem TestFunction.toBoundedContinuousFunctionCLM_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] (x : TestFunction Ω F n) :

(toBoundedContinuousFunctionCLM 𝕜) x = { toFun := ⇑x, continuous_toFun := ⋯, map_bounded' := ⋯ }

theorem TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] (𝕜' : Type u_6) [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' F] [Algebra ℝ 𝕜'] [IsScalarTower ℝ 𝕜' F] :

⇑(toBoundedContinuousFunctionCLM 𝕜) = ⇑(toBoundedContinuousFunctionCLM 𝕜')

theorem TestFunction.injective_toBoundedContinuousFunctionCLM (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {n : ℕ∞} [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] :

Function.Injective ⇑(toBoundedContinuousFunctionCLM 𝕜)

instance TestFunction.instT3Space {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} :

T3Space (TestFunction Ω F n)

noncomputable def TestFunction.postcompCLM {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {F' : Type u_5} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] {n : ℕ∞} [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 F'] (T : F →L[𝕜] F') :

TestFunction Ω F n →L[𝕜] TestFunction Ω F' n

Given T : F →L[𝕜] F', postcompCLM T is the continuous 𝕜-linear-map sending f : 𝓓^{n}(Ω, F) to T ∘ f as an element of 𝓓^{n}(Ω, F').

Equations

TestFunction.postcompCLM T = TestFunction.mkCLM 𝕜 (fun (f : TestFunction Ω F n) => { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }) ⋯ ⋯ ⋯

Instances For

@[simp]

theorem TestFunction.postcompCLM_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {F' : Type u_5} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] {n : ℕ∞} [Algebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 F'] (T : F →L[𝕜] F') (f : TestFunction Ω F n) :

⇑((postcompCLM T) f) = ⇑T ∘ ⇑f