Continuously differentiable functions supported in a given compact set

This file develops the basic theory of bundled n-times continuously differentiable functions with support contained in a given compact set.

Given n : ℕ∞ and a compact subset K of a normed space E, we consider the type of bundled functions f : E → F (where F is a normed vector space) such that:

• f is n-times continuously differentiable: ContDiff ℝ n f.
• f vanishes outside of a compact set: EqOn f 0 Kᶜ.

The main reason this exists as a bundled type is to be endowed with its natural locally convex topology (namely, uniform convergence of f and its derivative up to order n). Taking the locally convex inductive limit of these as K varies yields the natural topology on test functions, used to define distributions. While most of distribution theory cares only about C^∞ functions, we also want to endow the space of C^n test functions with its natural topology. Indeed, distributions of order less than n are precisely those which extend continuously to this larger space of test functions.

Main definitions

• ContDiffMapSupportedIn E F n K: the type of bundled n-times continuously differentiable functions E → F which vanish outside of K.
• ContDiffMapSupportedIn.iteratedFDerivₗ': wraps iteratedFDeriv into a 𝕜-linear map on ContDiffMapSupportedIn E F n K, as a map into ContDiffMapSupportedIn E (E [×i]→L[ℝ] F) (n-i) K.

Main statements

TODO:

• ContDiffMapSupportedIn.instIsUniformAddGroup and ContDiffMapSupportedIn.instLocallyConvexSpace: ContDiffMapSupportedIn is a locally convex topological vector space.

Notation

• 𝓓^{n}_{K}(E, F): the space of n-times continuously differentiable functions E → F which vanish outside of K.
• 𝓓_{K}(E, F): the space of smooth (infinitely differentiable) functions E → F which vanish outside of K, i.e. 𝓓^{⊤}_{K}(E, F).

Implementation details

The technical choice of spelling EqOn f 0 Kᶜ in the definition, as opposed to tsupport f ⊆ K is to make rewriting f x to 0 easier when x ∉ K.

Tags

distributions

structure ContDiffMapSupportedIn (E : Type u_2) (F : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) (K : TopologicalSpace.Compacts E) : Type (max u_2 u_3)

The type of bundled n-times continuously differentiable maps which vanish outside of a fixed compact set K.

• toFun : E → F

  The underlying function. Use coercion instead.

• contDiff' : ContDiff ℝ (↑n) self.toFun
• zero_on_compl' : Set.EqOn self.toFun 0 (↑K)ᶜ

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

Notation for the space of bundled n-times continuously differentiable functions with support in a compact set K.

Equations

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

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

Notation for the space of bundled smooth (inifinitely differentiable) functions with support in a compact set K.

Equations

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

class ContDiffMapSupportedInClass (B : Type u_4) (E : outParam (Type u_5)) (F : outParam (Type u_6)) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (n : outParam ℕ∞) (K : outParam (TopologicalSpace.Compacts E)) extends DFunLike B E fun (x : E) => F : Type (max (max u_4 u_5) u_6)

ContDiffMapSupportedInClass B E F n K states that B is a type of bundled n-times continously differentiable functions with support in the compact set K.

• coe : B → (a : E) → F
• coe_injective' : Function.Injective coe
• map_contDiff (f : B) : ContDiff ℝ ↑n ⇑f
• map_zero_on_compl (f : B) : Set.EqOn (⇑f) 0 (↑K)ᶜ

instance instContinuousMapClass (B : Type u_4) (E : outParam (Type u_5)) (F : outParam (Type u_6)) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (n : outParam ℕ∞) (K : outParam (TopologicalSpace.Compacts E)) [ContDiffMapSupportedInClass B E F n K] : ContinuousMapClass B E F

instance instBoundedContinuousMapClass (B : Type u_4) (E : outParam (Type u_5)) (F : outParam (Type u_6)) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (n : outParam ℕ∞) (K : outParam (TopologicalSpace.Compacts E)) [ContDiffMapSupportedInClass B E F n K] : BoundedContinuousMapClass B E F

