Simple functions on a discrete space as bounded continuous functions

On a discrete space X, a simple function has finite range, so it is a bounded continuous function. When every subset of X is measurable, every finite-valued function is simple, and so simple functions are uniformly dense among bounded real functions on X.

Main definitions

• MeasureTheory.SimpleFunc.toBoundedContinuousFunction: a simple function on a discrete space as a bounded continuous function.
• MeasureTheory.SimpleFunc.toBoundedContinuousFunctionLinearMap: the same inclusion, as a linear map.

Main results

• MeasureTheory.SimpleFunc.denseRange_toBoundedContinuousFunction: on a discrete space where every subset is measurable, simple functions are uniformly dense among bounded real functions.

noncomputable def MeasureTheory.SimpleFunc.toBoundedContinuousFunction {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {E : Type u_2} [PseudoMetricSpace E] (g : SimpleFunc X E) : BoundedContinuousFunction X E

On a discrete space, a simple function as a bounded continuous function.

@[simp]

theorem MeasureTheory.SimpleFunc.toBoundedContinuousFunction_apply {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {E : Type u_2} [PseudoMetricSpace E] (g : SimpleFunc X E) (x : X) : g.toBoundedContinuousFunction x = g x

theorem MeasureTheory.SimpleFunc.toBoundedContinuousFunction_piecewise_const {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {s : Set X} (hs : MeasurableSet s) (c : ℝ) : (piecewise s hs (const X c) (const X 0)).toBoundedContinuousFunction = c • BoundedContinuousFunction.indicator s ⋯

A simple function equal to c on s and to 0 off s is c times the characteristic function of s.

theorem MeasureTheory.SimpleFunc.denseRange_toBoundedContinuousFunction {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [DiscreteMeasurableSpace X] : DenseRange toBoundedContinuousFunction

On a discrete space where every subset is measurable, simple functions are uniformly dense among bounded real functions.

@[simp]

theorem MeasureTheory.SimpleFunc.toBoundedContinuousFunction_add {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {E : Type u_2} [SeminormedAddCommGroup E] (f g : SimpleFunc X E) : (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction

noncomputable def MeasureTheory.SimpleFunc.toBoundedContinuousFunctionLinearMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {E : Type u_2} [SeminormedAddCommGroup E] (𝕜 : Type u_3) [NormedField 𝕜] [NormedSpace 𝕜 E] : SimpleFunc X E →ₗ[𝕜] BoundedContinuousFunction X E

On a discrete space, the inclusion of simple functions into bounded continuous functions, as a linear map.

@[simp]

theorem MeasureTheory.SimpleFunc.coe_toBoundedContinuousFunctionLinearMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {E : Type u_2} [SeminormedAddCommGroup E] (𝕜 : Type u_3) [NormedField 𝕜] [NormedSpace 𝕜 E] : ⇑(toBoundedContinuousFunctionLinearMap 𝕜) = toBoundedContinuousFunction

theorem MeasureTheory.SimpleFunc.toBoundedContinuousFunctionLinearMap_apply {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] {E : Type u_2} [SeminormedAddCommGroup E] (𝕜 : Type u_3) [NormedField 𝕜] [NormedSpace 𝕜 E] (g : SimpleFunc X E) : (toBoundedContinuousFunctionLinearMap 𝕜) g = g.toBoundedContinuousFunction

theorem MeasureTheory.SimpleFunc.denseRange_toBoundedContinuousFunctionLinearMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [DiscreteMeasurableSpace X] : DenseRange ⇑(toBoundedContinuousFunctionLinearMap ℝ)

On a discrete space where every subset is measurable, simple functions are uniformly dense among bounded real functions, stated for the linear inclusion.