Analytic sets in the sense of a paved space

A paving of 𝓧 is a set of sets p : Set (Set 𝓧). A set s is analytic for p if it is the projection on 𝓧 of a set of 𝓧 × 𝓚 that is a countable intersection of countable unions of products A ×ˢ K with A ∈ p and K in a compact system of 𝓚.

Main definitions

• MeasureTheory.IsPavingAnalyticFor p 𝓚 s: s is analytic for the paving p, with an auxiliary space 𝓚.
• MeasureTheory.IsPavingAnalytic p s: s is analytic for the paving p.
• MeasureTheory.IsMeasurableAnalytic s: s is the projection of a measurable set of 𝓧 × ℝ.

Main statements

• MeasureTheory.IsPavingAnalyticFor.isPavingAnalyticFor_nat_nat: the auxiliary space in the definition of analytic sets can always be taken to be ℕ → ℕ.
• MeasureTheory.IsPavingAnalytic.iUnion, MeasureTheory.IsPavingAnalytic.iInter: analytic sets are stable by countable unions and intersections.
• MeasureTheory.IsPavingAnalytic.fst: the projection of an analytic set for a product paving p × q, with q a compact system, is analytic for p.
• MeasureTheory.isPavingAnalytic_isPavingAnalytic_iff: a set analytic for the paving of analytic sets is analytic.
• MeasureTheory.isPavingAnalytic_of_measurableSet_generateFrom: if the complement of every set of p is analytic, then every set of the σ-algebra generated by p is analytic.
• MeasurableSet.isPavingAnalytic_fst: the projection of a measurable set of 𝓧 × ℝ is analytic for the paving of measurable sets.

Implementation notes

In the definition of IsPavingAnalytic, the auxiliary space 𝓚 lives in Type, since we cannot quantify over universes. This is not a restriction: by IsPavingAnalyticFor.isPavingAnalyticFor_nat_nat, a set that is analytic with an auxiliary space in any universe is analytic with auxiliary space ℕ → ℕ.

Some references require the compact system q to contain ∅ and the auxiliary space 𝓚 to be nonempty. This gives the same notion: insert ∅ q is a compact system if q is one, and a set that is analytic with an empty auxiliary space is empty, hence analytic with any auxiliary space.

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

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

Auxiliary measure theory lemmas

theorem supClosed_measurableSet {α : Type u_6} [MeasurableSpace α] : SupClosed {t : Set α | MeasurableSet t}

theorem infClosed_measurableSet {α : Type u_6} [MeasurableSpace α] : InfClosed {t : Set α | MeasurableSet t}

theorem borel_eq_generateFrom_Icc' (α : Type u_6) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), Set.Icc l u = S}

theorem borel_eq_generateFrom_insert_empty_Icc (α : Type u_6) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (insert ∅ {S : Set α | ∃ (l : α) (u : α), Set.Icc l u = S})

theorem MeasurableSet.of_mem_countableInfClosure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {s : Set 𝓧} {p : Set (Set 𝓧)} (hs : s ∈ countableInfClosure p) (hp : ∀ t ∈ p, MeasurableSet t) : MeasurableSet s

theorem MeasurableSet.of_mem_countableSupClosure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {s : Set 𝓧} {p : Set (Set 𝓧)} (hs : s ∈ countableSupClosure p) (hp : ∀ t ∈ p, MeasurableSet t) : MeasurableSet s

theorem MeasurableSet.of_mem_supClosure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {s : Set 𝓧} {p : Set (Set 𝓧)} (hs : s ∈ supClosure p) (hp : ∀ t ∈ p, MeasurableSet t) : MeasurableSet s

theorem MeasurableSet.of_mem_image2_prod {Ω : Type u_6} {𝓧 : Type u_7} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {s : Set (𝓧 × Ω)} {p : Set (Set 𝓧)} {q : Set (Set Ω)} (hs : s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set Ω) => x1 ×ˢ x2) p q) (hp : ∀ t ∈ p, MeasurableSet t) (hq : ∀ t ∈ q, MeasurableSet t) : MeasurableSet s

