Choquet capacities and the capacitability theorem

A capacity for a paving p is a monotone set function m : Set 𝓧 → ℝ≥0∞ that is continuous along increasing sequences of sets, and along decreasing sequences of sets of p. A set s is capacitable if m s is the supremum of m t over the sets t ⊆ s that are countable intersections of sets of p.

Main definitions

• MeasureTheory.Capacity p: capacities for the paving p.
• MeasureTheory.Measure.capacity: the capacity defined by a finite measure.
• MeasureTheory.Capacity.compFst: the composition of a capacity with the projection Prod.fst.
• MeasureTheory.IsCapacitable m s: the set s is capacitable for the capacity m.

Main statements

• MeasureTheory.IsPavingAnalytic.isCapacitable: Choquet's capacitability theorem. If the paving p contains ∅ and is closed under binary unions and intersections, then every analytic set for p is capacitable for every capacity for p.
• MeasureTheory.IsPavingAnalytic.nullMeasurableSet: a set that is analytic for the paving of measurable sets is null-measurable for every s-finite measure.
• MeasurableSet.nullMeasurableSet_fst: measurable projection theorem. The projection of a measurable set of 𝓧 × 𝓨, with 𝓨 a standard Borel space, is null-measurable for every s-finite measure on 𝓧.

References

• [K. Bichteler, Stochastic integration with jumps][bichteler2002stochastic]
• [S. He, J. Wang and J. Yan, Semimartingale theory and stochastic calculus][he2019semimartingale]

structure MeasureTheory.Capacity {𝓧 : Type u_1} (p : Set (Set 𝓧)) : 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 : ℕ), f n ∈ p) → self.capacityOf (⋂ (n : ℕ), f n) = ⨅ (n : ℕ), self.capacityOf (f n)

@[instance_reducible]

instance MeasureTheory.Capacity.instFunLikeSetENNReal {𝓧 : Type u_1} {p : Set (Set 𝓧)} : 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 (Set 𝓧)} (m : Capacity p) : m.capacityOf = ⇑m

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

theorem MeasureTheory.capacity_iUnion {𝓧 : Type u_1} {p : Set (Set 𝓧)} {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 (Set 𝓧)} {f : ℕ → Set 𝓧} {m : Capacity p} (hf : Antitone f) (hp : ∀ (n : ℕ), f n ∈ p) : m (⋂ (n : ℕ), f n) = ⨅ (n : ℕ), m (f n)

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

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.compFst {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp_empty : ∅ ∈ p) (hp_union : SupClosed p) (m : Capacity p) (hq : IsCompactSystem q) : Capacity (supClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q))

The capacity obtained by composition of a capacity with the projection Prod.fst, for the paving of finite unions of products A ×ˢ K with A ∈ p and K in a compact system q. See Theorem A.5.8 (ii) of [bichteler2002stochastic] and Theorem 1.35 of [he2019semimartingale].

Equations

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

