Theorems · Theorem · measure theory

RealRMK.measure_le_of_isCompact_of_integral

∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [inst_2 : MeasurableSpace X] [BorelSpace X]
  {μ ν : MeasureTheory.Measure X} [LocallyCompactSpace X] [ν.OuterRegular] [MeasureTheory.IsFiniteMeasureOnCompacts ν]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  (∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν) →
    ∀ ⦃K : Set X⦄, IsCompact K → μ K ≤ ν K

Note: the assumption IsFiniteMeasureOnCompacts μ cannot be removed. For example, if μ is infinite on any nonempty set and ν = 0, then the hypotheses are satisfied.

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceMeasurableSpaceBorelSpaceLocallyCompactSpaceMeasureTheory.Measure.OuterRegularMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.IsFiniteMeasureOnCompacts