def MeasureTheory.IsPavingAnalyticFor {𝓧 : Type u_1} (p : Set (Set 𝓧)) (𝓚 : Type u_6) (s : Set 𝓧) : Prop

A set s is analytic for a paving p and a type 𝓚 if there exists a compact system q of 𝓚 such that s is the projection of a set t ∈ prodSigmaDelta p q.

Equations

• MeasureTheory.IsPavingAnalyticFor p 𝓚 s = ∃ (q : Set (Set 𝓚)), IsCompactSystem q ∧ ∃ t ∈ MeasureTheory.prodSigmaDelta p q, s = Prod.fst '' t

def MeasureTheory.IsPavingAnalytic {𝓧 : Type u_1} (p : Set (Set 𝓧)) (s : Set 𝓧) : Prop

A set s is analytic for a paving p if there exists a type 𝓚 and a compact system q of 𝓚 such that s is the projection of a set t ∈ prodSigmaDelta p q.

Equations

• MeasureTheory.IsPavingAnalytic p s = ∃ (𝓚 : Type), MeasureTheory.IsPavingAnalyticFor p 𝓚 s

theorem MeasureTheory.IsPavingAnalyticFor.isPavingAnalyticFor_nat_nat {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalyticFor p (ℕ → ℕ) s

The auxiliary space in the definition of analytic sets can always be taken to be ℕ → ℕ.

theorem MeasureTheory.IsPavingAnalyticFor.isPavingAnalytic {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalytic p s

theorem MeasureTheory.isPavingAnalyticFor_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (𝓚 : Type u_6) [Nonempty 𝓚] (hs : s ∈ p) : IsPavingAnalyticFor p 𝓚 s

theorem MeasureTheory.isPavingAnalytic_of_mem {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : s ∈ p) : IsPavingAnalytic p s

theorem MeasureTheory.IsPavingAnalyticFor.mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hp : p ⊆ p') (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalyticFor p' 𝓚 s

theorem MeasureTheory.IsPavingAnalytic.mono {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hp : p ⊆ p') (hs : IsPavingAnalytic p s) : IsPavingAnalytic p' s

theorem MeasureTheory.IsPavingAnalyticFor.exists_mem_countableSupClosure_superset {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) : ∃ t ∈ countableSupClosure p, s ⊆ t

An analytic set for p is contained in a countable union of sets of p. See the paragraph after Definition 1.25 of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalyticFor_empty {𝓧 : Type u_1} {p : Set (Set 𝓧)} (𝓚 : Type u_6) (hp : p.Nonempty) : IsPavingAnalyticFor p 𝓚 ∅

@[simp]

theorem MeasureTheory.isPavingAnalytic_empty {𝓧 : Type u_1} {p : Set (Set 𝓧)} (hp : p.Nonempty) : IsPavingAnalytic p ∅

@[simp]

theorem MeasureTheory.isPavingAnalyticFor_iff_eq_empty {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} [IsEmpty 𝓚] (hp : p.Nonempty) : IsPavingAnalyticFor p 𝓚 s ↔ s = ∅

theorem MeasureTheory.IsPavingAnalyticFor.iInter {𝓧 : Type u_1} {ι : Type u_5} {p : Set (Set 𝓧)} [Countable ι] [Nonempty ι] {𝓚 : ι → Type u_6} {s : ι → Set 𝓧} (hs : ∀ (i : ι), IsPavingAnalyticFor p (𝓚 i) (s i)) : IsPavingAnalyticFor p ((i : ι) → 𝓚 i) (⋂ (i : ι), s i)

A countable intersection of analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalytic.iInter {𝓧 : Type u_1} {ι : Type u_5} {p : Set (Set 𝓧)} [Countable ι] [Nonempty ι] {s : ι → Set 𝓧} (hs : ∀ (i : ι), IsPavingAnalytic p (s i)) : IsPavingAnalytic p (⋂ (i : ι), s i)

A countable intersection of analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalyticFor.iUnion {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓚 : ℕ → Type u_6} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), IsPavingAnalyticFor p (𝓚 n) (s n)) : IsPavingAnalyticFor p ((n : ℕ) × 𝓚 n) (⋃ (n : ℕ), s n)

A countable union of analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalytic.iUnion {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : ℕ → Set 𝓧} (hs : ∀ (n : ℕ), IsPavingAnalytic p (s n)) : IsPavingAnalytic p (⋃ (n : ℕ), s n)

A countable union of analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalyticFor.inter {𝓧 : Type u_1} {𝓚 : Type u_3} {𝓚' : Type u_4} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : IsPavingAnalyticFor p 𝓚' t) : IsPavingAnalyticFor p (𝓚 × 𝓚') (s ∩ t)

The intersection of two analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalytic.inter {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : IsPavingAnalytic p s) (ht : IsPavingAnalytic p t) : IsPavingAnalytic p (s ∩ t)

The intersection of two analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalyticFor.union {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓚' : Type u_6} {t : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : IsPavingAnalyticFor p 𝓚' t) : IsPavingAnalyticFor p (𝓚 ⊕ 𝓚') (s ∪ t)

The union of two analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalytic.union {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s t : Set 𝓧} (hs : IsPavingAnalytic p s) (ht : IsPavingAnalytic p t) : IsPavingAnalytic p (s ∪ t)

The union of two analytic sets is analytic. Theorem 1.26 of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableInfClosure_of_imp {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableInfClosure p') (hqp : ∀ x ∈ p', IsPavingAnalyticFor p 𝓚 x) : IsPavingAnalyticFor p (ℕ → 𝓚) s

theorem MeasureTheory.isPavingAnalytic_of_mem_countableInfClosure_of_imp {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableInfClosure p') (hqp : ∀ x ∈ p', IsPavingAnalytic p x) : IsPavingAnalytic p s

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableSupClosure_of_imp {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableSupClosure p') (hqp : ∀ x ∈ p', IsPavingAnalyticFor p 𝓚 x) : IsPavingAnalyticFor p ((_ : ℕ) × 𝓚) s

theorem MeasureTheory.isPavingAnalytic_of_mem_countableSupClosure_of_imp {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {p' : Set (Set 𝓧)} (hs : s ∈ countableSupClosure p') (hqp : ∀ x ∈ p', IsPavingAnalytic p x) : IsPavingAnalytic p s

theorem MeasureTheory.IsPavingAnalyticFor.fst {𝓧 : Type u_1} {𝓚 : Type u_3} {𝓚' : Type u_4} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) 𝓚' s) : IsPavingAnalyticFor p (𝓚 × 𝓚') (Prod.fst '' s)

The projection of an analytic set for the paving p × q, with q a compact system, is analytic for p. This is Theorem 1.28 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalytic.fst {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {q : Set (Set 𝓚)} (hq : IsCompactSystem q) {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓚) => x1 ×ˢ x2) p q) s) : IsPavingAnalytic p (Prod.fst '' s)

The projection of an analytic set for the paving p × q, with q a compact system, is analytic for p. This is Theorem 1.28 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalyticFor.prod_left {𝓧 : Type u_1} {𝓨 : Type u_2} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {r : Set (Set 𝓨)} {t : Set 𝓨} (ht : t ∈ r) (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) 𝓚 (t ×ˢ s)

The product of an analytic set for p with a set of r is analytic for the product paving r × p.

theorem MeasureTheory.IsPavingAnalytic.prod_left {𝓧 : Type u_1} {𝓨 : Type u_2} {p : Set (Set 𝓧)} {s : Set 𝓧} {r : Set (Set 𝓨)} {t : Set 𝓨} (ht : t ∈ r) (hs : IsPavingAnalytic p s) : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) (t ×ˢ s)

The product of an analytic set for p with a set of r is analytic for the product paving r × p.

theorem MeasureTheory.IsPavingAnalyticFor.prod_right {𝓧 : Type u_1} {𝓨 : Type u_2} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {r : Set (Set 𝓨)} {t : Set 𝓨} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : t ∈ r) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) 𝓚 (s ×ˢ t)

The product of an analytic set for p with a set of r is analytic for the product paving p × r.

theorem MeasureTheory.IsPavingAnalytic.prod_right {𝓧 : Type u_1} {𝓨 : Type u_2} {p : Set (Set 𝓧)} {s : Set 𝓧} {r : Set (Set 𝓨)} {t : Set 𝓨} (hs : IsPavingAnalytic p s) (ht : t ∈ r) : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) (s ×ˢ t)

