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.

• toFun : α → β
• continuous_toFun : Continuous self.toFun
• hasCompactSupport' : HasCompactSupport self.toFun

  The function has compact support .

def CompactlySupported.«termC_c(_,_)» : Lean.ParserDescr

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.

def CompactlySupported.«term_→C_c_» : Lean.TrailingParserDescr

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.

class CompactlySupportedContinuousMapClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) [TopologicalSpace α] [Zero β] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass F α β : Prop

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

You should also extend this typeclass when you extend CompactlySupportedContinuousMap.

• map_continuous (f : F) : Continuous ⇑f
• hasCompactSupport (f : F) : HasCompactSupport ⇑f

  Each member of the class has compact support.

instance CompactlySupportedContinuousMap.instFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] : FunLike (CompactlySupportedContinuousMap α β) α β

theorem CompactlySupportedContinuousMap.hasCompactSupport {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : CompactlySupportedContinuousMap α β) : HasCompactSupport ⇑f

instance CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] : CompactlySupportedContinuousMapClass (CompactlySupportedContinuousMap α β) α β

@[simp]

theorem CompactlySupportedContinuousMap.coe_toContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : CompactlySupportedContinuousMap α β) : ⇑f.toContinuousMap = ⇑f

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) : CompactlySupportedContinuousMap α β

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

