Theorems · Definition · measure theory

NNRealRMK.rieszMeasure

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    (CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) →
      [T2Space X] → [LocallyCompactSpace X] → [inst_3 : MeasurableSpace X] → [BorelSpace X] → MeasureTheory.Measure X

rieszContent gives a Content from Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0. Here rieszContent Λ is promoted to a measure. It will be later shown that ∫ (x : X), f x ∂(rieszMeasure Λ hΛ) = Λ f for all f : C_c(X, ℝ≥0).

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceLocallyCompactSpaceMeasurableSpaceBorelSpace