The product of an analytic set for p with a set of r is analytic for the product paving p × r.

theorem MeasureTheory.isPavingAnalyticFor_of_image2_prod_isPavingAnalyticFor_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set (𝓨 × 𝓧)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r {s : Set 𝓧 | IsPavingAnalyticFor p 𝓚 s}) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) 𝓚 t

theorem MeasureTheory.isPavingAnalytic_of_image2_prod_isPavingAnalytic_left {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set (𝓨 × 𝓧)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r {s : Set 𝓧 | IsPavingAnalytic p s}) : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) t

theorem MeasureTheory.isPavingAnalyticFor_of_image2_prod_isPavingAnalyticFor_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set (𝓧 × 𝓨)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) {s : Set 𝓧 | IsPavingAnalyticFor p 𝓚 s} r) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) 𝓚 t

theorem MeasureTheory.isPavingAnalytic_of_image2_prod_isPavingAnalytic_right {𝓧 : Type u_1} {p : Set (Set 𝓧)} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set (𝓧 × 𝓨)} (ht : t ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) {s : Set 𝓧 | IsPavingAnalytic p s} r) : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) t

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableSupClosure_image2_prod_isPavingAnalyticFor_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set (𝓨 × 𝓧)} (ht : t ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r {s : Set 𝓧 | IsPavingAnalyticFor p 𝓚 s})) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) ((_ : ℕ) × 𝓚) t

