Documentation

Mathlib.Topology.ContinuousMap.CompactlySupported

Compactly supported continuous functions #

In this file, we define the type C_c(α, β) of compactly supported continuous functions and the class CompactlySupportedContinuousMapClass, and prove basic properties.

Main definitions and results #

This file contains various instances such as Add, Mul, SMul F C_c(α, β) when F is a class of continuous functions. When β has more structures, C_c(α, β) inherits such structures as AddCommGroup, NonUnitalRing and StarRing.

When the domain α is compact, ContinuousMap.liftCompactlySupported gives the identification C(α, β) ≃ C_c(α, β).

structure CompactlySupportedContinuousMap (α : Type u_5) (β : Type u_6) [TopologicalSpace α] [Zero β] [TopologicalSpace β] extends C(α, β) :
Type (max u_5 u_6)

C_c(α, β) is the type of continuous functions α → β with compact support from a topological space to a topological space with a zero element.

When possible, instead of parametrizing results over f : C_c(α, β), you should parametrize over {F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend CompactlySupportedContinuousMapClass.

C_c(α, β) is the type of continuous functions α → β with compact support from a topological space to a topological space with a zero element.

When possible, instead of parametrizing results over f : C_c(α, β), you should parametrize over {F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend CompactlySupportedContinuousMapClass.

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

C_c(α, β) is the type of continuous functions α → β with compact support from a topological space to a topological space with a zero element.

When possible, instead of parametrizing results over f : C_c(α, β), you should parametrize over {F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend CompactlySupportedContinuousMapClass.

Equations
  • One or more equations did not get rendered due to their size.
class CompactlySupportedContinuousMapClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) [TopologicalSpace α] [Zero β] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass F α β :

CompactlySupportedContinuousMapClass F α β states that F is a type of continuous maps with compact support.

You should also extend this typeclass when you extend CompactlySupportedContinuousMap.

Instances
    theorem CompactlySupportedContinuousMap.ext {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {f g : CompactlySupportedContinuousMap α β} (h : ∀ (x : α), f x = g x) :
    f = g
    theorem CompactlySupportedContinuousMap.ext_iff {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {f g : CompactlySupportedContinuousMap α β} :
    f = g ∀ (x : α), f x = g x
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_mk {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : C(α, β)) (h : HasCompactSupport f) :
    { toContinuousMap := f, hasCompactSupport' := h } = f
    def CompactlySupportedContinuousMap.copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : CompactlySupportedContinuousMap α β) (f' : αβ) (h : f' = f) :

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

    Equations
    • f.copy f' h = { toFun := f', continuous_toFun := , hasCompactSupport' := }
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : CompactlySupportedContinuousMap α β) (f' : αβ) (h : f' = f) :
    (f.copy f' h) = f'
    theorem CompactlySupportedContinuousMap.copy_eq {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : CompactlySupportedContinuousMap α β) (f' : αβ) (h : f' = f) :
    f.copy f' h = f

    A continuous function on a compact space automatically has compact support.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def CompactlySupportedContinuousMap.compLeft {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {γ : Type u_5} [TopologicalSpace γ] [Zero γ] (g : C(β, γ)) (f : CompactlySupportedContinuousMap α β) :

    Composition of a continuous function f with compact support with another continuous function g sending 0 to 0 from the left yields another continuous function g ∘ f with compact support.

    If g doesn't send 0 to 0, f.compLeft g defaults to 0.

    Equations
    theorem CompactlySupportedContinuousMap.toContinuousMap_compLeft {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {γ : Type u_5} [TopologicalSpace γ] [Zero γ] {g : C(β, γ)} (hg : g 0 = 0) (f : CompactlySupportedContinuousMap α β) :
    theorem CompactlySupportedContinuousMap.coe_compLeft {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {γ : Type u_5} [TopologicalSpace γ] [Zero γ] {g : C(β, γ)} (hg : g 0 = 0) (f : CompactlySupportedContinuousMap α β) :
    (compLeft g f) = g f
    theorem CompactlySupportedContinuousMap.compLeft_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {γ : Type u_5} [TopologicalSpace γ] [Zero γ] {g : C(β, γ)} (hg : g 0 = 0) (f : CompactlySupportedContinuousMap α β) (a : α) :
    (compLeft g f) a = g (f a)

    Algebraic structure #

    Whenever β has the structure of continuous additive monoid and a compatible topological structure, then C_c(α, β) inherits a corresponding algebraic structure. The primary exception to this is that C_c(α, β) will not have a multiplicative identity.

    Equations
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_zero {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] :
    0 = 0
    theorem CompactlySupportedContinuousMap.zero_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (x : α) [Zero β] :
    0 x = 0
    Equations
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_mul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] (f g : CompactlySupportedContinuousMap α β) :
    ⇑(f * g) = f * g
    theorem CompactlySupportedContinuousMap.mul_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (x : α) [MulZeroClass β] [ContinuousMul β] (f g : CompactlySupportedContinuousMap α β) :
    (f * g) x = f x * g x

    the product of f : F assuming ContinuousMapClass F α γ and ContinuousSMul γ β and g : C_c(α, β) is in C_c(α, β)

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_smulc {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β] {F : Type u_5} [FunLike F α γ] [ContinuousMapClass F α γ] (f : F) (g : CompactlySupportedContinuousMap α β) :
    ⇑(f g) = fun (x : α) => f x g x
    theorem CompactlySupportedContinuousMap.smulc_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β] {F : Type u_5} [FunLike F α γ] [ContinuousMapClass F α γ] (f : F) (g : CompactlySupportedContinuousMap α β) (x : α) :
    (f g) x = f x g x
    Equations
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_add {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (f g : CompactlySupportedContinuousMap α β) :
    ⇑(f + g) = f + g
    theorem CompactlySupportedContinuousMap.add_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (x : α) [AddZeroClass β] [ContinuousAdd β] (f g : CompactlySupportedContinuousMap α β) :
    (f + g) x = f x + g x

    Coercion to a function as a AddMonoidHom. Similar to AddMonoidHom.coeFn.

    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_smul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_5} [SMulZeroClass R β] [ContinuousConstSMul R β] (r : R) (f : CompactlySupportedContinuousMap α β) :
    ⇑(r f) = r f
    theorem CompactlySupportedContinuousMap.smul_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_5} [SMulZeroClass R β] [ContinuousConstSMul R β] (r : R) (f : CompactlySupportedContinuousMap α β) (x : α) :
    (r f) x = r f x
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_sum {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_5} (s : Finset ι) (f : ιCompactlySupportedContinuousMap α β) :
    (∑ is, f i) = is, (f i)
    theorem CompactlySupportedContinuousMap.sum_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_5} (s : Finset ι) (f : ιCompactlySupportedContinuousMap α β) (a : α) :
    (∑ is, f i) a = is, (f i) a
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CompactlySupportedContinuousMap.sub_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (x : α) [AddGroup β] [IsTopologicalAddGroup β] (f g : CompactlySupportedContinuousMap α β) :
    (f - g) x = f x - g x

    Star structure #

    It is possible to equip C_c(α, β) with a pointwise star operation whenever there is a continuous star : β → β for which star (0 : β) = 0. We don't have quite this weak a typeclass, but StarAddMonoid is close enough.

    The StarAddMonoid class on C_c(α, β) is inherited from their counterparts on α →ᵇ β.

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

    The partial order in C_c #

    When β is equipped with a partial order, C_c(α, β) is given the pointwise partial order.

    theorem CompactlySupportedContinuousMap.le_def {α : Type u_2} [TopologicalSpace α] {β : Type u_5} [TopologicalSpace β] [Zero β] [PartialOrder β] {f g : CompactlySupportedContinuousMap α β} :
    f g ∀ (a : α), f a g a
    theorem CompactlySupportedContinuousMap.lt_def {α : Type u_2} [TopologicalSpace α] {β : Type u_5} [TopologicalSpace β] [Zero β] [PartialOrder β] {f g : CompactlySupportedContinuousMap α β} :
    f < g (∀ (a : α), f a g a) ∃ (a : α), f a < g a
    Equations
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_sup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] (f g : CompactlySupportedContinuousMap α β) :
    (fg) = fg
    @[simp]
    theorem CompactlySupportedContinuousMap.sup_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] (f g : CompactlySupportedContinuousMap α β) (a : α) :
    (fg) a = f ag a
    theorem CompactlySupportedContinuousMap.finsetSup'_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty) (f : ιCompactlySupportedContinuousMap α β) (a : α) :
    (s.sup' H f) a = s.sup' H fun (i : ι) => (f i) a
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_finsetSup' {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty) (f : ιCompactlySupportedContinuousMap α β) :
    (s.sup' H f) = s.sup' H fun (i : ι) => (f i)
    Equations
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_inf {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] (f g : CompactlySupportedContinuousMap α β) :
    (fg) = fg
    @[simp]
    theorem CompactlySupportedContinuousMap.inf_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] (f g : CompactlySupportedContinuousMap α β) (a : α) :
    (fg) a = f ag a
    theorem CompactlySupportedContinuousMap.finsetInf'_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty) (f : ιCompactlySupportedContinuousMap α β) (a : α) :
    (s.inf' H f) a = s.inf' H fun (i : ι) => (f i) a
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_finsetInf' {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty) (f : ιCompactlySupportedContinuousMap α β) :
    (s.inf' H f) = s.inf' H fun (i : ι) => (f i)

    C_c as a functor #

    For each β with sufficient structure, there is a contravariant functor C_c(-, β) from the category of topological spaces with morphisms given by CocompactMaps.

    Composition of a continuous function with compact support with a cocompact map yields another continuous function with compact support.

    Equations
    • f.comp g = { toContinuousMap := (↑f).comp g, hasCompactSupport' := }
    @[simp]
    theorem CompactlySupportedContinuousMap.coe_comp_to_continuous_fun {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : CompactlySupportedContinuousMap γ δ) (g : CocompactMap β γ) :
    (f.comp g) = f g
    @[simp]
    theorem CompactlySupportedContinuousMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : CompactlySupportedContinuousMap γ δ) (g : CocompactMap β γ) (h : CocompactMap α β) :
    (f.comp g).comp h = f.comp (g.comp h)
    @[simp]
    theorem CompactlySupportedContinuousMap.zero_comp {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (g : CocompactMap β γ) :
    comp 0 g = 0

    Composition as an additive monoid homomorphism.

    Equations

    Composition as a semigroup homomorphism.

    Equations

    Composition as a linear map.

    Equations

    Composition as a non-unital algebra homomorphism.

    Equations
    Equations

    A continuous function on a compact space has automatically compact support. This is not an instance to avoid type class loops.

    The nonnegative part of a bounded continuous -valued function as a bounded continuous ℝ≥0-valued function.

    Equations

    The compactly supported continuous ℝ≥0-valued function as a compactly supported -valued function.

    Equations

    The compactly supported continuous ℝ≥0-valued function as a compactly supported -valued function.

    Equations

    For a positive linear functional Λ : C_c(α, ℝ) → ℝ, define a ℝ≥0-linear map.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CompactlySupportedContinuousMap.toNNRealLinear_inj {α : Type u_2} [TopologicalSpace α] (Λ₁ Λ₂ : CompactlySupportedContinuousMap α →ₗ[] ) (hΛ₁ : ∀ (f : CompactlySupportedContinuousMap α ), 0 f0 Λ₁ f) (hΛ₂ : ∀ (f : CompactlySupportedContinuousMap α ), 0 f0 Λ₂ f) :
    toNNRealLinear Λ₁ hΛ₁ = toNNRealLinear Λ₂ hΛ₂ Λ₁ = Λ₂