Documentation

Mathlib.MeasureTheory.OuterMeasure.Caratheodory

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 #

References #

Tags #

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

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)
Instances For
    theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le' {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} :
    m.IsCaratheodory s ∀ (t : Set α), m (t s) + m (t \ s) m t
    theorem MeasureTheory.OuterMeasure.isCaratheodory_compl {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} :
    m.IsCaratheodory s₁m.IsCaratheodory s₁
    @[simp]
    theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} :
    m.IsCaratheodory s m.IsCaratheodory s
    theorem MeasureTheory.OuterMeasure.isCaratheodory_union {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) :
    m.IsCaratheodory (s₁ s₂)
    theorem MeasureTheory.OuterMeasure.measure_inter_union {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {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 : MeasureTheory.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 : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) :
    m.IsCaratheodory (s₁ s₂)
    theorem MeasureTheory.OuterMeasure.isCaratheodory_diff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) :
    m.IsCaratheodory (s₁ \ s₂)
    theorem MeasureTheory.OuterMeasure.isCaratheodory_partialSups {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} (h : ∀ (i : ), m.IsCaratheodory (s i)) (i : ) :
    m.IsCaratheodory ((partialSups s) i)
    theorem MeasureTheory.OuterMeasure.isCaratheodory_disjointed {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} (h : ∀ (i : ), m.IsCaratheodory (s i)) (i : ) :
    m.IsCaratheodory (disjointed s i)
    theorem MeasureTheory.OuterMeasure.isCaratheodory_sum {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} (h : ∀ (i : ), m.IsCaratheodory (s i)) (hd : Pairwise (Disjoint on s)) {t : Set α} {n : } :
    iFinset.range n, m (t s i) = m (t ⋃ (i : ), ⋃ (_ : i < n), s i)
    theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} (h : ∀ (i : ), m.IsCaratheodory (s i)) (hd : Pairwise (Disjoint on s)) :
    m.IsCaratheodory (⋃ (i : ), s i)

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

    @[deprecated MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint]
    theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_nat {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} (h : ∀ (i : ), m.IsCaratheodory (s i)) (hd : Pairwise (Disjoint on s)) :
    m.IsCaratheodory (⋃ (i : ), s i)

    Alias of MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint.


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

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

    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 := }
    Instances For

      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
      Instances For
        theorem MeasureTheory.OuterMeasure.isCaratheodory_iff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} :
        MeasurableSet s ∀ (t : Set α), m t = m (t s) + m (t \ s)
        theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le {α : Type u} (m : MeasureTheory.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 : MeasureTheory.OuterMeasure α) {s : Set α} (h : ∀ (i : ), MeasurableSet (s i)) (hd : Pairwise (Disjoint on 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) :
        theorem MeasureTheory.OuterMeasure.boundedBy_caratheodory {α : Type u_1} {m : Set αENNReal} {s : Set α} (hs : ∀ (t : Set α), m (t s) + m (t \ s) m t) :
        theorem MeasureTheory.OuterMeasure.le_add_caratheodory {α : Type u_1} (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) :
        m₁.caratheodory m₂.caratheodory (m₁ + m₂).caratheodory
        theorem MeasureTheory.OuterMeasure.le_sum_caratheodory {α : Type u_1} {ι : Type u_2} (m : ιMeasureTheory.OuterMeasure α) :
        ⨅ (i : ι), (m i).caratheodory (MeasureTheory.OuterMeasure.sum m).caratheodory
        theorem MeasureTheory.OuterMeasure.le_smul_caratheodory {α : Type u_1} (a : ENNReal) (m : MeasureTheory.OuterMeasure α) :
        m.caratheodory (a m).caratheodory