Borel sets

borel.lean

import measure_theory.borel_space

-- Various descriptions of Borel sets with different induction principles.

universe u

section borel

variables {X : Type u} [topological_space X]

def borel_mathlib : set X → Prop :=
λ s, (borel X).is_measurable s

/-- Direct inductive description of Borel sets in a fixed X.
Inductive principle: For each fixed topological space X,
Borel sets are built up from open ones by complement and union. -/
inductive borel_ind : set X → Prop
| opn (s) (h : is_open s) : borel_ind s
| compl (s) (h : borel_ind s) : borel_ind (-s)
| union (f : ℕ → set X) (h : ∀ i, borel_ind (f i)) : borel_ind (⋃ i, f i)

lemma mathlib_iff_ind {s : set X} : borel_mathlib s ↔ borel_ind s := sorry

inductive borel_rank : Type
| opn : borel_rank
| compl (r : borel_rank) : borel_rank
| union (r : ℕ → borel_rank) : borel_rank

inductive borel_ranked_ind : borel_rank → set X → Prop
| opn (s) (h : is_open s) : borel_ranked_ind borel_rank.opn s
| compl (s) (r : borel_rank) (h : borel_ranked_ind r s) : borel_ranked_ind (borel_rank.compl r) (-s)
| union (f : ℕ → set X) (r : ℕ → borel_rank)
    (h : ∀ i, borel_ranked_ind (r i) (f i)) : borel_ranked_ind (borel_rank.union r) (⋃ i, f i)

lemma ind_iff_ranked_ind {s : set X} : borel_ind s ↔ ∃ r, borel_ranked_ind r s := sorry

def borel_ranked_rec : borel_rank → set X → Prop
| borel_rank.opn := is_open
| (borel_rank.compl r) := λ s', ∃ s (h : borel_ranked_rec r s), s' = -s
| (borel_rank.union r) := λ s',
  ∃ (f : ℕ → set X) (h : ∀ i, borel_ranked_rec (r i) (f i)), s' = ⋃ i, f i

lemma ranked_ind_iff_ranked_rec {r : borel_rank} {s : set X} :
  borel_ranked_ind r s ↔ borel_ranked_rec r s := sorry

-- After David Wärn

inductive borel_family : set (set X) → Prop
| opn : borel_family is_open
| compl (F : set (set X)) (h : borel_family F) :
  borel_family {s' | ∃ s (h : s ∈ F), s' = -s}
| union (F : ℕ → set (set X)) (h : ∀ i, borel_family (F i)) :
  borel_family {s' | ∃ (f : ℕ → set X) (h : ∀ i, f i ∈ F i), s' = ⋃ i, f i}

lemma ranked_ind_iff_family {s : set X} :
  (∃ r, borel_ranked_ind r s) ↔ (∃ F : set (set X), borel_family F ∧ s ∈ F) := sorry

inductive borel_family_global : (Π (Y : Type u) [topological_space Y], set (set Y)) → Prop
| opn : borel_family_global @is_open
| compl (Φ) (h : borel_family_global Φ) :
  borel_family_global (λ Y τ s', ∃ s (h : @Φ Y τ s), s' = -s)
| union (Φ : ℕ → Π (Y : Type u) [topological_space Y], set (set Y))
        (h : ∀ i, borel_family_global (Φ i)) :
  borel_family_global (λ Y τ s', ∃ (f : ℕ → set Y) (h : ∀ i, @Φ i Y τ (f i)), s' = ⋃ i, f i)

lemma family_iff_family_global {Y : Type u} [topological_space Y] {s : set Y} :
  (∃ (F : set (set Y)), borel_family F ∧ s ∈ F) ↔
  (∃ Φ, borel_family_global Φ ∧ s ∈ Φ Y) := sorry

end borel