instance ContDiffMapSupportedIn.toContDiffMapSupportedInClass (E : Type u_2) (F : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : ContDiffMapSupportedInClass (ContDiffMapSupportedIn E F n K) E F n K

Equations

• ContDiffMapSupportedIn.toContDiffMapSupportedInClass E F = { coe := fun (f : ContDiffMapSupportedIn E F n K) => f.toFun, coe_injective' := ⋯, map_contDiff := ⋯, map_zero_on_compl := ⋯ }

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

theorem ContDiffMapSupportedIn.zero_on_compl {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) : Set.EqOn (⇑f) 0 (↑K)ᶜ

theorem ContDiffMapSupportedIn.compact_supp {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) : HasCompactSupport ⇑f

@[simp]

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

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

See note [custom simps projection].

Equations

• ContDiffMapSupportedIn.Simps.coe f = ⇑f

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

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

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

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

Equations

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

@[simp]

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

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

@[simp]

theorem ContDiffMapSupportedIn.toBoundedContinuousFunction_apply {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) (x : E) : { toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } x = f x

instance ContDiffMapSupportedIn.instZero {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : Zero (ContDiffMapSupportedIn E F n K)

Equations

• ContDiffMapSupportedIn.instZero = { zero := { toFun := 0, contDiff' := ⋯, zero_on_compl' := ⋯ } }

@[simp]

theorem ContDiffMapSupportedIn.coe_zero {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : ⇑0 = 0

instance ContDiffMapSupportedIn.instAdd {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : Add (ContDiffMapSupportedIn E F n K)

Equations

• ContDiffMapSupportedIn.instAdd = { add := fun (f g : ContDiffMapSupportedIn E F n K) => { toFun := ⇑f + ⇑g, contDiff' := ⋯, zero_on_compl' := ⋯ } }

@[simp]

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

instance ContDiffMapSupportedIn.instNeg {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : Neg (ContDiffMapSupportedIn E F n K)

Equations

• ContDiffMapSupportedIn.instNeg = { neg := fun (f : ContDiffMapSupportedIn E F n K) => { toFun := -⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ } }

@[simp]

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

instance ContDiffMapSupportedIn.instSub {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : Sub (ContDiffMapSupportedIn E F n K)

Equations

• ContDiffMapSupportedIn.instSub = { sub := fun (f g : ContDiffMapSupportedIn E F n K) => { toFun := ⇑f - ⇑g, contDiff' := ⋯, zero_on_compl' := ⋯ } }

@[simp]

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

instance ContDiffMapSupportedIn.instSMul {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F] : SMul R (ContDiffMapSupportedIn E F n K)

Equations

• ContDiffMapSupportedIn.instSMul = { smul := fun (c : R) (f : ContDiffMapSupportedIn E F n K) => { toFun := c • ⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ } }

@[simp]

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

instance ContDiffMapSupportedIn.instAddCommGroup {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} : AddCommGroup (ContDiffMapSupportedIn E F n K)

Equations

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

def ContDiffMapSupportedIn.coeHom (E : Type u_2) (F : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) (K : TopologicalSpace.Compacts E) : ContDiffMapSupportedIn E F n K →+ E → F

Coercion as an additive homomorphism.

Equations

• ContDiffMapSupportedIn.coeHom E F n K = { toFun := fun (f : ContDiffMapSupportedIn E F n K) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }

theorem ContDiffMapSupportedIn.coe_coeHom {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) (K : TopologicalSpace.Compacts E) : ⇑(coeHom E F n K) = DFunLike.coe

theorem ContDiffMapSupportedIn.coeHom_injective {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) (K : TopologicalSpace.Compacts E) : Function.Injective ⇑(coeHom E F n K)

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

Equations

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

theorem ContDiffMapSupportedIn.support_subset {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) : Function.support ⇑f ⊆ ↑K

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

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

def ContDiffMapSupportedIn.of_support_subset {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : E → F} (hf : ContDiff ℝ (↑n) f) (hsupp : Function.support f ⊆ ↑K) : ContDiffMapSupportedIn E F n K

Inclusion of unbundled n-times continuously differentiable function with support included in a compact K into the space 𝓓^{n}_{K}.

Equations

• ContDiffMapSupportedIn.of_support_subset hf hsupp = { toFun := f, contDiff' := hf, zero_on_compl' := ⋯ }

@[simp]

theorem ContDiffMapSupportedIn.coe_of_support_subset {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : E → F} (hf : ContDiff ℝ (↑n) f) (hsupp : Function.support f ⊆ ↑K) (a✝ : E) : (ContDiffMapSupportedIn.of_support_subset hf hsupp) a✝ = f a✝