Theorems · Theorem · measure theory

exists_lt_rieszContentAux_add_pos

∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [T2Space X] [LocallyCompactSpace X] (K : TopologicalSpace.Compacts X) {ε : NNReal},
  0 < ε → ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

The Riesz content can be approximated arbitrarily well by evaluating the positive linear functional on test functions: for any ε > 0, there exists a compactly supported continuous nonnegative function f on X such that f ≥ 1 on K and such that λ(K) ≤ Λ f < λ(K) + ε.

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceLocallyCompactSpace