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.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) : E → F

See note [custom simps projection].

Equations

• ContDiffMapSupportedIn.Simps.apply 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