Documentation

Mathlib.MeasureTheory.Integral.CompactlySupported

Integrating compactly supported continuous functions #

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

source
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) μ
source
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, ℝ).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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 ∂μ
    source
    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).

    Equations
    Instances For
      source
      @[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) ∂μ, ⋯⟩