Integrating compactly supported continuous functions

This file contains definitions and lemmas related to integrals of compactly supported continuous functions.

theorem CompactlySupportedContinuousMap.integrable {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {E : Type u_2} [NormedAddCommGroup E] (f : CompactlySupportedContinuousMap X E) {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.Integrable (⇑f) μ

noncomputable def CompactlySupportedContinuousMap.integralPositiveLinearMap {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

Integral as a positive linear functional on C_c(X, ℝ).

@[simp]

theorem CompactlySupportedContinuousMap.integralPositiveLinearMap_toFun {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap X ℝ) : (integralPositiveLinearMap μ) f = ∫ (x : X), f x ∂μ

noncomputable def CompactlySupportedContinuousMap.integralLinearMap {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal

Integration as a positive linear functional on C_c(X, ℝ≥0).

@[simp]

theorem CompactlySupportedContinuousMap.integralLinearMap_apply {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap X NNReal) : (integralLinearMap μ) f = ⟨∫ (x : X), ↑(f x) ∂μ, ⋯⟩