Documentation

Mathlib.MeasureTheory.Covering.VitaliFamily

Vitali families #

On a metric space X with a measure μ, consider for each x : X a family of measurable sets with nonempty interiors, called setsAt x. This family is a Vitali family if it satisfies the following property: consider a (possibly non-measurable) set s, and for any x in s a subfamily f x of setsAt x containing sets of arbitrarily small diameter. Then one can extract a disjoint subfamily covering almost all s.

Vitali families are provided by covering theorems such as the Besicovitch covering theorem or the Vitali covering theorem. They make it possible to formulate general versions of theorems on differentiations of measure that apply in both contexts.

This file gives the basic definition of Vitali families. More interesting developments of this notion are deferred to other files:

Main definitions #

Let v be such a Vitali family.

References #

structure VitaliFamily {α : Type u_1} [MetricSpace α] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) :
Type u_1

On a metric space X with a measure μ, consider for each x : X a family of measurable sets with nonempty interiors, called setsAt x. This family is a Vitali family if it satisfies the following property: consider a (possibly non-measurable) set s, and for any x in s a subfamily f x of setsAt x containing sets of arbitrarily small diameter. Then one can extract a disjoint subfamily covering almost all s.

Vitali families are provided by covering theorems such as the Besicovitch covering theorem or the Vitali covering theorem. They make it possible to formulate general versions of theorems on differentiations of measure that apply in both contexts.

  • setsAt : αSet (Set α)

    Sets of the family "centered" at a given point.

  • measurableSet : ∀ (x : α), sself.setsAt x, MeasurableSet s

    All sets of the family are measurable.

  • nonempty_interior : ∀ (x : α), sself.setsAt x, (interior s).Nonempty

    All sets of the family have nonempty interior.

  • nontrivial : ∀ (x : α), ε > 0, sself.setsAt x, s Metric.closedBall x ε

    For any closed ball around x, there exists a set of the family contained in this ball.

  • covering : ∀ (s : Set α) (f : αSet (Set α)), (xs, f x self.setsAt x)(xs, ε > 0, af x, a Metric.closedBall x ε)∃ (t : Set (α × Set α)), (pt, p.1 s) (t.PairwiseDisjoint fun (p : α × Set α) => p.2) (pt, p.2 f p.1) μ (s \ pt, p.2) = 0

    Consider a (possibly non-measurable) set s, and for any x in s a subfamily f x of setsAt x containing sets of arbitrarily small diameter. Then one can extract a disjoint subfamily covering almost all s.

