Physlib

PhyslibAlpha.Mathematics.MeasureTheory.PositiveFunctionalIntegral

Positive functionals are integrals

i. Overview

On a compact space `X`, a positive linear functional on continuous functions is integration against a measure. This is the Riesz–Markov–Kakutani theorem. Often the functional is only known on some continuous functions, for example on observables seen as functions on the pure states.

Here the functional `φ` is given through a linear map `T : V → C(X, ℝ)` whose range contains the constant `1`. Suppose `φ v ≥ 0` whenever `T v ≥ 0`, and `φ` equals `1` at a preimage of `1`. Then `φ` is integration of `T` against a regular probability measure. The M. Riesz extension theorem first extends `φ` positively to all continuous functions.

ii. Key results

- `ContinuousMap.instPosSMulMono` proves that scaling by a nonnegative number preserves the order of continuous functions. - `exists_positive_extension` proves that `φ` extends to a positive functional on `C(X, ℝ)`. - `exists_regular_probabilityMeasure_integral_eq` proves that `φ` is an integral.

iii. Table of contents

  • A. Scaling continuous functions preserves their order
  • B. Positive functionals are integrals

A. Scaling continuous functions preserves their order

B. Positive functionals are integrals

6 declarations

instance

Non-negative Scaling Preserves Pointwise Order in C(X,R)C(X, \mathbb{R})

Let XX be a topological space and C(X,R)C(X, \mathbb{R}) be the space of continuous real-valued functions on XX. For any non-negative real number c∈Rc \in \mathbb{R} (where c≥0c \ge 0) and any two functions f,g∈C(X,R)f, g \in C(X, \mathbb{R}), if f≤gf \le g pointwise, then c⋅f≤c⋅gc \cdot f \le c \cdot g pointwise. This confirms that scaling continuous functions by a non-negative scalar preserves their pointwise ordering.

theorem

Positivity of ϕ\phi relative to TT implies ker⁡T⊆ker⁡ϕ\ker T \subseteq \ker \phi

Let VV be a vector space and C(X,R)C(X, \mathbb{R}) be the space of continuous real-valued functions on a topological space XX. Suppose T:V→C(X,R)T : V \to C(X, \mathbb{R}) is a linear map and ϕ:V→R\phi : V \to \mathbb{R} is a linear functional. If ϕ\phi is positive with respect to TT (meaning that for all v∈Vv \in V, T(v)≥0T(v) \geq 0 implies ϕ(v)≥0\phi(v) \geq 0), then the kernel of TT is a subset of the kernel of ϕ\phi, denoted as ker⁡T⊆ker⁡ϕ\ker T \subseteq \ker \phi.

definition

Linear functional on range(T)\text{range}(T) induced by ϕ\phi

Let XX be a topological space and VV be a real vector space. Suppose T:V→C(X,R)T : V \to C(X, \mathbb{R}) is a linear map and ϕ:V→R\phi : V \to \mathbb{R} is a linear functional such that ϕ\phi is positive with respect to TT (i.e., for any v∈Vv \in V, Tv≥0T v \ge 0 implies ϕv≥0\phi v \ge 0). The `rangeFunctional` is the linear map defined from the subspace range(T)⊆C(X,R)\text{range}(T) \subseteq C(X, \mathbb{R}) to R\mathbb{R} that maps TvT v to ϕv\phi v. This map is well-defined because the positivity condition ensures that the kernel of TT is contained in the kernel of ϕ\phi.

theorem

The induced functional LL on range(T)\text{range}(T) satisfies L(Tv)=ϕvL(T v) = \phi v

Let XX be a topological space and VV be a real vector space. Suppose T:V→C(X,R)T : V \to C(X, \mathbb{R}) is a linear map and ϕ:V→R\phi : V \to \mathbb{R} is a linear functional that is positive with respect to TT (that is, for any v∈Vv \in V, Tv≥0T v \ge 0 implies ϕv≥0\phi v \ge 0). Let L:range(T)→RL : \text{range}(T) \to \mathbb{R} be the linear functional on the subspace range(T)⊆C(X,R)\text{range}(T) \subseteq C(X, \mathbb{R}) induced by ϕ\phi. For any v∈Vv \in V, the value of LL applied to the image TvT v is equal to ϕv\phi v.

theorem

Existence of a positive linear extension to C(X,R)C(X, \mathbb{R})

Let XX be a compact space and VV be a real vector space. Suppose T:V→C(X,R)T : V \to C(X, \mathbb{R}) is a linear map and ϕ:V→R\phi : V \to \mathbb{R} is a linear functional. There exists a linear functional Λ:C(X,R)→R\Lambda : C(X, \mathbb{R}) \to \mathbb{R} such that Λ(Tv)=ϕv\Lambda(T v) = \phi v for all v∈Vv \in V, and Λ\Lambda is positive, meaning that for any g∈C(X,R)g \in C(X, \mathbb{R}), if g≥0g \ge 0, then Λg≥0\Lambda g \ge 0.

theorem

Positive linear functionals are integrals against regular probability measures

Let XX be a compact space and VV be a real vector space. Let T:V→C(X,R)T : V \to C(X, \mathbb{R}) be a linear map into the space of continuous functions on XX, and let ϕ:V→R\phi : V \to \mathbb{R} be a linear functional. Suppose ϕ\phi is positive with respect to TT (i.e., ϕ(v)≥0\phi(v) \ge 0 whenever T(v)≥0T(v) \ge 0 pointwise) and there exists an element one∈V\text{one} \in V such that T(one)=1T(\text{one}) = 1 (the constant function) and ϕ(one)=1\phi(\text{one}) = 1. Then there exists a regular probability measure μ\mu on XX such that for every v∈Vv \in V, the integral of T(v)T(v) with respect to μ\mu equals ϕ(v)\phi(v): ∫XT(v) dμ=ϕ(v)\int_X T(v) \, d\mu = \phi(v)