2.2. Measurable Sets🔗

Definition.

We define inductively the notion of a subset A \subseteq \mathbb{R} being (Borel) measurable as follows:

For every a \in \mathbb{R}, the half-line [a,\infty) is measurable.
The empty set \emptyset is measurable.
If A is measurable, then its complement A^c is measurable.
If A_0, A_1, \dots are measurable, then \bigcup_{n \in \mathbb{N}} A_n is measurable.

Lean code

inductive MeasurableSet : Set ℝ → Prop
  | ici' : ∀ a : ℝ, MeasurableSet (Ici a)
  | empty' : MeasurableSet ∅
  | compl' : ∀ A, MeasurableSet A → MeasurableSet Aᶜ
  | iUnion' : ∀ A : ℕ → Set ℝ, (∀ n, MeasurableSet (A n)) → MeasurableSet (⋃ i, A i)

Lemma.

The empty set and the whole space \mathbb{R} are measurable.

Lean code

@[simp]
theorem MeasurableSet.empty : MeasurableSet (∅ : Set ℝ) :=
  MeasurableSet.empty'

theorem MeasurableSet.univ : MeasurableSet (Set.univ : Set ℝ) := by⊢ MeasurableSet Set.univ
  simpa using (MeasurableSet.empty : MeasurableSet (∅ : Set ℝ)).complAll goals completed! 🐙

Lemma.

Countable unions and intersections of measurable sets are measurable.

Lean code

theorem MeasurableSet.iUnion (A : ℕ → Set ℝ) (hA : ∀ n, MeasurableSet (A n)) :
    MeasurableSet (⋃ i, A i) :=
  MeasurableSet.iUnion' A hA

theorem MeasurableSet.iInter {A : ℕ → Set ℝ} (hA : ∀ n, MeasurableSet (A n)) :
    MeasurableSet (⋂ n, A n) := byA:ℕ → Set ℝhA:∀ (n : ℕ), MeasurableSet (A n)⊢ MeasurableSet (⋂ n, A n)
  have hEq : (⋂ n, A n) = (⋃ n, (A n)ᶜ)ᶜ := byA:ℕ → Set ℝhA:∀ (n : ℕ), MeasurableSet (A n)⊢ MeasurableSet (⋂ n, A n)
    ext xhA:ℕ → Set ℝhA:∀ (n : ℕ), MeasurableSet (A n)x:ℝ⊢ x ∈ ⋂ n, A n ↔ x ∈ (⋃ n, (A n)ᶜ)ᶜ
    simpAll goals completed! 🐙
  rw [hEq]A:ℕ → Set ℝhA:∀ (n : ℕ), MeasurableSet (A n)hEq:⋂ n, A n = (⋃ n, (A n)ᶜ)ᶜ := 
  ext fun x =>
    of_eq_true
      (Eq.trans
        (congr (congrArg Iff mem_iInter._simp_1)
          (Eq.trans
            (congrFun'
              (congrArg Membership.mem
                (Eq.trans (compl_iUnion fun i => (A i)ᶜ) (congrArg Set.iInter (funext fun i => compl_compl (A i)))))
              x)
            mem_iInter._simp_1))
        (iff_self (∀ (i : ℕ), x ∈ A i)))⊢ MeasurableSet (⋃ n, (A n)ᶜ)ᶜ
  exact (MeasurableSet.iUnion _ fun n ↦ (hA n).compl).complAll goals completed! 🐙

Lemma.

Unions, complements, and intersections of measurable sets are measurable.

Lean code

theorem MeasurableSet.union {A₁ A₂ : Set ℝ} (h₁ : MeasurableSet A₁) (h₂ : MeasurableSet A₂) :
    MeasurableSet (A₁ ∪ A₂) := byA₁:Set ℝA₂:Set ℝh₁:MeasurableSet A₁h₂:MeasurableSet A₂⊢ MeasurableSet (A₁ ∪ A₂)
  rw [union_eq_iUnion]A₁:Set ℝA₂:Set ℝh₁:MeasurableSet A₁h₂:MeasurableSet A₂⊢ MeasurableSet (⋃ b, bif b then A₁ else A₂)
  exact MeasurableSet.iUnion_countable (Bool.forall_bool.2 ⟨h₂, h₁⟩)All goals completed! 🐙

theorem MeasurableSet.compl {A : Set ℝ} (hA : MeasurableSet A) :
    MeasurableSet Aᶜ :=
  MeasurableSet.compl' A hA

theorem MeasurableSet.inter {A₁ A₂ : Set ℝ} (h₁ : MeasurableSet A₁) (h₂ : MeasurableSet A₂) :
    MeasurableSet (A₁ ∩ A₂) := byA₁:Set ℝA₂:Set ℝh₁:MeasurableSet A₁h₂:MeasurableSet A₂⊢ MeasurableSet (A₁ ∩ A₂)
  rw [(by grind : A₁ ∩ A₂ = (A₁ᶜ ∪ A₂ᶜ)ᶜ)]A₁:Set ℝA₂:Set ℝh₁:MeasurableSet A₁h₂:MeasurableSet A₂⊢ MeasurableSet (A₁ᶜ ∪ A₂ᶜ)ᶜ
  apply (h₁.compl.union h₂.compl).complAll goals completed! 🐙

