Integrals of continuous functions on a compact space

On a compact space X, every continuous function is integrable against a finite measure (Continuous.integrable_of_compactSpace, ContinuousMap.integrable), as is its product with an integrable function against any measure (MeasureTheory.Integrable.mul_continuous_of_compactSpace), and integration against a finite measure is Lipschitz, hence continuous, in the integrand for the sup norm on C(X, E). This is what lets an identity between integrals pass from a dense subset of C(X, E) to all of it.

For 𝕜 = ℝ or ℂ, integration against a finite measure is a positive linear functional on C(X, 𝕜) (ContinuousMap.integralPositiveLinearMap), the compact-space, 𝕜-valued counterpart of Mathlib's CompactlySupportedContinuousMap.integralPositiveLinearMap. For 𝕜 = ℂ it is a positive functional on the commutative C⋆-algebra C(X, ℂ), and a state when the measure is a probability measure.

A 𝕜-linear functional on C(X, 𝕜) that agrees with integration on real functions agrees with it everywhere (LinearMap.apply_eq_integral_of_forall_realToRCLike), since every f : C(X, 𝕜) is re f + i im f. This turns a Riesz–Markov–Kakutani measure of a real positive functional into a representation of its complexification.

theorem Continuous.integrable_of_compactSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {E : Type u_2} [NormedAddCommGroup E] {f : X → E} (hf : Continuous f) {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable f μ

On a compact space, a continuous function is integrable against every finite measure.

theorem ContinuousMap.integrable {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {E : Type u_2} [NormedAddCommGroup E] (f : C(X, E)) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (⇑f) μ

On a compact space, a continuous function is integrable against every finite measure.

theorem MeasureTheory.Integrable.mul_continuous_of_compactSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {𝕜 : Type u_2} [NormedRing 𝕜] {φ f : X → 𝕜} {μ : Measure X} (hφ : Integrable φ μ) (hf : Continuous f) : Integrable (fun (x : X) => φ x * f x) μ

On a compact space, the product of an integrable function with a continuous function is integrable.

noncomputable def ContinuousMap.integralPositiveLinearMap {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [RCLike 𝕜] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : C(X, 𝕜) →ₚ[𝕜] 𝕜

Integration against a finite measure on a compact space, as a positive linear functional on C(X, 𝕜).

@[simp]

theorem ContinuousMap.integralPositiveLinearMap_apply {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [RCLike 𝕜] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : C(X, 𝕜)) : (integralPositiveLinearMap μ) f = ∫ (x : X), f x ∂μ

ContinuousMap.integralPositiveLinearMap μ integrates against μ.

theorem ContinuousMap.integralPositiveLinearMap_one {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [RCLike 𝕜] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : (integralPositiveLinearMap μ) 1 = ↑(μ.real Set.univ)

Integration against μ sends the constant function 1 to the total mass of μ, so it is a state exactly when μ is a probability measure.

theorem LinearMap.apply_eq_integral_of_forall_realToRCLike {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [RCLike 𝕜] (φ : C(X, 𝕜) →ₗ[𝕜] 𝕜) {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (g : C(X, ℝ)), φ (ContinuousMap.realToRCLike 𝕜 g) = ↑(∫ (x : X), g x ∂μ)) (f : C(X, 𝕜)) : φ f = ∫ (x : X), f x ∂μ

On a compact space, a 𝕜-linear functional φ on C(X, 𝕜) that agrees with integration against a finite measure μ on real functions is integration against μ.

theorem TauCeti.continuous_integral_continuousMap {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] : Continuous fun (f : C(X, E)) => ∫ (x : X), f x ∂μ

On a compact space, integration against a finite measure is a continuous function of the integrand for the topology of uniform convergence on C(X, E).