Algebras of sets generated by sign conditions

Given a class of functions α → R, consider the algebra of sets generated by their zero sets {x | f x = 0} and positivity sets {x | 0 < f x}. Every member of it is described by a condition on the signs of finitely many functions of the class.

Main results

• TauCeti.exists_eq_setOf_sign_of_mem_generateSetAlgebra: the sign-condition normal form.
• MeasureTheory.IsSetAlgebra.preimage: the sets whose preimages under a fixed map lie in an algebra of sets form an algebra of sets.
• MeasureTheory.isSetAlgebra_measurableSet, MeasureTheory.isSetRing_measurableSet: the measurable sets form an algebra, hence a ring, of sets.
• MeasureTheory.isSetRing_nullMeasurableSet: the null-measurable sets of a measure form a ring of sets.

theorem TauCeti.exists_eq_setOf_sign_of_mem_generateSetAlgebra {α : Type u_1} {R : Type u_2} [Zero R] [LinearOrder R] {P : (α → R) → Prop} {t : Set α} (ht : t ∈ MeasureTheory.generateSetAlgebra ({t : Set α | ∃ (f : α → R), P f ∧ t = {x : α | f x = 0}} ∪ {t : Set α | ∃ (f : α → R), P f ∧ t = {x : α | 0 < f x}})) : ∃ (m : ℕ) (f : Fin m → α → R), (∀ (i : Fin m), P (f i)) ∧ ∃ (Φ : (Fin m → SignType) → Prop), t = {x : α | Φ fun (i : Fin m) => SignType.sign (f i x)}

Sign-condition normal form. Every member of the algebra of sets generated by the zero sets and the positivity sets of the functions f : α → R satisfying P is described by a condition on the signs of finitely many functions satisfying P.

theorem MeasureTheory.IsSetAlgebra.preimage {α : Type u_1} {β : Type u_2} {𝒜 : Set (Set β)} (h𝒜 : IsSetAlgebra 𝒜) (g : β → α) : IsSetAlgebra {t : Set α | g ⁻¹' t ∈ 𝒜}

The sets whose preimages under a map g lie in an algebra of sets form an algebra of sets. Combined with IsSetAlgebra.generateSetAlgebra_subset, this shows that a preimage of a member of a generated algebra lies in a given algebra once the preimages of the generators do.

theorem MeasureTheory.isSetAlgebra_measurableSet {α : Type u_1} [MeasurableSpace α] : IsSetAlgebra {s : Set α | MeasurableSet s}

The measurable sets form an algebra of sets.

theorem MeasureTheory.isSetRing_measurableSet {α : Type u_1} [MeasurableSpace α] : IsSetRing {s : Set α | MeasurableSet s}

The measurable sets form a ring of sets.

theorem MeasureTheory.isSetRing_nullMeasurableSet {α : Type u_1} [MeasurableSpace α] {μ : Measure α} : IsSetRing {s : Set α | NullMeasurableSet s μ}

The null-measurable sets of a measure form a ring of sets.

theorem MeasureTheory.sUnion_finset_mem_supClosure {β : Type u_2} {C : Set (Set β)} (hC : ∅ ∈ C) {I : Finset (Set β)} (hI : ∀ r ∈ I, r ∈ C) : ⋃₀ ↑I ∈ supClosure C

A finite union of sets from a family containing ∅ lies in the family supClosure C of finite unions of its members.