Choquet capacity

structure MeasureTheory.Capacity {𝓧 : Type u_1} (p : Set 𝓧 → Prop) : Type u_1

A capacity is a set function that is monotone, continuous from above for decreasing sequences of sets satisfying p, and continuous from below for increasing sequences of sets.

Any finite measure defines a capacity, but capacities have only the monotonicity properties of measures. The notable difference is that a capacity is not additive.

• capacityOf : Set 𝓧 → ENNReal

  The set function associated with a capacity.

• mono' (s t : Set 𝓧) (hst : s ⊆ t) : self.capacityOf s ≤ self.capacityOf t
• capacityOf_iUnion (f : ℕ → Set 𝓧) : Monotone f → self.capacityOf (⋃ (n : ℕ), f n) = ⨆ (n : ℕ), self.capacityOf (f n)
• capacityOf_iInter (f : ℕ → Set 𝓧) : Antitone f → (∀ (n : ℕ), p (f n)) → self.capacityOf (⋂ (n : ℕ), f n) = ⨅ (n : ℕ), self.capacityOf (f n)

instance MeasureTheory.Capacity.instFunLikeSetENNReal {𝓧 : Type u_1} {p : Set 𝓧 → Prop} : FunLike (Capacity p) (Set 𝓧) ENNReal

Equations

• MeasureTheory.Capacity.instFunLikeSetENNReal = { coe := fun (m : MeasureTheory.Capacity p) => m.capacityOf, coe_injective' := ⋯ }

@[simp]

theorem MeasureTheory.Capacity.capacityOf_eq_coe {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (m : Capacity p) : m.capacityOf = ⇑m

theorem MeasureTheory.Capacity.mono {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (m : Capacity p) {s t : Set 𝓧} (hst : s ⊆ t) : m s ≤ m t

theorem MeasureTheory.capacity_iUnion {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {f : ℕ → Set 𝓧} {m : Capacity p} (hf : Monotone f) : m (⋃ (n : ℕ), f n) = ⨆ (n : ℕ), m (f n)

theorem MeasureTheory.capacity_iInter {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {f : ℕ → Set 𝓧} {m : Capacity p} (hf : Antitone f) (hp : ∀ (n : ℕ), p (f n)) : m (⋂ (n : ℕ), f n) = ⨅ (n : ℕ), m (f n)

def MeasureTheory.Measure.capacity {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) [IsFiniteMeasure μ] : Capacity MeasurableSet

The capacity defined by a finite measure.

Equations

• μ.capacity = { capacityOf := fun (s : Set 𝓧) => μ s, mono' := ⋯, capacityOf_iUnion := ⋯, capacityOf_iInter := ⋯ }

@[simp]

theorem MeasureTheory.Measure.capacity_apply {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) [IsFiniteMeasure μ] (s : Set 𝓧) : μ.capacity s = μ s

def MeasureTheory.Capacity.comp_fst {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} (hp_empty : p ∅) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (m : Capacity p) (hq : IsCompactSystem q) : Capacity (memFiniteUnion (memProd p q))

The capacity obtained by composition of a capacity with a projection.

Equations

• MeasureTheory.Capacity.comp_fst hp_empty hp_union m hq = { capacityOf := fun (s : Set (𝓧 × 𝓚)) => m (Prod.fst '' s), mono' := ⋯, capacityOf_iUnion := ⋯, capacityOf_iInter := ⋯ }

def MeasureTheory.IsCapacitable {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (m : Capacity p) (s : Set 𝓧) : Prop

A set s is capacitable for a capacity m for a property p if m s can be approximated from above by countable intersections of sets t n such that p (t n) and ⋂ n, t n ⊆ s.

Equations

• MeasureTheory.IsCapacitable m s = ∀ a < m s, ∃ (t : Set 𝓧), MeasureTheory.memDelta p t ∧ t ⊆ s ∧ a ≤ m t

theorem MeasureTheory.isCapacitable_of_prop {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} {m : Capacity p} (hs : p s) : IsCapacitable m s

theorem MeasureTheory.isCapacitable_memDelta_memSigma {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} (m : Capacity p) (hp_empty : p ∅) (hp_inter : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (hs : memDelta (memSigma p) s) : IsCapacitable m s

theorem MeasureTheory.aux1 {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {s t : Set (𝓧 × 𝓚)} (hp_empty : p ∅) (hp_inter : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (hq_empty : q ∅) (hq_inter : ∀ (s t : Set 𝓚), q s → q t → q (s ∩ t)) (hq : IsCompactSystem q) (hs : memFiniteUnion (memProd p q) s) (ht : memFiniteUnion (memProd p q) t) : memFiniteUnion (memProd p q) (s ∩ t)

theorem MeasureTheory.memDelta_fst {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {s : Set (𝓧 × 𝓚)} (hp_empty : p ∅) (hp_inter : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (hq_empty : q ∅) (hq_inter : ∀ (s t : Set 𝓚), q s → q t → q (s ∩ t)) (hq : IsCompactSystem q) (hs : memDelta (memFiniteUnion (memProd p q)) s) : memDelta p (Prod.fst '' s)

theorem MeasureTheory.IsCapacitable.fst {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} (hp_empty : p ∅) (hp_inter : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (m : Capacity p) (hq_empty : q ∅) (hq_inter : ∀ (s t : Set 𝓚), q s → q t → q (s ∩ t)) (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsCapacitable (Capacity.comp_fst hp_empty hp_union m hq) s) : IsCapacitable m (Prod.fst '' s)

theorem MeasureTheory.IsPavingAnalyticFor.isCapacitable {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set 𝓧 → Prop} {s : Set 𝓧} {m : Capacity p} (hp_empty : p ∅) (hp_inter : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (hs : IsPavingAnalyticFor p 𝓚 s) : IsCapacitable m s

Choquet's capacitability theorem.

theorem MeasureTheory.IsPavingAnalytic.isCapacitable {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} {m : Capacity p} (hp_empty : p ∅) (hp_inter : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) (hp_union : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) (hs : IsPavingAnalytic p s) : IsCapacitable m s

Choquet's capacitability theorem. Every analytic set for a paving stable by intersection and union is capacitable.

theorem MeasureTheory.isCapacitable_measure_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) [IsFiniteMeasure μ] (s : Set 𝓧) : IsCapacitable μ.capacity s ↔ NullMeasurableSet s μ

theorem MeasureTheory.IsPavingAnalytic.nullMeasurableSet {𝓧 : Type u_1} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} (hs : IsPavingAnalytic MeasurableSet s) (μ : Measure 𝓧) [IsFiniteMeasure μ] : NullMeasurableSet s μ

An analytic set is universally measurable: it is null-measurable with respect to any finite measure.

theorem MeasureTheory.IsMeasurableAnalytic.nullMeasurableSet {𝓧 : Type u_1} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} (hs : IsMeasurableAnalytic s) (μ : Measure 𝓧) [IsFiniteMeasure μ] : NullMeasurableSet s μ

An analytic set is universally measurable: it is null-measurable with respect to any finite measure.

theorem MeasurableSet.nullMeasurableSet_fst {𝓧 : Type u_1} {𝓨 : Type u_3} {_m𝓧 : MeasurableSpace 𝓧} {_m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] {s : Set (𝓧 × 𝓨)} (hs : MeasurableSet s) (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.NullMeasurableSet (Prod.fst '' s) μ

Measurable projection theorem: the projection of a measurable set is universally measurable (null-measurable for any finite measure).