Pavings and compact systems

A paving of a type 𝓧 is a set of sets of 𝓧, p : Set (Set 𝓧). This file gathers the facts about pavings and compact systems (IsCompactSystem, from Mathlib) that are needed to define analytic sets with respect to a paving and to prove Choquet's capacitability theorem.

Main definitions

• MeasureTheory.prodSigmaDelta p q: the countable intersections of countable unions of products A ×ˢ K with A ∈ p and K ∈ q.

Main statements

• isCompactSystem_finite: the finite sets form a compact system.
• IsCompactSystem.univ_sigma: compact systems on the fibers of a sigma type over a finite index type give a compact system on the sigma type.
• IsCompactSystem.image: the image of a compact system by a map f is a compact system if its sets are saturated for f.
• IsCompactSystem.fst_image_iInter: if q is a compact system, the projection on the first coordinate commutes with the intersection of a decreasing sequence of finite unions of products A ×ˢ K with K ∈ q.

Implementation notes

We use IsCompactSystem, which corresponds to the semi-compact pavings of Dellacherie and Meyer, rather than compact pavings (the same notion with arbitrary intersections instead of countable ones): this is sufficient for our applications and easier to work with.

References

• [S. He, J. Wang and J. Yan, Semimartingale theory and stochastic calculus][he2019semimartingale]

Auxiliary lemmas about sets and pavings

theorem Set.iInter_prod {α : Type u_6} {β : Type u_7} {ι : Type u_8} {s : Set α} {t : ι → Set β} [hι : Nonempty ι] : (⋂ (i : ι), t i) ×ˢ s = ⋂ (i : ι), t i ×ˢ s

theorem mem_supClosure_set_iff {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ supClosure S ↔ ∃ (L : Finset (Set α)), L.Nonempty ∧ s = ⋃₀ ↑L ∧ ↑L ⊆ S

theorem mem_infClosure_set_iff {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ infClosure S ↔ ∃ (L : Finset (Set α)), L.Nonempty ∧ s = ⋂₀ ↑L ∧ ↑L ⊆ S

theorem mem_supClosure_set_iff' {α : Type u_6} {S : Set (Set α)} (s : Set α) : s ∈ supClosure S ↔ ∃ (t : Finset ℕ) (_ : t.Nonempty) (A : ℕ → Set α), (∀ n ∈ t, A n ∈ S) ∧ s = ⋃ n ∈ t, A n

theorem biUnion_finset_mem_supClosure {ι : Type u_5} {α : Type u_6} {S : Set (Set α)} {s : Finset ι} (hs_nonempty : s.Nonempty) {A : ι → Set α} (hs : ∀ i ∈ s, A i ∈ S) : ⋃ i ∈ s, A i ∈ supClosure S

theorem isCompactSystem_singleton_empty {α : Type u_6} : IsCompactSystem {∅}

theorem isCompactSystem_Icc (α : Type u_6) [TopologicalSpace α] [T2Space α] [Preorder α] [CompactIccSpace α] : IsCompactSystem {t : Set α | ∃ (a : α) (b : α), Set.Icc a b = t}

theorem isCompactSystem_insert_empty_Icc (α : Type u_6) [TopologicalSpace α] [T2Space α] [Preorder α] [CompactIccSpace α] : IsCompactSystem (insert ∅ {t : Set α | ∃ (a : α) (b : α), Set.Icc a b = t})

theorem infClosed_insert_empty_Icc {ι : Type u_6} [LinearOrder ι] : InfClosed (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})

theorem isCompactSystem_finite (𝓚 : Type u_6) : IsCompactSystem {t : Set 𝓚 | t.Finite}

The finite sets form a compact system.

theorem IsCompactSystem.preimage_of_surjective {𝓚 : Type u_3} {𝓚' : Type u_4} {f : 𝓚' → 𝓚} (hf : Function.Surjective f) {S : Set (Set 𝓚')} (hS : IsCompactSystem S) : IsCompactSystem {t : Set 𝓚 | f ⁻¹' t ∈ S}

The preimage of a compact system by a surjective map is a compact system.

theorem IsCompactSystem.image {α : Type u_6} {β : Type u_7} {f : α → β} {S : Set (Set α)} (hS : IsCompactSystem S) (hf : ∀ K ∈ S, f ⁻¹' f '' K = K) : IsCompactSystem ((fun (x : Set α) => f '' x) '' S)

The image of a compact system by a map f is a compact system if each of its sets is the preimage by f of its image.

theorem Set.iInter_sigma_eq_empty_iff {ι : Type u_5} {𝓚 : ι → Type u_6} {β : Type u_7} (s : β → Set ι) (f : β → (i : ι) → Set (𝓚 i)) : ⋂ (b : β), (s b).sigma (f b) = ∅ ↔ ∀ i ∈ ⋂ (b : β), s b, ⋂ (b : β), f b i = ∅

theorem Set.iInter₂_sigma_eq_empty_iff {ι : Type u_5} {𝓚 : ι → Type u_6} {β : Type u_7} {p : β → Prop} (s : β → Set ι) (f : β → (i : ι) → Set (𝓚 i)) : ⋂ (b : β), ⋂ (_ : p b), (s b).sigma (f b) = ∅ ↔ ∀ i ∈ ⋂ (b : β), ⋂ (_ : p b), s b, ⋂ (b : β), ⋂ (_ : p b), f b i = ∅

Variant with an additional condition p b (e.g. b ≤ n for dissipate).

theorem IsCompactSystem.univ_sigma {ι : Type u_5} [Finite ι] {𝓚 : ι → Type u_6} {q : (i : ι) → Set (Set (𝓚 i))} (hq : ∀ (i : ι), IsCompactSystem (q i)) : IsCompactSystem (Set.univ.sigma '' Set.univ.pi q)

Variant of IsCompactSystem.sigma for a finite index type, with sets above all indices.

theorem InfClosed.image2_prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp_inter : InfClosed p) (hq_inter : InfClosed q) : InfClosed (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q)

The products A ×ˢ K with A ∈ p and K ∈ q form an inf-closed paving if p and q are inf-closed.

def MeasureTheory.prodSigmaDelta {𝓧 : Type u_1} {𝓚 : Type u_3} (p : Set (Set 𝓧)) (q : Set (Set 𝓚)) : Set (Set (𝓧 × 𝓚))

The paving of countable intersections of countable unions of products A ×ˢ K with A ∈ p and K ∈ q. See mem_prodSigmaDelta_iff.

Equations

• MeasureTheory.prodSigmaDelta p q = countableInfClosure (countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q))

theorem MeasureTheory.mem_countableSupClosure_image2_prod_iff {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set (𝓧 × 𝓚)} : s ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) ↔ ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), A n ∈ p) ∧ ∃ (K : ℕ → Set 𝓚), (∀ (n : ℕ), K n ∈ q) ∧ ⋃ (n : ℕ), A n ×ˢ K n = s