Lemma.

The intervals [a,\infty), (-\infty,a), (a,\infty), (-\infty,a], (a,b], [a,b), [a,b], (a,b) and the singleton \{a\} are measurable.

Lean code

theorem measurableSet_Ici (a : ℝ) : MeasurableSet (Set.Ici a) := bya:ℝ⊢ MeasurableSet (Ici a)
  apply MeasurableSet.iciAll goals completed! 🐙

theorem measurableSet_Iio (a : ℝ) : MeasurableSet (Set.Iio a) := bya:ℝ⊢ MeasurableSet (Iio a)
  rw [← Set.compl_Ici]a:ℝ⊢ MeasurableSet (Ici a)ᶜ
  apply MeasurableSet.complhAa:ℝ⊢ MeasurableSet (Ici a)
  apply MeasurableSet.iciAll goals completed! 🐙

theorem measurableSet_Ioi (a : ℝ) : MeasurableSet (Set.Ioi a) := bya:ℝ⊢ MeasurableSet (Ioi a)
  rcases TopologicalSpace.isOpen_biUnion_countable (Set.Ioi a) Set.Ioi fun _ _ ↦ isOpen_Ioi
    with ⟨A, haA, hAc, hAU⟩a:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi i⊢ MeasurableSet (Ioi a)
  have : Set.Ioi a = ⋃ b ∈ A, Set.Ici b := bya:ℝ⊢ MeasurableSet (Ioi a)
    refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ bya:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi ib:ℝhb:b ∈ A⊢ Ici b ⊆ Ioi a grindAll goals completed! 🐙
    refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Set.Ioi_subset_Ici_selfa:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi i⊢ Ioi a ⊆ ⋃ i ∈ A, Ioi i
    simp only [hAU, mem_Ioi, subset_def, mem_iUnion, exists_prop]a:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi i⊢ ∀ (x : ℝ), a < x → ∃ i, a < i ∧ i < x
    intro b haba:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi ib:ℝhab:a < b⊢ ∃ i, a < i ∧ i < b
    exact exists_between habAll goals completed! 🐙
  simp only [this]a:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi ithis:Ioi a = ⋃ b ∈ A, Ici b := 
  Subset.antisymm
    (Subset.trans
      (Eq.mpr
        (id
          (Eq.trans
            (congrArg (Subset (Ioi a))
              (Eq.trans hAU
                (congrArg iUnion
                  (funext fun i => iUnion_congr_Prop (Iff.of_eq measurableSet_Ioi._simp_1) fun x => Eq.refl (Ioi i)))))
            (forall_congr fun x =>
              implies_congr measurableSet_Ioi._simp_1
                (Eq.trans measurableSet_Ioi._simp_2
                  (congrArg Exists
                    (funext fun i =>
                      Eq.trans measurableSet_Ioi._simp_2
                        (Eq.trans
                          (propext
                            (exists_prop_congr (fun h => Iff.of_eq measurableSet_Ioi._simp_1)
                              (Iff.of_eq (Eq.refl (a < i)))))
                          measurableSet_Ioi._simp_3)))))))
        fun b hab => exists_between hab)
      (iUnion₂_mono fun x x_1 => Ioi_subset_Ici_self))
    (iUnion₂_subset fun b hb => measurableSet_Ioi._proof_1 a A haA b hb)⊢ MeasurableSet (⋃ b ∈ A, Ici b)
  apply MeasurableSet.biUnion hAca:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi ithis:Ioi a = ⋃ b ∈ A, Ici b := 
  Subset.antisymm
    (Subset.trans
      (Eq.mpr
        (id
          (Eq.trans
            (congrArg (Subset (Ioi a))
              (Eq.trans hAU
                (congrArg iUnion
                  (funext fun i => iUnion_congr_Prop (Iff.of_eq measurableSet_Ioi._simp_1) fun x => Eq.refl (Ioi i)))))
            (forall_congr fun x =>
              implies_congr measurableSet_Ioi._simp_1
                (Eq.trans measurableSet_Ioi._simp_2
                  (congrArg Exists
                    (funext fun i =>
                      Eq.trans measurableSet_Ioi._simp_2
                        (Eq.trans
                          (propext
                            (exists_prop_congr (fun h => Iff.of_eq measurableSet_Ioi._simp_1)
                              (Iff.of_eq (Eq.refl (a < i)))))
                          measurableSet_Ioi._simp_3)))))))
        fun b hab => exists_between hab)
      (iUnion₂_mono fun x x_1 => Ioi_subset_Ici_self))
    (iUnion₂_subset fun b hb => measurableSet_Ioi._proof_1 a A haA b hb)⊢ ∀ b ∈ A, MeasurableSet (Ici b)
  intro a haa✝:ℝA:Set ℝhaA:A ⊆ Ioi ahAc:A.CountablehAU:⋃ i ∈ A, Ioi i = ⋃ i ∈ Ioi a, Ioi ithis:Ioi a = ⋃ b ∈ A, Ici b := 
  Subset.antisymm
    (Subset.trans
      (Eq.mpr
        (id
          (Eq.trans
            (congrArg (Subset (Ioi a))
              (Eq.trans hAU
                (congrArg iUnion
                  (funext fun i => iUnion_congr_Prop (Iff.of_eq measurableSet_Ioi._simp_1) fun x => Eq.refl (Ioi i)))))
            (forall_congr fun x =>
              implies_congr measurableSet_Ioi._simp_1
                (Eq.trans measurableSet_Ioi._simp_2
                  (congrArg Exists
                    (funext fun i =>
                      Eq.trans measurableSet_Ioi._simp_2
                        (Eq.trans
                          (propext
                            (exists_prop_congr (fun h => Iff.of_eq measurableSet_Ioi._simp_1)
                              (Iff.of_eq (Eq.refl (a < i)))))
                          measurableSet_Ioi._simp_3)))))))
        fun b hab => exists_between hab)
      (iUnion₂_mono fun x x_1 => Ioi_subset_Ici_self))
    (iUnion₂_subset fun b hb => measurableSet_Ioi._proof_1 a A haA b hb)a:ℝha:a ∈ A⊢ MeasurableSet (Ici a)
  exact measurableSet_Ici aAll goals completed! 🐙

