Documentation

Mathlib.MeasureTheory.Measure.NullMeasurable

Null measurable sets and complete measures #

Main definitions #

Null measurable sets and functions #

A set s : Set α is called null measurable (MeasureTheory.NullMeasurableSet) if it satisfies any of the following equivalent conditions:

Null measurable sets form a σ-algebra that is registered as a MeasurableSpace instance on MeasureTheory.NullMeasurableSpace α μ. We also say that f : α → β is MeasureTheory.NullMeasurable if the preimage of a measurable set is a null measurable set. In other words, f : α → β is null measurable if it is measurable as a function MeasureTheory.NullMeasurableSpace α μ → β.

Complete measures #

We say that a measure μ is complete w.r.t. the MeasurableSpace α σ-algebra (or the σ-algebra is complete w.r.t measure μ) if every set of measure zero is measurable. In this case all null measurable sets and functions are measurable.

For each measure μ, we define MeasureTheory.Measure.completion μ to be the same measure interpreted as a measure on MeasureTheory.NullMeasurableSpace α μ and prove that this is a complete measure.

Implementation notes #

We define MeasureTheory.NullMeasurableSet as @MeasurableSet (NullMeasurableSpace α μ) _ so that theorems about MeasurableSets like MeasurableSet.union can be applied to NullMeasurableSets. However, these lemmas output terms of the same form @MeasurableSet (NullMeasurableSpace α μ) _ _. While this is definitionally equal to the expected output NullMeasurableSet s μ, it looks different and may be misleading. So we copy all standard lemmas about measurable sets to the MeasureTheory.NullMeasurableSet namespace and fix the output type.

Tags #

measurable, measure, null measurable, completion

A type tag for α with MeasurableSet given by NullMeasurableSet.