theorem MeasureTheory.isPavingAnalyticFor_of_mem_countableSupClosure_image2_prod_isPavingAnalyticFor_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set (𝓧 × 𝓨)} (ht : t ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) {s : Set 𝓧 | IsPavingAnalyticFor p 𝓚 s} r)) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) ((_ : ℕ) × 𝓚) t

theorem MeasureTheory.IsPavingAnalyticFor.prod_mem_countableSupClosure_left {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set 𝓨} (ht : t ∈ countableSupClosure r) (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) ((_ : ℕ) × 𝓚) (t ×ˢ s)

theorem MeasureTheory.IsPavingAnalyticFor.prod_mem_countableSupClosure_right {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set 𝓨} (hs : IsPavingAnalyticFor p 𝓚 s) (ht : t ∈ countableSupClosure r) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set 𝓨) => x1 ×ˢ x2) p r) ((_ : ℕ) × 𝓚) (s ×ˢ t)

theorem MeasureTheory.IsPavingAnalyticFor.prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_6} {𝓚' : Type u_7} {r : Set (Set 𝓨)} {t : Set 𝓨} (ht : IsPavingAnalyticFor r 𝓚' t) (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalyticFor (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) (((_ : ℕ) × 𝓚') × (_ : ℕ) × 𝓚) (t ×ˢ s)

The product of two analytic sets is analytic for the product paving. Theorem 1.27 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalytic.prod {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} {𝓨 : Type u_6} {r : Set (Set 𝓨)} {t : Set 𝓨} (ht : IsPavingAnalytic r t) (hs : IsPavingAnalytic p s) : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓨) (x2 : Set 𝓧) => x1 ×ˢ x2) r p) (t ×ˢ s)

The product of two analytic sets is analytic for the product paving. Theorem 1.27 of [he2019semimartingale].