theorem measurableSet_Iic (a : ℝ) : MeasurableSet (Set.Iic a) := bya:ℝ⊢ MeasurableSet (Iic a)
  rw [← Set.compl_Ioi]a:ℝ⊢ MeasurableSet (Ioi a)ᶜ
  apply MeasurableSet.complhAa:ℝ⊢ MeasurableSet (Ioi a)
  exact measurableSet_Ioi aAll goals completed! 🐙

theorem measurableSet_Ioc (a b : ℝ) : MeasurableSet (Set.Ioc a b) := bya:ℝb:ℝ⊢ MeasurableSet (Ioc a b)
  have : Set.Ioc a b = Set.Ioi a ∩ Set.Iic b := bya:ℝb:ℝ⊢ MeasurableSet (Ioc a b) grindAll goals completed! 🐙
  rw [this]a:ℝb:ℝthis:Ioc a b = Ioi a ∩ Iic b := measurableSet_Ioc._proof_1 a b⊢ MeasurableSet (Ioi a ∩ Iic b)
  apply (measurableSet_Ioi a).inter (measurableSet_Iic b)All goals completed! 🐙

theorem measurableSet_Ico (a b : ℝ) : MeasurableSet (Set.Ico a b) := bya:ℝb:ℝ⊢ MeasurableSet (Ico a b)
  have : Set.Ico a b = Set.Ici a ∩ Set.Iio b := bya:ℝb:ℝ⊢ MeasurableSet (Ico a b) grindAll goals completed! 🐙
  rw [this]a:ℝb:ℝthis:Ico a b = Ici a ∩ Iio b := measurableSet_Ico._proof_1 a b⊢ MeasurableSet (Ici a ∩ Iio b)
  apply (measurableSet_Ici a).inter (measurableSet_Iio b)All goals completed! 🐙

theorem measurableSet_Icc (a b : ℝ) : MeasurableSet (Set.Icc a b) := bya:ℝb:ℝ⊢ MeasurableSet (Icc a b)
  have : Set.Icc a b = Set.Iic b ∩ Set.Ici a := bya:ℝb:ℝ⊢ MeasurableSet (Icc a b) grindAll goals completed! 🐙
  rw [this]a:ℝb:ℝthis:Icc a b = Iic b ∩ Ici a := measurableSet_Icc._proof_1 a b⊢ MeasurableSet (Iic b ∩ Ici a)
  apply (measurableSet_Iic b).inter (measurableSet_Ici a)All goals completed! 🐙

theorem measurableSet_Ioo (a b : ℝ) : MeasurableSet (Set.Ioo a b) := bya:ℝb:ℝ⊢ MeasurableSet (Ioo a b)
  have : Set.Ioo a b = Set.Ioi a ∩ Set.Iio b := bya:ℝb:ℝ⊢ MeasurableSet (Ioo a b) grindAll goals completed! 🐙
  rw [this]a:ℝb:ℝthis:Ioo a b = Ioi a ∩ Iio b := measurableSet_Ioo._proof_1 a b⊢ MeasurableSet (Ioi a ∩ Iio b)
  apply (measurableSet_Ioi a).inter (measurableSet_Iio b)All goals completed! 🐙

theorem measurableSet_singleton (a : ℝ) : MeasurableSet ({a} : Set ℝ) := bya:ℝ⊢ MeasurableSet {a}
  have : ({a} : Set ℝ) = Set.Iic a ∩ Set.Ici a := bya:ℝ⊢ MeasurableSet {a} grindAll goals completed! 🐙
  rw [this]a:ℝthis:{a} = Iic a ∩ Ici a := measurableSet_singleton._proof_1 a⊢ MeasurableSet (Iic a ∩ Ici a)
  apply (measurableSet_Iic a).inter (measurableSet_Ici a)All goals completed! 🐙