Instances For
    theorem VitaliFamily.measurableSet {α : Type u_1} [MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (self : VitaliFamily μ) (x : α) (s : Set α) :
    s self.setsAt xMeasurableSet s

    All sets of the family are measurable.

    theorem VitaliFamily.nonempty_interior {α : Type u_1} [MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (self : VitaliFamily μ) (x : α) (s : Set α) :
    s self.setsAt x(interior s).Nonempty

    All sets of the family have nonempty interior.

    theorem VitaliFamily.nontrivial {α : Type u_1} [MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (self : VitaliFamily μ) (x : α) (ε : ) :
    ε > 0sself.setsAt x, s Metric.closedBall x ε

    For any closed ball around x, there exists a set of the family contained in this ball.

    theorem VitaliFamily.covering {α : Type u_1} [MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (self : VitaliFamily μ) (s : Set α) (f : αSet (Set α)) :
    (xs, f x self.setsAt x)(xs, ε > 0, af x, a Metric.closedBall x ε)∃ (t : Set (α × Set α)), (pt, p.1 s) (t.PairwiseDisjoint fun (p : α × Set α) => p.2) (pt, p.2 f p.1) μ (s \ pt, p.2) = 0

    Consider a (possibly non-measurable) set s, and for any x in s a subfamily f x of setsAt x containing sets of arbitrarily small diameter. Then one can extract a disjoint subfamily covering almost all s.

    def VitaliFamily.mono {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (ν : MeasureTheory.Measure α) (hν : ν.AbsolutelyContinuous μ) :

    A Vitali family for a measure μ is also a Vitali family for any measure absolutely continuous with respect to μ.

    Equations
    • v.mono ν = let __spread.0 := v; { setsAt := __spread.0.setsAt, measurableSet := , nonempty_interior := , nontrivial := , covering := }
    Instances For
      def VitaliFamily.FineSubfamilyOn {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (f : αSet (Set α)) (s : Set α) :

      Given a Vitali family v for a measure μ, a family f is a fine subfamily on a set s if every point x in s belongs to arbitrarily small sets in v.setsAt x ∩ f x. This is precisely the subfamilies for which the Vitali family definition ensures that one can extract a disjoint covering of almost all s.

      Equations
      Instances For
        theorem VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) :
        ∃ (t : Set (α × Set α)), (pt, p.1 s) (t.PairwiseDisjoint fun (p : α × Set α) => p.2) (pt, p.2 v.setsAt p.1 f p.1) μ (s \ pt, p.2) = 0
        def VitaliFamily.FineSubfamilyOn.index {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) :
        Set (α × Set α)

        Given h : v.FineSubfamilyOn f s, then h.index is a set parametrizing a disjoint covering of almost every s.

        Equations
        • h.index = .choose
        Instances For
          def VitaliFamily.FineSubfamilyOn.covering {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (_h : v.FineSubfamilyOn f s) :
          α × Set αSet α

          Given h : v.FineSubfamilyOn f s, then h.covering p is a set in the family, for p ∈ h.index, such that these sets form a disjoint covering of almost every s.

          Equations
          • _h.covering p = p.2
          Instances For
            theorem VitaliFamily.FineSubfamilyOn.index_subset {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) (p : α × Set α) :
            p h.indexp.1 s
            theorem VitaliFamily.FineSubfamilyOn.covering_disjoint {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) :
            h.index.PairwiseDisjoint h.covering
            theorem VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) :
            Pairwise (Disjoint on fun (x : h.index) => h.covering x)
            theorem VitaliFamily.FineSubfamilyOn.covering_mem {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) {p : α × Set α} (hp : p h.index) :
            h.covering p f p.1
            theorem VitaliFamily.FineSubfamilyOn.covering_mem_family {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) {p : α × Set α} (hp : p h.index) :
            h.covering p v.setsAt p.1
            theorem VitaliFamily.FineSubfamilyOn.measure_diff_biUnion {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) :
            μ (s \ ph.index, h.covering p) = 0
            theorem VitaliFamily.FineSubfamilyOn.index_countable {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) [SecondCountableTopology α] :
            h.index.Countable
            theorem VitaliFamily.FineSubfamilyOn.measurableSet_u {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) {p : α × Set α} (hp : p h.index) :
            MeasurableSet (h.covering p)
            theorem VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) [SecondCountableTopology α] {ρ : MeasureTheory.Measure α} (hρ : ρ.AbsolutelyContinuous μ) :
            ρ s ∑' (p : h.index), ρ (h.covering p)
            theorem VitaliFamily.FineSubfamilyOn.measure_le_tsum {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ} {f : αSet (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s) [SecondCountableTopology α] :
            μ s ∑' (x : h.index), μ (h.covering x)
            def VitaliFamily.enlarge {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (δ : ) (δpos : 0 < δ) :

            One can enlarge a Vitali family by adding to the sets f x at x all sets which are not contained in a δ-neighborhood on x. This does not change the local filter at a point, but it can be convenient to get a nicer global behavior.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def VitaliFamily.filterAt {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (x : α) :
              Filter (Set α)

              Given a vitali family v, then v.filterAt x is the filter on Set α made of those families that contain all sets of v.setsAt x of a sufficiently small diameter. This filter makes it possible to express limiting behavior when sets in v.setsAt x shrink to x.

              Equations
              Instances For
                theorem Filter.HasBasis.vitaliFamily {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {ι : Sort u_2} {p : ιProp} {s : ιSet α} {x : α} (h : (nhds x).HasBasis p s) :
                (v.filterAt x).HasBasis p fun (i : ι) => {t : Set α | t v.setsAt x t s i}
                theorem VitaliFamily.filterAt_basis_closedBall {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (x : α) :
                (v.filterAt x).HasBasis (fun (x : ) => 0 < x) fun (x_1 : ) => {a : Set α | a v.setsAt x a Metric.closedBall x x_1}
                theorem VitaliFamily.mem_filterAt_iff {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {x : α} {s : Set (Set α)} :
                s v.filterAt x ε > 0, av.setsAt x, a Metric.closedBall x εa s
                instance VitaliFamily.filterAt_neBot {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (x : α) :
                (v.filterAt x).NeBot
                Equations
                • =
                theorem VitaliFamily.eventually_filterAt_iff {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {x : α} {P : Set αProp} :
                (∀ᶠ (a : Set α) in v.filterAt x, P a) ε > 0, av.setsAt x, a Metric.closedBall x εP a
                theorem VitaliFamily.tendsto_filterAt_iff {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {ι : Type u_2} {l : Filter ι} {f : ιSet α} {x : α} :
                Filter.Tendsto f l (v.filterAt x) (∀ᶠ (i : ι) in l, f i v.setsAt x) ε > 0, ∀ᶠ (i : ι) in l, f i Metric.closedBall x ε
                theorem VitaliFamily.eventually_filterAt_mem_setsAt {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (x : α) :
                ∀ᶠ (a : Set α) in v.filterAt x, a v.setsAt x
                theorem VitaliFamily.eventually_filterAt_subset_closedBall {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (x : α) {ε : } (hε : 0 < ε) :
                ∀ᶠ (a : Set α) in v.filterAt x, a Metric.closedBall x ε
                theorem VitaliFamily.eventually_filterAt_measurableSet {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (x : α) :
                ∀ᶠ (a : Set α) in v.filterAt x, MeasurableSet a
                theorem VitaliFamily.frequently_filterAt_iff {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {x : α} {P : Set αProp} :
                (∃ᶠ (a : Set α) in v.filterAt x, P a) ε > 0, av.setsAt x, a Metric.closedBall x ε P a
                theorem VitaliFamily.eventually_filterAt_subset_of_nhds {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {x : α} {o : Set α} (hx : o nhds x) :
                ∀ᶠ (a : Set α) in v.filterAt x, a o
                theorem VitaliFamily.fineSubfamilyOn_of_frequently {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (f : αSet (Set α)) (s : Set α) (h : xs, ∃ᶠ (a : Set α) in v.filterAt x, a f x) :
                v.FineSubfamilyOn f s