theorem MeasureTheory.Capacity.compFst_apply {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {hp_empty : ∅ ∈ p} {hp_union : SupClosed p} (m : Capacity p) {hq : IsCompactSystem q} (s : Set (𝓧 × 𝓚)) : (compFst hp_empty hp_union m hq) s = m (Prod.fst '' s)

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

A set s is capacitable for a capacity m for the paving p if m s can be approximated from below by the capacity of subsets of s that are countable intersections of sets of p: m s is the supremum of m t over the sets t ⊆ s in countableInfClosure p.

Equations

• MeasureTheory.IsCapacitable m s = ∀ a < m s, ∃ t ∈ countableInfClosure p, t ⊆ s ∧ a ≤ m t

theorem MeasureTheory.isCapacitable_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {m : Capacity p} (hs : s ∈ p) : IsCapacitable m s

theorem MeasureTheory.isCapacitable_of_mem_countableInfClosure_countableSupClosure {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (m : Capacity p) (hp_inter : InfClosed p) (hp_union : SupClosed p) (hs : s ∈ countableInfClosure (countableSupClosure p)) : IsCapacitable m s

If p is closed under binary unions and intersections, then every countable intersection of countable unions of sets of p is capacitable. This is Theorem 1.34 of [he2019semimartingale].

theorem MeasureTheory.fst_image_mem_countableInfClosure {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set (𝓧 × 𝓚)} (hp_empty : ∅ ∈ p) (hp_inter : InfClosed p) (hp_union : SupClosed p) (hq_inter : InfClosed q) (hq : IsCompactSystem q) (hs : s ∈ countableInfClosure (supClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q))) : Prod.fst '' s ∈ countableInfClosure p

If p is closed under binary unions and intersections, and q under binary intersections, then the projection of a set of countableInfClosure (supClosure (p × q)) is in countableInfClosure p.

theorem MeasureTheory.IsCapacitable.fst {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp_empty : ∅ ∈ p) (hp_inter : InfClosed p) (hp_union : SupClosed p) (m : Capacity p) (hq_inter : InfClosed q) (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsCapacitable (Capacity.compFst hp_empty hp_union m hq) s) : IsCapacitable m (Prod.fst '' s)

If a set s of 𝓧 × 𝓚 is capacitable for the capacity m.compFst, then its projection is capacitable for m.

theorem MeasureTheory.IsPavingAnalyticFor.isCapacitable {𝓧 : Type u_1} {𝓚 : Type u_2} {p : Set (Set 𝓧)} {s : Set 𝓧} {m : Capacity p} (hp_empty : ∅ ∈ p) (hp_inter : InfClosed p) (hp_union : SupClosed p) (hs : IsPavingAnalyticFor p 𝓚 s) : IsCapacitable m s

Choquet's capacitability theorem, for a set that is analytic with auxiliary space 𝓚.

theorem MeasureTheory.IsPavingAnalytic.isCapacitable {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {m : Capacity p} (hp_empty : ∅ ∈ p) (hp_inter : InfClosed p) (hp_union : SupClosed p) (hs : IsPavingAnalytic p s) : IsCapacitable m s

Choquet's capacitability theorem. If the paving p contains ∅ and is closed under binary unions and intersections, then every analytic set for p is capacitable for every capacity for p.

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

For the capacity defined by a finite measure, the capacitable sets are the null-measurable sets.

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

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

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

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

theorem MeasureTheory.IsPavingAnalytic.nullMeasurableSet_fst {𝓧 : Type u_1} {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [CompactIccSpace ι] {mι : MeasurableSpace ι} [BorelSpace ι] {m𝓧 : MeasurableSpace 𝓧} {s : Set (𝓧 × ι)} (hs : IsPavingAnalytic {t : Set (𝓧 × ι) | MeasurableSet t} s) (μ : Measure 𝓧) [SFinite μ] : NullMeasurableSet (Prod.fst '' s) μ

The projection of an analytic set of 𝓧 × ι is null-measurable with respect to any s-finite measure.

theorem MeasureTheory.IsPavingAnalytic.nullMeasurableSet_snd {𝓧 : Type u_1} {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [CompactIccSpace ι] {mι : MeasurableSpace ι} [BorelSpace ι] {m𝓧 : MeasurableSpace 𝓧} {s : Set (ι × 𝓧)} (hs : IsPavingAnalytic {t : Set (ι × 𝓧) | MeasurableSet t} s) (μ : Measure 𝓧) [SFinite μ] : NullMeasurableSet (Prod.snd '' s) μ

The projection of an analytic set of ι × 𝓧 is null-measurable with respect to any s-finite measure.

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

The projection of a measurably analytic set of 𝓧 × 𝓨, with 𝓨 a standard Borel space, is null-measurable with respect to any s-finite measure.

theorem MeasureTheory.IsMeasurableAnalytic.nullMeasurableSet_snd {𝓧 : Type u_1} {𝓨 : Type u_3} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] {s : Set (𝓨 × 𝓧)} (hs : IsMeasurableAnalytic s) (μ : Measure 𝓧) [SFinite μ] : NullMeasurableSet (Prod.snd '' s) μ

The projection of a measurably analytic set of 𝓨 × 𝓧, with 𝓨 a standard Borel space, is null-measurable with respect to any s-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.SFinite μ] : MeasureTheory.NullMeasurableSet (Prod.fst '' s) μ

Measurable projection theorem: the projection of a measurable set is universally measurable (null-measurable with respect to any s-finite measure).

theorem MeasurableSet.nullMeasurableSet_snd {𝓧 : Type u_1} {𝓨 : Type u_3} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] {s : Set (𝓨 × 𝓧)} (hs : MeasurableSet s) (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.SFinite μ] : MeasureTheory.NullMeasurableSet (Prod.snd '' s) μ

Measurable projection theorem: the projection of a measurable set is universally measurable (null-measurable with respect to any s-finite measure).