theorem MeasureTheory.IsPavingAnalyticFor.image_of_injective {𝓧 : Type u_1} {𝓨 : Type u_2} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} {f : 𝓧 → 𝓨} (hf : Function.Injective f) (hs : IsPavingAnalyticFor p 𝓚 s) : IsPavingAnalyticFor ((fun (x : Set 𝓧) => f '' x) '' p) 𝓚 (f '' s)

The image of an analytic set by an injective map is analytic for the image paving.

theorem MeasureTheory.IsPavingAnalytic.image_of_injective {𝓧 : Type u_1} {𝓨 : Type u_2} {p : Set (Set 𝓧)} {s : Set 𝓧} {f : 𝓧 → 𝓨} (hf : Function.Injective f) (hs : IsPavingAnalytic p s) : IsPavingAnalytic ((fun (x : Set 𝓧) => f '' x) '' p) (f '' s)

The image of an analytic set by an injective map is analytic for the image paving.

theorem MeasureTheory.IsPavingAnalytic.image_measurableEmbedding {𝓧 : Type u_1} {𝓨 : Type u_2} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓧 → 𝓨} (hf : MeasurableEmbedding f) (hs : IsPavingAnalytic {t : Set 𝓧 | MeasurableSet t} s) : IsPavingAnalytic {t : Set 𝓨 | MeasurableSet t} (f '' s)

The image of a set that is analytic for the paving of measurable sets by a measurable embedding is analytic for the paving of measurable sets.

theorem MeasureTheory.IsPavingAnalytic.image_swap {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {s : Set (𝓧 × 𝓨)} (hs : IsPavingAnalytic {t : Set (𝓧 × 𝓨) | MeasurableSet t} s) : IsPavingAnalytic {t : Set (𝓨 × 𝓧) | MeasurableSet t} (Prod.swap '' s)

theorem MeasureTheory.isPavingAnalyticFor_isPavingAnalyticFor {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor {t : Set 𝓧 | IsPavingAnalyticFor p 𝓚 t} 𝓚 s) : IsPavingAnalyticFor p (𝓚 × (ℕ → (_ : ℕ) × 𝓚)) s

A set that is analytic for the paving of analytic sets is analytic. Theorem 1.29 of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalytic_isPavingAnalytic {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalytic {t : Set 𝓧 | IsPavingAnalytic p t} s) : IsPavingAnalytic p s

A set that is analytic for the paving of analytic sets is analytic. Theorem 1.29 of [he2019semimartingale].

@[simp]

theorem MeasureTheory.isPavingAnalytic_isPavingAnalytic_iff {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} : IsPavingAnalytic {t : Set 𝓧 | IsPavingAnalytic p t} s ↔ IsPavingAnalytic p s

A set is analytic for the paving of analytic sets if and only if it is analytic.

theorem MeasureTheory.IsPavingAnalyticFor.inter_set {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (hs : IsPavingAnalyticFor p 𝓚 s) (t : Set 𝓧) : IsPavingAnalyticFor {u : Set 𝓧 | ∃ v ∈ p, u = v ∩ t} 𝓚 (s ∩ t)

If s is analytic for p, then s ∩ t is analytic for the trace of p on t. Theorem 1.30 of [he2019semimartingale].

theorem MeasureTheory.exists_isPavingAnalyticFor_of_inter_set {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set (Set 𝓧)} {s : Set 𝓧} (t : Set 𝓧) (hs : IsPavingAnalyticFor {u : Set 𝓧 | ∃ v ∈ p, u = v ∩ t} 𝓚 s) : ∃ (s' : Set 𝓧), IsPavingAnalyticFor p 𝓚 s' ∧ s = s' ∩ t

A set that is analytic for the trace of p on t is the intersection with t of a set that is analytic for p. Theorem 1.30 of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalytic_of_measurableSet_generateFrom {𝓧 : Type u_1} {p : Set (Set 𝓧)} {s : Set 𝓧} (hp_nonempty : p.Nonempty) (hp : ∀ s ∈ p, IsPavingAnalytic p sᶜ) (hs : MeasurableSet s) : IsPavingAnalytic p s

If the complement of every set of p is analytic for p, then every set of the σ-algebra generated by p is analytic for p. This is Theorem 1.31 of [he2019semimartingale].

theorem MeasureTheory.Iic_mem_countableSupClosure_Icc {ι : Type u_6} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (u : ι) : Set.Iic u ∈ countableSupClosure {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}

theorem MeasureTheory.Ici_mem_countableSupClosure_Icc {ι : Type u_6} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (u : ι) : Set.Ici u ∈ countableSupClosure {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}

theorem MeasureTheory.Iio_mem_countableSupClosure_Icc {ι : Type u_6} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (u : ι) : Set.Iio u ∈ countableSupClosure (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})

theorem MeasureTheory.Ioi_mem_countableSupClosure_Icc {ι : Type u_6} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (u : ι) : Set.Ioi u ∈ countableSupClosure (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})

theorem MeasureTheory.univ_mem_countableSupClosure_Icc {ι : Type u_6} [hι : Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] : Set.univ ∈ countableSupClosure {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}

theorem MeasureTheory.compl_Icc_mem_countableSupClosure_Icc {ι : Type u_6} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (l u : ι) : (Set.Icc l u)ᶜ ∈ countableSupClosure (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})