theorem MeasureTheory.mem_prodSigmaDelta_iff {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set (𝓧 × 𝓚)} : s ∈ prodSigmaDelta p q ↔ ∃ (A : ℕ → ℕ → Set 𝓧), (∀ (n m : ℕ), A n m ∈ p) ∧ ∃ (K : ℕ → ℕ → Set 𝓚), (∀ (n m : ℕ), K n m ∈ q) ∧ ⋂ (n : ℕ), ⋃ (m : ℕ), A n m ×ˢ K n m = s

theorem MeasureTheory.prod_mem_prodSigmaDelta {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {s : Set 𝓧} {t : Set 𝓚} (hs : s ∈ p) (ht : t ∈ q) : s ×ˢ t ∈ prodSigmaDelta p q

theorem MeasureTheory.prodSigmaDelta_mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {p' : Set (Set 𝓧)} {q' : Set (Set 𝓚)} (hp : p ⊆ p') (hq : q ⊆ q') : prodSigmaDelta p q ⊆ prodSigmaDelta p' q'

theorem MeasureTheory.countableInfClosed_prodSigmaDelta {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} : CountableInfClosed (prodSigmaDelta p q)

theorem MeasureTheory.preimage_prodMap_mem_prodSigmaDelta {𝓧 : Type u_1} {𝓨 : Type u_2} {𝓚 : Type u_3} {𝓚' : Type u_4} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} {g : 𝓨 → 𝓧} {f : 𝓚' → 𝓚} {t : Set (𝓧 × 𝓚)} (ht : t ∈ prodSigmaDelta p q) : Prod.map g f ⁻¹' t ∈ prodSigmaDelta ((fun (x : Set 𝓧) => g ⁻¹' x) '' p) ((fun (x : Set 𝓚) => f ⁻¹' x) '' q)

The preimage of a set of prodSigmaDelta p q by Prod.map g f belongs to the prodSigmaDelta of the preimage pavings.

theorem SupClosed.mem_countableSupClosure_iff_monotone {α : Type u_6} [CompleteLattice α] {S : Set α} {a : α} (hS : SupClosed S) : a ∈ countableSupClosure S ↔ ∃ (t : ℕ → α), (∀ (n : ℕ), t n ∈ S) ∧ Monotone t ∧ ⨆ (n : ℕ), t n = a

If S is closed under binary suprema, the elements of its countable supremum closure are the suprema of monotone sequences of elements of S.

theorem InfClosed.mem_countableInfClosure_iff_antitone {α : Type u_6} [CompleteLattice α] {S : Set α} {a : α} (hS : InfClosed S) : a ∈ countableInfClosure S ↔ ∃ (t : ℕ → α), (∀ (n : ℕ), t n ∈ S) ∧ Antitone t ∧ ⨅ (n : ℕ), t n = a

If S is closed under binary infima, the elements of its countable infimum closure are the infima of antitone sequences of elements of S.

theorem MeasureTheory.fst_image_mem_of_mem_supClosure_image2_prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hp_empty : ∅ ∈ p) (hp_union : SupClosed p) {s : Set (𝓧 × 𝓚)} (hs : s ∈ supClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q)) : Prod.fst '' s ∈ p

If p is closed under binary unions and contains ∅, then the projection on the first coordinate of a finite union of products A ×ˢ K with A ∈ p is in p.

theorem IsCompactSystem.fst_image_iInter {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hq : IsCompactSystem q) {B : ℕ → Set (𝓧 × 𝓚)} (hB_anti : Antitone B) (hB : ∀ (n : ℕ), B n ∈ supClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q)) : Prod.fst '' ⋂ (n : ℕ), B n = ⋂ (n : ℕ), Prod.fst '' B n

If q is a compact system, the projection on the first coordinate commutes with the intersection of a decreasing sequence of finite unions of products A ×ˢ K with K ∈ q.

This is equation (35.1) in the proof of Theorem 1.35 of [he2019semimartingale].