@[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

theorem CompactlySupportedContinuousMap.eq_of_empty {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [IsEmpty α] (f g : CompactlySupportedContinuousMap α β) : f = g

def CompactlySupportedContinuousMap.ContinuousMap.liftCompactlySupported {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] : C(α, β) ≃ CompactlySupportedContinuousMap α β

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

@[simp]

theorem CompactlySupportedContinuousMap.ContinuousMap.liftCompactlySupported_apply_toFun {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] (f : C(α, β)) (a : α) : (liftCompactlySupported f) a = f a

@[simp]

theorem CompactlySupportedContinuousMap.ContinuousMap.liftCompactlySupported_symm_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [CompactSpace α] (f : CompactlySupportedContinuousMap α β) : liftCompactlySupported.symm f = ↑f

noncomputable def CompactlySupportedContinuousMap.compLeft {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {γ : Type u_5} [TopologicalSpace γ] [Zero γ] (g : C(β, γ)) (f : CompactlySupportedContinuousMap α β) : 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.

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 α β) : (compLeft g f).toContinuousMap = g.comp ↑f

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.

instance CompactlySupportedContinuousMap.instZero {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] : Zero (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instInhabited {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] : Inhabited (CompactlySupportedContinuousMap α β)

@[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

instance CompactlySupportedContinuousMap.instMulOfContinuousMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] : Mul (CompactlySupportedContinuousMap α β)

@[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

instance CompactlySupportedContinuousMap.instSMulOfContinuousSMulOfContinuousMapClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β] {F : Type u_5} [FunLike F α γ] [ContinuousMapClass F α γ] : SMul F (CompactlySupportedContinuousMap α β)

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

@[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

instance CompactlySupportedContinuousMap.instMulZeroClassOfContinuousMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] : MulZeroClass (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instSemigroupWithZeroOfContinuousMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [SemigroupWithZero β] [ContinuousMul β] : SemigroupWithZero (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instAddOfContinuousAdd {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] : Add (CompactlySupportedContinuousMap α β)

@[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

instance CompactlySupportedContinuousMap.instAddZeroClassOfContinuousAdd {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] : AddZeroClass (CompactlySupportedContinuousMap α β)

def CompactlySupportedContinuousMap.coeFnMonoidHom {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] : CompactlySupportedContinuousMap α β →+ α → β

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

instance CompactlySupportedContinuousMap.instSMulOfContinuousConstSMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_5} [SMulZeroClass R β] [ContinuousConstSMul R β] : SMul R (CompactlySupportedContinuousMap α β)

@[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

instance CompactlySupportedContinuousMap.instAddMonoidOfContinuousAdd {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] : AddMonoid (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] : AddCommMonoid (CompactlySupportedContinuousMap α β)

@[simp]

theorem CompactlySupportedContinuousMap.coe_sum {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_5} (s : Finset ι) (f : ι → CompactlySupportedContinuousMap α β) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

theorem CompactlySupportedContinuousMap.sum_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_5} (s : Finset ι) (f : ι → CompactlySupportedContinuousMap α β) (a : α) : (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

instance CompactlySupportedContinuousMap.instNeg {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] : Neg (CompactlySupportedContinuousMap α β)

@[simp]

theorem CompactlySupportedContinuousMap.coe_neg {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] (f : CompactlySupportedContinuousMap α β) : ⇑(-f) = -⇑f

theorem CompactlySupportedContinuousMap.neg_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (x : α) [AddGroup β] [IsTopologicalAddGroup β] (f : CompactlySupportedContinuousMap α β) : (-f) x = -f x

instance CompactlySupportedContinuousMap.instSub {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] : Sub (CompactlySupportedContinuousMap α β)

@[simp]

theorem CompactlySupportedContinuousMap.coe_sub {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] (f g : CompactlySupportedContinuousMap α β) : ⇑(f - g) = ⇑f - ⇑g

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

instance CompactlySupportedContinuousMap.instAddGroup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] : AddGroup (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instAddCommGroupOfIsTopologicalAddGroup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [IsTopologicalAddGroup β] : AddCommGroup (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instIsCentralScalar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_5} [Zero R] [SMulWithZero R β] [SMulWithZero Rᵐᵒᵖ β] [ContinuousConstSMul R β] [IsCentralScalar R β] : IsCentralScalar R (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instSMulWithZeroOfContinuousConstSMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_5} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] : SMulWithZero R (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instMulActionWithZeroOfContinuousConstSMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {R : Type u_5} [MonoidWithZero R] [MulActionWithZero R β] [ContinuousConstSMul R β] : MulActionWithZero R (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {R : Type u_5} [Semiring R] [Module R β] [ContinuousConstSMul R β] : Module R (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] : NonUnitalNonAssocSemiring (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instNonUnitalSemiringOfIsTopologicalSemiring {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalSemiring β] [IsTopologicalSemiring β] : NonUnitalSemiring (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instNonUnitalCommSemiringOfIsTopologicalSemiring {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommSemiring β] [IsTopologicalSemiring β] : NonUnitalCommSemiring (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instNonUnitalNonAssocRingOfIsTopologicalRing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocRing β] [IsTopologicalRing β] : NonUnitalNonAssocRing (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instNonUnitalRingOfIsTopologicalRing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalRing β] [IsTopologicalRing β] : NonUnitalRing (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instNonUnitalCommRingOfIsTopologicalRing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommRing β] [IsTopologicalRing β] : NonUnitalCommRing (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instIsScalarTower {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_5} [Semiring R] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [Module R β] [ContinuousConstSMul R β] [IsScalarTower R β β] : IsScalarTower R (CompactlySupportedContinuousMap α β) (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instSMulCommClass {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_5} [Semiring R] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [Module R β] [ContinuousConstSMul R β] [SMulCommClass R β β] : SMulCommClass R (CompactlySupportedContinuousMap α β) (CompactlySupportedContinuousMap α β)

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 α →ᵇ β.

instance CompactlySupportedContinuousMap.instStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] : Star (CompactlySupportedContinuousMap α β)

@[simp]

theorem CompactlySupportedContinuousMap.coe_star {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] (f : CompactlySupportedContinuousMap α β) : ⇑(star f) = star ⇑f

theorem CompactlySupportedContinuousMap.star_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] (f : CompactlySupportedContinuousMap α β) (x : α) : (star f) x = star (f x)

instance CompactlySupportedContinuousMap.instTrivialStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] [TrivialStar β] : TrivialStar (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instStarAddMonoid {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [StarAddMonoid β] [ContinuousStar β] [ContinuousAdd β] : StarAddMonoid (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instStarModule {α : Type u_2} {β : Type u_3} [TopologicalSpace α] {𝕜 : Type u_5} [Zero 𝕜] [Star 𝕜] [AddMonoid β] [StarAddMonoid β] [TopologicalSpace β] [ContinuousStar β] [SMulWithZero 𝕜 β] [ContinuousConstSMul 𝕜 β] [StarModule 𝕜 β] : StarModule 𝕜 (CompactlySupportedContinuousMap α β)

instance CompactlySupportedContinuousMap.instStarRing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [NonUnitalSemiring β] [StarRing β] [TopologicalSpace β] [ContinuousStar β] [IsTopologicalSemiring β] : StarRing (CompactlySupportedContinuousMap α β)

The partial order in C_c

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

instance CompactlySupportedContinuousMap.partialOrder {α : Type u_2} [TopologicalSpace α] {β : Type u_5} [TopologicalSpace β] [Zero β] [PartialOrder β] : PartialOrder (CompactlySupportedContinuousMap α β)

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

instance CompactlySupportedContinuousMap.instSup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] : Max (CompactlySupportedContinuousMap α β)

@[simp]

theorem CompactlySupportedContinuousMap.coe_sup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] (f g : CompactlySupportedContinuousMap α β) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

@[simp]

theorem CompactlySupportedContinuousMap.sup_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] (f g : CompactlySupportedContinuousMap α β) (a : α) : (f ⊔ g) a = f a ⊔ g a

instance CompactlySupportedContinuousMap.semilatticeSup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeSup β] [Zero β] [TopologicalSpace β] [ContinuousSup β] : SemilatticeSup (CompactlySupportedContinuousMap α β)

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)

instance CompactlySupportedContinuousMap.instInf {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] : Min (CompactlySupportedContinuousMap α β)

@[simp]

theorem CompactlySupportedContinuousMap.coe_inf {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] (f g : CompactlySupportedContinuousMap α β) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

@[simp]

theorem CompactlySupportedContinuousMap.inf_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] (f g : CompactlySupportedContinuousMap α β) (a : α) : (f ⊓ g) a = f a ⊓ g a

instance CompactlySupportedContinuousMap.semilatticeInf {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SemilatticeInf β] [Zero β] [TopologicalSpace β] [ContinuousInf β] : SemilatticeInf (CompactlySupportedContinuousMap α β)

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)

instance CompactlySupportedContinuousMap.instLatticeOfTopologicalLattice {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Lattice β] [TopologicalSpace β] [TopologicalLattice β] [Zero β] : Lattice (CompactlySupportedContinuousMap α β)

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.

def CompactlySupportedContinuousMap.comp {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : CompactlySupportedContinuousMap γ δ) (g : CocompactMap β γ) : CompactlySupportedContinuousMap β δ

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

@[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_id {γ : Type u_4} {δ : Type u_5} [TopologicalSpace γ] [TopologicalSpace δ] [Zero δ] (f : CompactlySupportedContinuousMap γ δ) : f.comp (CocompactMap.id γ) = f

@[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

def CompactlySupportedContinuousMap.compAddMonoidHom {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [AddMonoid δ] [ContinuousAdd δ] (g : CocompactMap β γ) : CompactlySupportedContinuousMap γ δ →+ CompactlySupportedContinuousMap β δ

Composition as an additive monoid homomorphism.

def CompactlySupportedContinuousMap.compMulHom {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [MulZeroClass δ] [ContinuousMul δ] (g : CocompactMap β γ) : CompactlySupportedContinuousMap γ δ →ₙ* CompactlySupportedContinuousMap β δ

Composition as a semigroup homomorphism.

def CompactlySupportedContinuousMap.compLinearMap {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] [AddCommMonoid δ] [ContinuousAdd δ] {R : Type u_6} [Semiring R] [Module R δ] [ContinuousConstSMul R δ] (g : CocompactMap β γ) : CompactlySupportedContinuousMap γ δ →ₗ[R] CompactlySupportedContinuousMap β δ

Composition as a linear map.

def CompactlySupportedContinuousMap.compNonUnitalAlgHom {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {R : Type u_6} [Semiring R] [NonUnitalNonAssocSemiring δ] [IsTopologicalSemiring δ] [Module R δ] [ContinuousConstSMul R δ] (g : CocompactMap β γ) : CompactlySupportedContinuousMap γ δ →ₙₐ[R] CompactlySupportedContinuousMap β δ

Composition as a non-unital algebra homomorphism.

instance CompactlySupportedContinuousMapClass.instCoeTCCompactlySupportedContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Zero β] [TopologicalSpace β] [FunLike F α β] [CompactlySupportedContinuousMapClass F α β] : CoeTC F (CompactlySupportedContinuousMap α β)

theorem CompactlySupportedContinuousMapClass.of_compactSpace {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Zero β] [TopologicalSpace β] (G : Type u_5) [FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α] : CompactlySupportedContinuousMapClass G α β

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

theorem CompactlySupportedContinuousMapClass.uniformContinuous {F : Type u_1} {β : Type u_3} {γ : Type u_4} [UniformSpace β] [UniformSpace γ] [Zero γ] [FunLike F β γ] [CompactlySupportedContinuousMapClass F β γ] (f : F) : UniformContinuous ⇑f

instance CompactlySupportedContinuousMapClass.instZeroAtInftyContinuousMapClass {F : Type u_1} {β : Type u_3} {γ : Type u_4} [TopologicalSpace β] [TopologicalSpace γ] [Zero γ] [FunLike F β γ] [CompactlySupportedContinuousMapClass F β γ] : ZeroAtInftyContinuousMapClass F β γ

theorem CompactlySupportedContinuousMap.exists_add_of_le {α : Type u_2} [TopologicalSpace α] {f₁ f₂ : CompactlySupportedContinuousMap α NNReal} (h : f₁ ≤ f₂) : ∃ (g : CompactlySupportedContinuousMap α NNReal), f₁ + g = f₂

noncomputable def CompactlySupportedContinuousMap.nnrealPart {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) : CompactlySupportedContinuousMap α NNReal

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

@[simp]

theorem CompactlySupportedContinuousMap.nnrealPart_apply {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) (x : α) : f.nnrealPart x = (f x).toNNReal

theorem CompactlySupportedContinuousMap.nnrealPart_neg_eq_zero_of_nonneg {α : Type u_2} [TopologicalSpace α] {f : CompactlySupportedContinuousMap α ℝ} (hf : 0 ≤ f) : (-f).nnrealPart = 0

theorem CompactlySupportedContinuousMap.nnrealPart_smul_pos {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) {a : ℝ} (ha : 0 ≤ a) : (a • f).nnrealPart = a.toNNReal • f.nnrealPart

theorem CompactlySupportedContinuousMap.nnrealPart_smul_neg {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) {a : ℝ} (ha : a ≤ 0) : (a • f).nnrealPart = (-a).toNNReal • (-f).nnrealPart

theorem CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart {α : Type u_2} [TopologicalSpace α] (f g : CompactlySupportedContinuousMap α ℝ) : (f + g).nnrealPart ≤ f.nnrealPart + g.nnrealPart

theorem CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq {α : Type u_2} [TopologicalSpace α] (f g : CompactlySupportedContinuousMap α ℝ) : ∃ (h : CompactlySupportedContinuousMap α NNReal), (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

noncomputable def CompactlySupportedContinuousMap.toReal {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) : CompactlySupportedContinuousMap α ℝ

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

@[simp]

theorem CompactlySupportedContinuousMap.toReal_apply {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) (x : α) : f.toReal x = ↑(f x)

@[simp]

theorem CompactlySupportedContinuousMap.toReal_nonneg {α : Type u_2} [TopologicalSpace α] {f : CompactlySupportedContinuousMap α NNReal} : 0 ≤ f.toReal

@[simp]

theorem CompactlySupportedContinuousMap.toReal_add {α : Type u_2} [TopologicalSpace α] (f g : CompactlySupportedContinuousMap α NNReal) : (f + g).toReal = f.toReal + g.toReal

@[simp]

theorem CompactlySupportedContinuousMap.toReal_smul {α : Type u_2} [TopologicalSpace α] (r : NNReal) (f : CompactlySupportedContinuousMap α NNReal) : (r • f).toReal = r • f.toReal

@[simp]

theorem CompactlySupportedContinuousMap.nnrealPart_sub_nnrealPart_neg {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) : f.nnrealPart.toReal - (-f).nnrealPart.toReal = f

noncomputable def CompactlySupportedContinuousMap.toRealLinearMap {α : Type u_2} [TopologicalSpace α] : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] CompactlySupportedContinuousMap α ℝ

The map toReal defined as a ℝ≥0-linear map.

@[simp]

theorem CompactlySupportedContinuousMap.coe_toRealLinearMap {α : Type u_2} [TopologicalSpace α] : ⇑toRealLinearMap = toReal

theorem CompactlySupportedContinuousMap.toRealLinearMap_apply {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) : toRealLinearMap f = f.toReal

theorem CompactlySupportedContinuousMap.toRealLinearMap_apply_apply {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) (x : α) : (toRealLinearMap f) x = ↑(f x)

@[simp]

theorem CompactlySupportedContinuousMap.nnrealPart_toReal_eq {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) : f.toReal.nnrealPart = f

@[simp]

theorem CompactlySupportedContinuousMap.nnrealPart_neg_toReal_eq {α : Type u_2} [TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) : (-f.toReal).nnrealPart = 0

noncomputable def CompactlySupportedContinuousMap.toNNRealLinear {α : Type u_2} [TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α ℝ →ₗ[ℝ] ℝ) (hΛ : ∀ (f : CompactlySupportedContinuousMap α ℝ), 0 ≤ f → 0 ≤ Λ f) : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal

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

@[simp]

theorem CompactlySupportedContinuousMap.toNNRealLinear_apply {α : Type u_2} [TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α ℝ →ₗ[ℝ] ℝ) (hΛ : ∀ (f : CompactlySupportedContinuousMap α ℝ), 0 ≤ f → 0 ≤ Λ f) (f : CompactlySupportedContinuousMap α NNReal) : ↑((toNNRealLinear Λ hΛ) f) = Λ f.toReal

@[simp]

theorem CompactlySupportedContinuousMap.toNNRealLinear_inj {α : Type u_2} [TopologicalSpace α] (Λ₁ Λ₂ : CompactlySupportedContinuousMap α ℝ →ₗ[ℝ] ℝ) (hΛ₁ : ∀ (f : CompactlySupportedContinuousMap α ℝ), 0 ≤ f → 0 ≤ Λ₁ f) (hΛ₂ : ∀ (f : CompactlySupportedContinuousMap α ℝ), 0 ≤ f → 0 ≤ Λ₂ f) : toNNRealLinear Λ₁ hΛ₁ = toNNRealLinear Λ₂ hΛ₂ ↔ Λ₁ = Λ₂

noncomputable def CompactlySupportedContinuousMap.toRealLinear {α : Type u_2} [TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal) : CompactlySupportedContinuousMap α ℝ →ₗ[ℝ] ℝ

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

theorem CompactlySupportedContinuousMap.toRealLinear_apply {α : Type u_2} [TopologicalSpace α] {Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal} (f : CompactlySupportedContinuousMap α ℝ) : (toRealLinear Λ) f = ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart)

theorem CompactlySupportedContinuousMap.toRealLinear_nonneg {α : Type u_2} [TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal) (g : CompactlySupportedContinuousMap α ℝ) (hg : 0 ≤ g) : 0 ≤ (toRealLinear Λ) g

@[simp]

theorem CompactlySupportedContinuousMap.eq_toRealLinear_toReal {α : Type u_2} [TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal) (f : CompactlySupportedContinuousMap α NNReal) : (toRealLinear Λ) f.toReal = ↑(Λ f)

@[simp]

theorem CompactlySupportedContinuousMap.eq_toNNRealLinear_toRealLinear {α : Type u_2} [TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal) : toNNRealLinear (toRealLinear Λ) ⋯ = Λ