Maps on compactly supported continuous functions

Order and nnrealPart lemmas for Mathlib's CompactlySupportedContinuousMap.toReal, the map C_c(X, ℝ≥0) → C_c(X, ℝ): it sends 0 to 0, it is an order embedding, and on nonnegative functions it is inverse to CompactlySupportedContinuousMap.nnrealPart.

The forgetful map from compactly supported to continuous functions preserves addition and constant scalar multiplication whenever those operations are defined.

On a linearly ordered domain, a compactly supported continuous function is dominated by a constant multiple of the indicator of a closed interval, and such a domination forces it to vanish off that interval.

@[simp]

theorem CompactlySupportedContinuousMap.toContinuousMap_add {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] [AddZeroClass Y] [ContinuousAdd Y] (f g : CompactlySupportedContinuousMap X Y) : (f + g).toContinuousMap = f.toContinuousMap + g.toContinuousMap

Forgetting compact support preserves addition.

@[simp]

theorem CompactlySupportedContinuousMap.toContinuousMap_smul {X : Type u_1} [TopologicalSpace X] {R : Type u_2} {Y : Type u_3} [TopologicalSpace Y] [Zero Y] [SMulZeroClass R Y] [ContinuousConstSMul R Y] (r : R) (f : CompactlySupportedContinuousMap X Y) : (r • f).toContinuousMap = r • f.toContinuousMap

Forgetting compact support preserves scalar multiplication.

@[simp]

theorem CompactlySupportedContinuousMap.toReal_zero {X : Type u_1} [TopologicalSpace X] : toReal 0 = 0

toReal sends the zero function to the zero function.

@[simp]

theorem CompactlySupportedContinuousMap.toReal_le_toReal_iff {X : Type u_1} [TopologicalSpace X] {f g : CompactlySupportedContinuousMap X NNReal} : f.toReal ≤ g.toReal ↔ f ≤ g

toReal is an order embedding.

theorem CompactlySupportedContinuousMap.toReal_nnrealPart_of_nonneg {X : Type u_1} [TopologicalSpace X] {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) : f.nnrealPart.toReal = f

On a nonnegative function, toReal is a left inverse of nnrealPart; compare nnrealPart_toReal_eq.

theorem CompactlySupportedContinuousMap.exists_enorm_le_indicator {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [ClosedIicTopology X] [ClosedIciTopology X] [Nonempty X] {E : Type u_2} [NormedAddGroup E] (f : CompactlySupportedContinuousMap X E) : ∃ (C : NNReal) (a : X) (b : X), ∀ (y : X), ‖f y‖ₑ ≤ (Set.Icc a b).indicator (fun (x : X) => ↑C) y

On a linearly ordered domain, a compactly supported continuous function is dominated by a constant multiple of the indicator of a closed interval.

theorem CompactlySupportedContinuousMap.eq_zero_of_enorm_le_indicator {X : Type u_1} [TopologicalSpace X] [Preorder X] {E : Type u_2} [NormedAddGroup E] {f : CompactlySupportedContinuousMap X E} {C : NNReal} {a b x : X} (hf : ∀ (y : X), ‖f y‖ₑ ≤ (Set.Icc a b).indicator (fun (x : X) => ↑C) y) (hx : x ∉ Set.Icc a b) : f x = 0

A function dominated by a multiple of the indicator of Icc a b vanishes off Icc a b.