Functionals on bounded functions and contents on all subsets

On a discrete space, applying a linear functional to characteristic functions gives a real-valued content on all subsets. It is nonnegative when the functional is positive, and its total mass is the functional's value at one.

Conversely, every nonnegative real content ν on all subsets of a discrete space X arises in this way from exactly one positive linear functional on X →ᵇ ℝ. A finite-valued function f is integrated by the finite sum ∑ c, c * ν {x | f x = c}. These sums are bounded by ν univ times the supremum norm, and finite-valued functions are uniformly dense among bounded functions, so the integral extends uniquely by continuity. The extension is positive because it has norm at most its value ν univ at the constant one. This is the correspondence between means and finitely additive probabilities; neither side involves countable additivity.

We use Mathlib's bounded continuous characteristic functions, with a small API for clopen sets that also applies without discreteness. The finite sums are MeasureTheory.AddContent.integralSimple, the density of finite-valued functions is MeasureTheory.SimpleFunc.denseRange_toBoundedContinuousFunction, and the extension is LinearMap.extendOfNorm.

Main definitions

• LinearMap.toAddContent: the real content s ↦ m (indicator s) of a linear functional m.
• PositiveLinearMap.addContentEquiv: positive linear functionals on bounded functions on a discrete space correspond to nonnegative real contents on all subsets.

Main results

• PositiveLinearMap.addContentEquiv_symm_apply_indicator: the functional associated to a content ν takes the value ν s at the characteristic function of s.

References

• A. Garrido, An introduction to amenable groups, Theorem 1.15.

@[simp]

theorem BoundedContinuousFunction.indicator_empty {X : Type u_1} [TopologicalSpace X] : indicator ∅ ⋯ = 0

@[simp]

theorem BoundedContinuousFunction.indicator_univ {X : Type u_1} [TopologicalSpace X] : indicator Set.univ ⋯ = 1

theorem BoundedContinuousFunction.indicator_union {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hs : IsClopen s) (ht : IsClopen t) (hst : Disjoint s t) : indicator (s ∪ t) ⋯ = indicator s hs + indicator t ht

Characteristic functions add on disjoint clopen sets.

theorem BoundedContinuousFunction.indicator_nonneg {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsClopen s) : 0 ≤ indicator s hs

A characteristic function is pointwise nonnegative.

@[simp]

theorem BoundedContinuousFunction.indicator_compContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (hs : IsClopen s) (f : C(Y, X)) : (indicator s hs).compContinuous f = indicator (⇑f ⁻¹' s) ⋯

Pullback of a characteristic function is the characteristic function of the preimage.

noncomputable def LinearMap.toAddContent {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (m : BoundedContinuousFunction X ℝ →ₗ[ℝ] ℝ) : MeasureTheory.AddContent ℝ Set.univ

The real content obtained by evaluating a linear functional on characteristic functions.

@[simp]

theorem LinearMap.toAddContent_apply {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (m : BoundedContinuousFunction X ℝ →ₗ[ℝ] ℝ) (s : Set X) : m.toAddContent s = m (BoundedContinuousFunction.indicator s ⋯)

@[simp]

theorem LinearMap.toAddContent_univ {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (m : BoundedContinuousFunction X ℝ →ₗ[ℝ] ℝ) : m.toAddContent Set.univ = m 1

theorem PositiveLinearMap.toAddContent_nonneg {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (m : BoundedContinuousFunction X ℝ →ₚ[ℝ] ℝ) (s : Set X) : 0 ≤ m.toAddContent s

The content of a positive functional is nonnegative.

Integration against a nonnegative content

A nonnegative real content ν on all subsets of X is integrated first on finite-valued functions, by ∑ c, c * ν {x | f x = c}, and then on all bounded functions by uniform approximation. For the finite sums we use AddContent.integralSimple, with every subset measurable.

noncomputable def PositiveLinearMap.addContentEquiv (X : Type u_1) [TopologicalSpace X] [DiscreteTopology X] : (BoundedContinuousFunction X ℝ →ₚ[ℝ] ℝ) ≃ { ν : MeasureTheory.AddContent ℝ Set.univ // ∀ (s : Set X), 0 ≤ ν s }

On a discrete space, positive linear functionals on bounded real functions correspond to nonnegative finitely additive real set functions on all subsets, by evaluating at characteristic functions. The inverse integrates a bounded function against the content.

@[simp]

theorem PositiveLinearMap.coe_addContentEquiv_apply {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (m : BoundedContinuousFunction X ℝ →ₚ[ℝ] ℝ) : ↑((addContentEquiv X) m) = m.toAddContent

@[simp]

theorem PositiveLinearMap.addContentEquiv_symm_apply_indicator {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (ν : { ν : MeasureTheory.AddContent ℝ Set.univ // ∀ (s : Set X), 0 ≤ ν s }) (s : Set X) : ((addContentEquiv X).symm ν) (BoundedContinuousFunction.indicator s ⋯) = ↑ν s

The functional associated to a content takes the value ν s at the characteristic function of s.

@[simp]

theorem PositiveLinearMap.addContentEquiv_symm_apply_one {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] (ν : { ν : MeasureTheory.AddContent ℝ Set.univ // ∀ (s : Set X), 0 ≤ ν s }) : ((addContentEquiv X).symm ν) 1 = ↑ν Set.univ

The functional associated to a content takes its total mass at the constant one.