The Caratheodory σ-algebra of an outer measure

Given an outer measure m, the Carathéodory-measurable sets are the sets s such that for all sets t we have m t = m (t ∩ s) + m (t \ s). This forms a measurable space.

Main definitions and statements

• MeasureTheory.OuterMeasure.caratheodory is the Carathéodory-measurable space of an outer measure.

References

• https://en.wikipedia.org/wiki/Outer_measure
• https://en.wikipedia.org/wiki/Carath%C3%A9odory%27s_criterion

Tags

Carathéodory-measurable, Carathéodory's criterion

def MeasureTheory.OuterMeasure.IsCaratheodory {α : Type u} (m : OuterMeasure α) (s : Set α) : Prop

A set s is Carathéodory-measurable for an outer measure m if for all sets t we have m t = m (t ∩ s) + m (t \ s).

Equations

• m.IsCaratheodory s = ∀ (t : Set α), m t = m (t ∩ s) + m (t \ s)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le' {α : Type u} (m : OuterMeasure α) {s : Set α} : m.IsCaratheodory s ↔ ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t

@[simp]

theorem MeasureTheory.OuterMeasure.isCaratheodory_empty {α : Type u} (m : OuterMeasure α) : m.IsCaratheodory ∅

theorem MeasureTheory.OuterMeasure.isCaratheodory_compl {α : Type u} (m : OuterMeasure α) {s₁ : Set α} : m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ

@[simp]

theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff {α : Type u} (m : OuterMeasure α) {s : Set α} : m.IsCaratheodory sᶜ ↔ m.IsCaratheodory s

theorem MeasureTheory.OuterMeasure.isCaratheodory_union {α : Type u} (m : OuterMeasure α) {s₁ s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) : m.IsCaratheodory (s₁ ∪ s₂)

theorem MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finite {α : Type u} {m : OuterMeasure α} {ι : Type u_1} {s : ι → Set α} {t : Set ι} (ht : t.Finite) (h : ∀ i ∈ t, m.IsCaratheodory (s i)) : m.IsCaratheodory (⋃ i ∈ t, s i)

theorem MeasureTheory.OuterMeasure.measure_inter_union {α : Type u} (m : OuterMeasure α) {s₁ s₂ : Set α} (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : m.IsCaratheodory s₁) {t : Set α} : m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt {α : Type u} (m : OuterMeasure α) {s : ℕ → Set α} {n : ℕ} : (∀ i < n, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ (i : ℕ), ⋃ (_ : i < n), s i)

theorem MeasureTheory.OuterMeasure.isCaratheodory_inter {α : Type u} (m : OuterMeasure α) {s₁ s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) : m.IsCaratheodory (s₁ ∩ s₂)

theorem MeasureTheory.OuterMeasure.isCaratheodory_diff {α : Type u} (m : OuterMeasure α) {s₁ s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) : m.IsCaratheodory (s₁ \ s₂)

theorem MeasureTheory.OuterMeasure.isCaratheodory_partialSups {α : Type u} (m : OuterMeasure α) {ι : Type u_1} [PartialOrder ι] [LocallyFiniteOrderBot ι] {s : ι → Set α} (h : ∀ (i : ι), m.IsCaratheodory (s i)) (i : ι) : m.IsCaratheodory ((partialSups s) i)

theorem MeasureTheory.OuterMeasure.isCaratheodory_disjointed {α : Type u} (m : OuterMeasure α) {ι : Type u_1} [PartialOrder ι] [LocallyFiniteOrderBot ι] {s : ι → Set α} (h : ∀ (i : ι), m.IsCaratheodory (s i)) (i : ι) : m.IsCaratheodory (disjointed s i)

theorem MeasureTheory.OuterMeasure.isCaratheodory_sum {α : Type u} (m : OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (hd : Pairwise (Function.onFun Disjoint s)) {t : Set α} {n : ℕ} : ∑ i ∈ Finset.range n, m (t ∩ s i) = m (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint {α : Type u} (m : OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (hd : Pairwise (Function.onFun Disjoint s)) : m.IsCaratheodory (⋃ (i : ℕ), s i)

Use isCaratheodory_iUnion instead, which does not require the disjoint assumption.

theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion {α : Type u} (m : OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) : m.IsCaratheodory (⋃ (i : ℕ), s i)

theorem MeasureTheory.OuterMeasure.f_iUnion {α : Type u} (m : OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (hd : Pairwise (Function.onFun Disjoint s)) : m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), m (s i)

def MeasureTheory.OuterMeasure.caratheodoryDynkin {α : Type u} (m : OuterMeasure α) : MeasurableSpace.DynkinSystem α

The Carathéodory-measurable sets for an outer measure m form a Dynkin system.

Equations

• m.caratheodoryDynkin = { Has := m.IsCaratheodory, has_empty := ⋯, has_compl := ⋯, has_iUnion_nat := ⋯ }

def MeasureTheory.OuterMeasure.caratheodory {α : Type u} (m : OuterMeasure α) : MeasurableSpace α

Given an outer measure μ, the Carathéodory-measurable space is defined such that s is measurable if ∀t, μ t = μ (t ∩ s) + μ (t \ s).

Equations

• m.caratheodory = m.caratheodoryDynkin.toMeasurableSpace ⋯

theorem MeasureTheory.OuterMeasure.isCaratheodory_iff {α : Type u} (m : OuterMeasure α) {s : Set α} : MeasurableSet s ↔ ∀ (t : Set α), m t = m (t ∩ s) + m (t \ s)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le {α : Type u} (m : OuterMeasure α) {s : Set α} : MeasurableSet s ↔ ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t

theorem MeasureTheory.OuterMeasure.iUnion_eq_of_caratheodory {α : Type u} (m : OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint s)) : m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), m (s i)

theorem MeasureTheory.OuterMeasure.ofFunction_caratheodory {α : Type u_1} {m : Set α → ENNReal} {s : Set α} {h₀ : m ∅ = 0} (hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t) : MeasurableSet s

theorem MeasureTheory.OuterMeasure.boundedBy_caratheodory {α : Type u_1} {m : Set α → ENNReal} {s : Set α} (hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t) : MeasurableSet s

@[simp]

theorem MeasureTheory.OuterMeasure.zero_caratheodory {α : Type u_1} : OuterMeasure.caratheodory 0 = ⊤

theorem MeasureTheory.OuterMeasure.top_caratheodory {α : Type u_1} : ⊤.caratheodory = ⊤

theorem MeasureTheory.OuterMeasure.le_add_caratheodory {α : Type u_1} (m₁ m₂ : OuterMeasure α) : m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂).caratheodory

theorem MeasureTheory.OuterMeasure.le_sum_caratheodory {α : Type u_1} {ι : Type u_2} (m : ι → OuterMeasure α) : ⨅ (i : ι), (m i).caratheodory ≤ (sum m).caratheodory

theorem MeasureTheory.OuterMeasure.le_smul_caratheodory {α : Type u_1} (a : ENNReal) (m : OuterMeasure α) : m.caratheodory ≤ (a • m).caratheodory

@[simp]

theorem MeasureTheory.OuterMeasure.dirac_caratheodory {α : Type u_1} (a : α) : (dirac a).caratheodory = ⊤