Measures vanishing on a set form a face

Among the measures in any set C of measures, those giving mass zero to a fixed set t form a face of C: a convex combination with positive weights vanishes on t only when both of its ends do. Mathlib's IsExtreme.extremePoints_eq then reads the extreme points of the face off those of C, which is how extremality among the laws carried by a set (vanishing on its complement) reduces to extremality among all of C. When C is convex so is the face.

Main results

• TauCeti.MeasureTheory.isExtreme_setOf_measure_eq_zero — the measures in C vanishing on t are a face of C.
• TauCeti.MeasureTheory.extremePoints_setOf_measure_eq_zero — their extreme points are the extreme points of C vanishing on t.
• TauCeti.MeasureTheory.Convex.setOf_measure_eq_zero — the face of a convex set is convex.

theorem TauCeti.MeasureTheory.isExtreme_setOf_measure_eq_zero {α : Type u_1} [MeasurableSpace α] (C : Set (MeasureTheory.Measure α)) (t : Set α) : IsExtreme ENNReal C {μ : MeasureTheory.Measure α | μ ∈ C ∧ μ t = 0}

Among the measures in a set C, those vanishing on t form a face: neither end of a convex combination with positive weights can charge t when the combination does not.

theorem TauCeti.MeasureTheory.extremePoints_setOf_measure_eq_zero {α : Type u_1} [MeasurableSpace α] (C : Set (MeasureTheory.Measure α)) (t : Set α) : Set.extremePoints ENNReal {μ : MeasureTheory.Measure α | μ ∈ C ∧ μ t = 0} = {μ : MeasureTheory.Measure α | μ ∈ C ∧ μ t = 0} ∩ Set.extremePoints ENNReal C

The extreme points of the measures in C vanishing on t are the extreme points of C vanishing on t.

theorem Convex.setOf_measure_eq_zero {α : Type u_1} [MeasurableSpace α] {C : Set (MeasureTheory.Measure α)} (hC : Convex ENNReal C) (t : Set α) : Convex ENNReal {μ : MeasureTheory.Measure α | μ ∈ C ∧ μ t = 0}

The measures in a convex set vanishing on t form a convex set.