theorem MeasureTheory.compl_mem_countableSupClosure_image2_prod_Icc {𝓧 : Type u_1} {ι : Type u_6} [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace 𝓧] (s : Set (𝓧 × ι)) (hs : s ∈ Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) {t : Set 𝓧 | MeasurableSet t} (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})) : sᶜ ∈ countableSupClosure (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) {t : Set 𝓧 | MeasurableSet t} (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}))

theorem MeasurableSet.isPavingAnalytic_Icc {ι : Type u_6} {mι : MeasurableSpace ι} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [BorelSpace ι] {s : Set ι} (hs : MeasurableSet s) : MeasureTheory.IsPavingAnalytic (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}) s

A measurable set of a second countable linear order is analytic for the paving of closed intervals. Variant of Theorem 1.32 (1) of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalytic_measurableSet_iff_isPavingAnalytic_Icc {ι : Type u_6} {mι : MeasurableSpace ι} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [BorelSpace ι] (s : Set ι) : IsPavingAnalytic {t : Set ι | MeasurableSet t} s ↔ IsPavingAnalytic (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t}) s

In a second countable linear order, a set is analytic for the paving of measurable sets if and only if it is analytic for the paving of closed intervals.

theorem MeasureTheory.isCountablySpanning_insert_empty_Icc {ι : Type u_6} [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] : IsCountablySpanning (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})

theorem MeasurableSet.isPavingAnalytic_image2_prod {𝓧 : Type u_1} {ι : Type u_6} {mι : MeasurableSpace ι} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [BorelSpace ι] {s : Set (𝓧 × ι)} {m𝓧 : MeasurableSpace 𝓧} (hs : MeasurableSet s) : MeasureTheory.IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) {t : Set 𝓧 | MeasurableSet t} (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})) s

A measurable set of 𝓧 × ι is analytic for the product of the paving of measurable sets and the paving of closed intervals. Variant of Theorem 1.32 (2) of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalytic_image2_prod_measurableSet_Icc_iff {𝓧 : Type u_1} {ι : Type u_6} {mι : MeasurableSpace ι} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [BorelSpace ι] {s : Set (𝓧 × ι)} [MeasurableSpace 𝓧] : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) {t : Set 𝓧 | MeasurableSet t} (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})) s ↔ IsPavingAnalytic {t : Set (𝓧 × ι) | MeasurableSet t} s

A set of 𝓧 × ι is analytic for the paving of measurable sets if and only if it is analytic for the product of the paving of measurable sets and the paving of closed intervals. Variant of Theorem 1.32 (2) of [he2019semimartingale].

