Theorems · Definition · measure theory

rieszContentAux

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    (CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) → TopologicalSpace.Compacts X → NNReal

Given a positive linear functional Λ on continuous compactly supported functions on X with values in ℝ≥0, for K ⊆ X compact define λ(K) = inf {Λf | 1≤f on K}. When X is a locally compact T2 space, this will be shown to be a content, and will be shown to agree with the Riesz measure on the compact subsets K ⊆ X.

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpace