HepLean 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

source
def MeasureTheory.OuterMeasure.IsCaratheodory {α : Type u} (m : MeasureTheory.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)
Instances For
    source
    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
    source
    @[simp]
    theorem MeasureTheory.OuterMeasure.isCaratheodory_empty {α : Type u} (m : MeasureTheory.OuterMeasure α) :
    m.IsCaratheodory ∅
    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_compl {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} :
    m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ
    source
    @[simp]
    theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} :
    m.IsCaratheodory sᶜ ↔ m.IsCaratheodory s
    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_union {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) :
    m.IsCaratheodory (s₁ ∪ s₂)
    source
    theorem MeasureTheory.OuterMeasure.measure_inter_union {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α} (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : m.IsCaratheodory s₁) {t : Set α} :
    m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)
    source
    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)
    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_inter {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) :
    m.IsCaratheodory (s₁ ∩ s₂)
    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_diff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α} (h₁ : m.IsCaratheodory s₁) (h₂ : m.IsCaratheodory s₂) :
    m.IsCaratheodory (s₁ \ s₂)
    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_partialSups {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (i : ℕ) :
    m.IsCaratheodory ((partialSups s) i)
    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_disjointed {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (i : ℕ) :
    m.IsCaratheodory (disjointed s i)
    source
    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 : ℕ} :
    ∑ i ∈ Finset.range n, m (t ∩ s i) = m (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i)
    source
    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.

    source
    @[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.

    source
    theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) :
    m.IsCaratheodory (⋃ (i : ℕ), s i)
    source
    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)
    source
    def MeasureTheory.OuterMeasure.caratheodoryDynkin {α : Type u} (m : MeasureTheory.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 := ⋯ }
    Instances For
      source
      def MeasureTheory.OuterMeasure.caratheodory {α : Type u} (m : MeasureTheory.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 ⋯
      Instances For
        source
        theorem MeasureTheory.OuterMeasure.isCaratheodory_iff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} :
        MeasurableSet s ↔ ∀ (t : Set α), m t = m (t ∩ s) + m (t \ s)
        source
        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
        source
        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)
        source
        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
        source
        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
        source
        @[simp]
        theorem MeasureTheory.OuterMeasure.zero_caratheodory {α : Type u_1} :
        MeasureTheory.OuterMeasure.caratheodory 0 = ⊤
        source
        theorem MeasureTheory.OuterMeasure.top_caratheodory {α : Type u_1} :
        ⊤.caratheodory = ⊤
        source
        theorem MeasureTheory.OuterMeasure.le_add_caratheodory {α : Type u_1} (m₁ m₂ : MeasureTheory.OuterMeasure α) :
        m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂).caratheodory
        source
        theorem MeasureTheory.OuterMeasure.le_sum_caratheodory {α : Type u_1} {ι : Type u_2} (m : ι → MeasureTheory.OuterMeasure α) :
        ⨅ (i : ι), (m i).caratheodory ≤ (MeasureTheory.OuterMeasure.sum m).caratheodory
        source
        theorem MeasureTheory.OuterMeasure.le_smul_caratheodory {α : Type u_1} (a : ENNReal) (m : MeasureTheory.OuterMeasure α) :
        m.caratheodory ≤ (a • m).caratheodory
        source
        @[simp]
        theorem MeasureTheory.OuterMeasure.dirac_caratheodory {α : Type u_1} (a : α) :
        (MeasureTheory.OuterMeasure.dirac a).caratheodory = ⊤