Theorems · Definition · measure theory

RealRMK.rieszMeasure

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    [T2Space X] →
      [inst_2 : MeasurableSpace X] →
        [BorelSpace X] →
          (CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) → [LocallyCompactSpace X] → MeasureTheory.Measure X

The measure induced for Real-linear positive functional Λ, defined through toNNRealLinear and the NNReal-version of rieszContent. This is under the namespace RealRMK, while rieszMeasure without namespace is for NNReal-linear Λ.

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Cited by

8 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT2SpaceMeasurableSpaceBorelSpaceLocallyCompactSpace