Measures supported on finite sets

For a measure that vanishes off a finite set, every set is null-measurable if singletons are measurable. Finite support is preserved by finite products of finite measures. These facts let sample-complexity arguments in learning theory measure failure events of arbitrary (non-measurable) learners under finitely supported adversarial distributions.

HasFiniteSupport records this property as a typeclass, with an instance for finite products.

The PFR project has an equivalent ProbabilityTheory.FiniteSupport class, expressed using an almost-everywhere Finset witness.

Main statements

• MeasureTheory.HasFiniteSupport: a measure vanishes off some finite set.
• MeasureTheory.HasFiniteSupport.exists_eq_sum_smul_dirac: on a space with measurable singletons, a measure with finite support is a finite sum of Dirac measures weighted by its singleton masses.
• MeasureTheory.HasFiniteSupport.isFiniteMeasure: a sigma-finite measure with finite support is finite.
• MeasureTheory.NullMeasurableSet.of_hasFiniteSupport: on a space with measurable singletons, every set is null-measurable for a measure with finite support, including finite products.

class MeasureTheory.HasFiniteSupport {α : Type u_1} [MeasurableSpace α] (μ : Measure α) : Prop

A measure vanishes off a finite set.

• exists_finite_measure_compl_zero : ∃ (s : Set α), s.Finite ∧ μ sᶜ = 0

  Some finite set has null complement.

theorem MeasureTheory.HasFiniteSupport.exists_eq_sum_smul_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [HasFiniteSupport μ] : ∃ (s : Finset α), μ = ∑ a ∈ s, μ {a} • Measure.dirac a

On a space with measurable singletons, a measure with finite support is a finite sum of Dirac measures weighted by its singleton masses. This is Measure.ae_mem_finset_iff applied to a finite support.

@[instance 100]

instance MeasureTheory.HasFiniteSupport.isFiniteMeasure {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [HasFiniteSupport μ] [SigmaFinite μ] : IsFiniteMeasure μ

A sigma-finite measure with finite support is finite.

theorem MeasureTheory.NullMeasurableSet.of_hasFiniteSupport {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {μ : Measure α} [HasFiniteSupport μ] (t : Set α) : NullMeasurableSet t μ

On a space with measurable singletons, every set is null-measurable for a measure with finite support.

instance MeasureTheory.instHasFiniteSupportForallPiOfIsFiniteMeasure {ι : Type u_1} [Fintype ι] {X : ι → Type u_2} [(i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → Measure (X i)) [∀ (i : ι), HasFiniteSupport (μ i)] [∀ (i : ι), IsFiniteMeasure (μ i)] : HasFiniteSupport (Measure.pi μ)