theorem MeasureTheory.isPavingAnalytic_fst_of_image2_prod_measurableSet_Icc {𝓧 : Type u_1} {ι : Type u_6} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι] [MeasurableSpace 𝓧] {s : Set (𝓧 × ι)} (hs : IsPavingAnalytic (Set.image2 (fun (x1 : Set 𝓧) (x2 : Set ι) => x1 ×ˢ x2) {t : Set 𝓧 | MeasurableSet t} (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})) s) : IsPavingAnalytic {t : Set 𝓧 | MeasurableSet t} (Prod.fst '' s)

The projection of an analytic set for the product of the paving of measurable sets and the paving of closed intervals is analytic for the paving of measurable sets. Variant of Theorem 1.32 (3) of [he2019semimartingale].

theorem MeasurableSet.isPavingAnalytic_fst {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {s : Set (𝓧 × ℝ)} (hs : MeasurableSet s) : MeasureTheory.IsPavingAnalytic {t : Set 𝓧 | MeasurableSet t} (Prod.fst '' s)

The projection of a measurable set of 𝓧 × ℝ is analytic for the paving of measurable sets.

def MeasureTheory.IsMeasurableAnalyticFor {𝓧 : Type u_1} (𝓚 : Type u_6) [MeasurableSpace 𝓚] [MeasurableSpace 𝓧] (s : Set 𝓧) : Prop

A set s of a measurable space 𝓧 is measurably analytic for a measurable space 𝓚 if it is the projection of a measurable set of 𝓧 × 𝓚.

Equations

• MeasureTheory.IsMeasurableAnalyticFor 𝓚 s = ∃ (t : Set (𝓧 × 𝓚)), MeasurableSet t ∧ s = Prod.fst '' t

theorem MeasureTheory.isMeasurableAnalyticFor_of_snd {𝓧 : Type u_1} {𝓚 : Type u_3} {x✝ : MeasurableSpace 𝓚} [MeasurableSpace 𝓧] {s : Set 𝓧} (t : Set (𝓚 × 𝓧)) (ht : MeasurableSet t) (hst : s = Prod.snd '' t) : IsMeasurableAnalyticFor 𝓚 s

def MeasureTheory.IsMeasurableAnalytic {𝓧 : Type u_1} [MeasurableSpace 𝓧] (s : Set 𝓧) : Prop

A set s of a measurable space 𝓧 is measurably analytic if it is the projection of a measurable set of 𝓧 × ℝ.

Equations

• MeasureTheory.IsMeasurableAnalytic s = MeasureTheory.IsMeasurableAnalyticFor ℝ s

theorem MeasureTheory.isMeasurableAnalytic_of_snd {𝓧 : Type u_1} [MeasurableSpace 𝓧] {s : Set 𝓧} (t : Set (ℝ × 𝓧)) (ht : MeasurableSet t) (hst : s = Prod.snd '' t) : IsMeasurableAnalytic s

theorem MeasureTheory.IsMeasurableAnalyticFor.isMeasurableAnalytic {𝓧 : Type u_1} {𝓚 : Type u_3} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} {m𝓚 : MeasurableSpace 𝓚} [StandardBorelSpace 𝓚] (hs : IsMeasurableAnalyticFor 𝓚 s) : IsMeasurableAnalytic s

If a set is measurably analytic for some standard Borel space 𝓚, then it is measurably analytic for ℝ.

theorem MeasurableSet.isMeasurableAnalytic {𝓧 : Type u_1} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} (hs : MeasurableSet s) : MeasureTheory.IsMeasurableAnalytic s

theorem MeasureTheory.IsMeasurableAnalytic.isPavingAnalytic {𝓧 : Type u_1} {s : Set 𝓧} {m𝓧 : MeasurableSpace 𝓧} (hs : IsMeasurableAnalytic s) : IsPavingAnalytic {t : Set 𝓧 | MeasurableSet t} s