Equations
Instances For
    Equations
    • MeasureTheory.NullMeasurableSpace.instInhabited = h
    Equations

    A set is called NullMeasurableSet if it can be approximated by a measurable set up to a set of null measure.

    Equations
    Instances For
      theorem MeasureTheory.NullMeasurableSet.iUnion {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} [Countable ι] {s : ιSet α} (h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) :
      MeasureTheory.NullMeasurableSet (⋃ (i : ι), s i) μ
      theorem MeasureTheory.NullMeasurableSet.biUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} {s : Set ι} (hs : s.Countable) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
      MeasureTheory.NullMeasurableSet (bs, f b) μ
      theorem MeasureTheory.NullMeasurableSet.sUnion {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} (hs : s.Countable) (h : ts, MeasureTheory.NullMeasurableSet t μ) :
      theorem MeasureTheory.NullMeasurableSet.iInter {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} [Countable ι] {f : ιSet α} (h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) :
      MeasureTheory.NullMeasurableSet (⋂ (i : ι), f i) μ
      theorem MeasureTheory.NullMeasurableSet.biInter {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : βSet α} {s : Set β} (hs : s.Countable) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
      MeasureTheory.NullMeasurableSet (bs, f b) μ
      theorem MeasureTheory.NullMeasurableSet.sInter {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} (hs : s.Countable) (h : ts, MeasureTheory.NullMeasurableSet t μ) :
      theorem MeasureTheory.exists_subordinate_pairwise_disjoint {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} (h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hd : Pairwise (MeasureTheory.AEDisjoint μ on s)) :
      ∃ (t : ιSet α), (∀ (i : ι), t i s i) (∀ (i : ι), s i =ᵐ[μ] t i) (∀ (i : ι), MeasurableSet (t i)) Pairwise (Disjoint on t)

      If sᵢ is a countable family of (null) measurable pairwise μ-a.e. disjoint sets, then there exists a subordinate family tᵢ ⊆ sᵢ of measurable pairwise disjoint sets such that tᵢ =ᵐ[μ] sᵢ.

      theorem MeasureTheory.measure_iUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {f : ιSet α} (hn : Pairwise (Disjoint on f)) (h : ∀ (i : ι), MeasurableSet (f i)) :
      μ (⋃ (i : ι), f i) = ∑' (i : ι), μ (f i)
      theorem MeasureTheory.measure_iUnion₀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {f : ιSet α} (hd : Pairwise (MeasureTheory.AEDisjoint μ on f)) (h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) :
      μ (⋃ (i : ι), f i) = ∑' (i : ι), μ (f i)
      theorem MeasureTheory.measure_union₀_aux {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (ht : MeasureTheory.NullMeasurableSet t μ) (hd : MeasureTheory.AEDisjoint μ s t) :
      μ (s t) = μ s + μ t
      theorem MeasureTheory.measure_inter_add_diff₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.NullMeasurableSet t μ) :
      μ (s t) + μ (s \ t) = μ s

      A null measurable set t is Carathéodory measurable: for any s, we have μ (s ∩ t) + μ (s \ t) = μ s.

      theorem MeasureTheory.measure_union_add_inter₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.NullMeasurableSet t μ) :
      μ (s t) + μ (s t) = μ s + μ t
      theorem MeasureTheory.measure_union_add_inter₀' {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (t : Set α) :
      μ (s t) + μ (s t) = μ s + μ t
      theorem MeasureTheory.measure_union₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasureTheory.NullMeasurableSet t μ) (hd : MeasureTheory.AEDisjoint μ s t) :
      μ (s t) = μ s + μ t
      theorem MeasureTheory.measure_union₀' {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hd : MeasureTheory.AEDisjoint μ s t) :
      μ (s t) = μ s + μ t
      theorem MeasureTheory.measure_add_measure_compl₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) :
      μ s + μ s = μ Set.univ
      theorem Set.Finite.nullMeasurableSet_biUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} {s : Set ι} (hs : s.Finite) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
      MeasureTheory.NullMeasurableSet (bs, f b) μ
      theorem Finset.nullMeasurableSet_biUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} (s : Finset ι) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
      MeasureTheory.NullMeasurableSet (bs, f b) μ
      theorem Set.Finite.nullMeasurableSet_sUnion {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} (hs : s.Finite) (h : ts, MeasureTheory.NullMeasurableSet t μ) :
      theorem Set.Finite.nullMeasurableSet_biInter {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} {s : Set ι} (hs : s.Finite) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
      MeasureTheory.NullMeasurableSet (bs, f b) μ
      theorem Finset.nullMeasurableSet_biInter {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} (s : Finset ι) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
      MeasureTheory.NullMeasurableSet (bs, f b) μ
      theorem Set.Finite.nullMeasurableSet_sInter {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} (hs : s.Finite) (h : ts, MeasureTheory.NullMeasurableSet t μ) :
      def MeasureTheory.NullMeasurable {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : αβ) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

      A function f : α → β is null measurable if the preimage of a measurable set is a null measurable set.

      Equations
      Instances For
        theorem Measurable.nullMeasurable {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} (h : Measurable f) :
        theorem MeasureTheory.Measurable.comp_nullMeasurable {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {μ : MeasureTheory.Measure α} {g : βγ} (hg : Measurable g) (hf : MeasureTheory.NullMeasurable f μ) :
        theorem MeasureTheory.NullMeasurable.congr {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {g : αβ} (hf : MeasureTheory.NullMeasurable f μ) (hg : f =ᵐ[μ] g) :

        A measure is complete if every null set is also measurable. A null set is a subset of a measurable set with measure 0. Since every measure is defined as a special case of an outer measure, we can more simply state that a set s is null if μ s = 0.

        Instances
          theorem MeasureTheory.Measure.IsComplete.out' {α : Type u_2} :
          ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : μ.IsComplete] (s : Set α), μ s = 0MeasurableSet s
          theorem MeasureTheory.Measure.isComplete_iff {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
          μ.IsComplete ∀ (s : Set α), μ s = 0MeasurableSet s
          theorem MeasureTheory.Measure.IsComplete.out {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (h : μ.IsComplete) (s : Set α) :
          μ s = 0MeasurableSet s
          theorem MeasureTheory.measurableSet_of_null {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [μ.IsComplete] (hs : μ s = 0) :
          theorem MeasureTheory.NullMeasurable.measurable_of_complete {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [μ.IsComplete] {_m1 : MeasurableSpace β} {f : αβ} (hf : MeasureTheory.NullMeasurable f μ) :
          theorem Measurable.congr_ae {α : Type u_5} {β : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [_hμ : μ.IsComplete] {f : αβ} {g : αβ} (hf : Measurable f) (hfg : f =ᵐ[μ] g) :

          Given a measure we can complete it to a (complete) measure on all null measurable sets.

          TODO: generalize to any larger σ-algebra.

          Equations
          • μ.completion = { toOuterMeasure := μ.toOuterMeasure, m_iUnion := , trim_le := }
          Instances For
            instance MeasureTheory.Measure.completion.isComplete {α : Type u_2} {_m : MeasurableSpace α} (μ : MeasureTheory.Measure α) :
            μ.completion.IsComplete
            Equations
            • =
            @[simp]
            theorem MeasureTheory.Measure.coe_completion {α : Type u_2} :
            ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.completion = μ
            theorem MeasureTheory.Measure.completion_apply {α : Type u_2} :
            ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.completion s = μ s