mathlib3 documentation

measure_theory.covering.vitali_family

Vitali families #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

On a metric space X with a measure μ, consider for each x : X a family of measurable sets with nonempty interiors, called sets_at 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 sets_at 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:

constructions of specific Vitali families are provided by the Besicovitch covering theorem, in besicovitch.vitali_family, and by the Vitali covering theorem, in vitali.vitali_family.
The main theorem on differentiation of measures along a Vitali family is proved in vitali_family.ae_tendsto_rn_deriv.

Main definitions #

vitali_family μ is a structure made, for each x : X, of a family of sets around x, such that one can extract an almost everywhere disjoint covering from any subfamily containing sets of arbitrarily small diameters.

Let v be such a Vitali family.

v.fine_subfamily_on describes the subfamilies of v from which one can extract almost everywhere disjoint coverings. This property, called v.fine_subfamily_on.exists_disjoint_covering_ae, is essentially a restatement of the definition of a Vitali family. We also provide an API to use efficiently such a disjoint covering.
v.filter_at x is a filter on sets of X, such that convergence with respect to this filter means convergence when sets in the Vitali family shrink towards x.

References #

Herbert Federer, Geometric Measure Theory, Chapter 2.8 (Vitali families are called Vitali relations there)

@[nolint]

structure vitali_family {α : Type u_1} [metric_space α] {m : measurable_space α} (μ : measure_theory.measure α) :

Type u_1

sets_at : α → set (set α)
measurable_set' : ∀ (x : α) (a : set α), a ∈ self.sets_at x → measurable_set a
nonempty_interior : ∀ (x : α) (y : set α), y ∈ self.sets_at x → (interior y).nonempty
nontrivial : ∀ (x : α) (ε : ℝ), ε > 0 → (∃ (y : set α) (H : y ∈ self.sets_at x), y ⊆ metric.closed_ball x ε)
covering : ∀ (s : set α) (f : α → set (set α)), (∀ (x : α), x ∈ s → f x ⊆ self.sets_at x) → (∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → (∃ (a : set α) (H : a ∈ f x), a ⊆ metric.closed_ball x ε)) → (∃ (t : set (α × set α)), (∀ (p : α × set α), p ∈ t → p.fst ∈ s) ∧ t.pairwise_disjoint (λ (p : α × set α), p.snd) ∧ (∀ (p : α × set α), p ∈ t → p.snd ∈ f p.fst) ∧ ⇑μ (s \ ⋃ (p : α × set α) (hp : p ∈ t), p.snd) = 0)

On a metric space X with a measure μ, consider for each x : X a family of measurable sets with nonempty interiors, called sets_at 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 sets_at 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.

Instances for vitali_family

vitali_family.has_sizeof_inst

def vitali_family.mono {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (ν : measure_theory.measure α) (hν : ν.absolutely_continuous μ) :

vitali_family ν

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

Equations

v.mono ν hν = {sets_at := v.sets_at, measurable_set' := _, nonempty_interior := _, nontrivial := _, covering := _}

def vitali_family.fine_subfamily_on {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (f : α → set (set α)) (s : set α) :

Prop

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.sets_at 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

v.fine_subfamily_on f s = ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → (∃ (a : set α) (H : a ∈ v.sets_at x ∩ f x), a ⊆ metric.closed_ball x ε)

theorem vitali_family.fine_subfamily_on.exists_disjoint_covering_ae {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) :

∃ (t : set (α × set α)), (∀ (p : α × set α), p ∈ t → p.fst ∈ s) ∧ t.pairwise_disjoint (λ (p : α × set α), p.snd) ∧ (∀ (p : α × set α), p ∈ t → p.snd ∈ v.sets_at p.fst ∩ f p.fst) ∧ ⇑μ (s \ ⋃ (p : α × set α) (hp : p ∈ t), p.snd) = 0

@[protected]

def vitali_family.fine_subfamily_on.index {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) :

set (α × set α)

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

Equations

h.index = _.some

@[protected, nolint]

def vitali_family.fine_subfamily_on.covering {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) :

α × set α → set α

Given h : v.fine_subfamily_on 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 : α × set α), p.snd

theorem vitali_family.fine_subfamily_on.index_subset {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) (p : α × set α) :

p ∈ h.index → p.fst ∈ s

theorem vitali_family.fine_subfamily_on.covering_disjoint {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) :

h.index.pairwise_disjoint h.covering

theorem vitali_family.fine_subfamily_on.covering_disjoint_subtype {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) :

pairwise (disjoint on λ (x : ↥(h.index)), h.covering ↑x)

theorem vitali_family.fine_subfamily_on.covering_mem {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) {p : α × set α} (hp : p ∈ h.index) :

h.covering p ∈ f p.fst

theorem vitali_family.fine_subfamily_on.covering_mem_family {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) {p : α × set α} (hp : p ∈ h.index) :

h.covering p ∈ v.sets_at p.fst

theorem vitali_family.fine_subfamily_on.measure_diff_bUnion {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) :

⇑μ (s \ ⋃ (p : α × set α) (H : p ∈ h.index), h.covering p) = 0

theorem vitali_family.fine_subfamily_on.index_countable {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) [topological_space.second_countable_topology α] :

h.index.countable

@[protected]

theorem vitali_family.fine_subfamily_on.measurable_set_u {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) {p : α × set α} (hp : p ∈ h.index) :

measurable_set (h.covering p)

theorem vitali_family.fine_subfamily_on.measure_le_tsum_of_absolutely_continuous {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) [topological_space.second_countable_topology α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :

⇑ρ s ≤ ∑' (p : ↥(h.index)), ⇑ρ (h.covering ↑p)

theorem vitali_family.fine_subfamily_on.measure_le_tsum {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} {v : vitali_family μ} {f : α → set (set α)} {s : set α} (h : v.fine_subfamily_on f s) [topological_space.second_countable_topology α] :

⇑μ s ≤ ∑' (x : ↥(h.index)), ⇑μ (h.covering ↑x)

def vitali_family.enlarge {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (δ : ℝ) (δpos : 0 < δ) :

vitali_family μ

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

v.enlarge δ δpos = {sets_at := λ (x : α), v.sets_at x ∪ {a : set α | measurable_set a ∧ (interior a).nonempty ∧ ¬a ⊆ metric.closed_ball x δ}, measurable_set' := _, nonempty_interior := _, nontrivial := _, covering := _}

def vitali_family.filter_at {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (x : α) :

filter (set α)

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

Equations

v.filter_at x = ⨅ (ε : ℝ) (H : ε ∈ set.Ioi 0), filter.principal {a ∈ v.sets_at x | a ⊆ metric.closed_ball x ε}

Instances for vitali_family.filter_at

vitali_family.filter_at_ne_bot

theorem vitali_family.mem_filter_at_iff {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {x : α} {s : set (set α)} :

s ∈ v.filter_at x ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ (a : set α), a ∈ v.sets_at x → a ⊆ metric.closed_ball x ε → a ∈ s

@[protected, instance]

def vitali_family.filter_at_ne_bot {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (x : α) :

(v.filter_at x).ne_bot

theorem vitali_family.eventually_filter_at_iff {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {x : α} {P : set α → Prop} :

(∀ᶠ (a : set α) in v.filter_at x, P a) ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ (a : set α), a ∈ v.sets_at x → a ⊆ metric.closed_ball x ε → P a

theorem vitali_family.eventually_filter_at_mem_sets {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (x : α) :

∀ᶠ (a : set α) in v.filter_at x, a ∈ v.sets_at x

theorem vitali_family.eventually_filter_at_subset_closed_ball {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (x : α) {ε : ℝ} (hε : 0 < ε) :

∀ᶠ (a : set α) in v.filter_at x, a ⊆ metric.closed_ball x ε

theorem vitali_family.tendsto_filter_at_iff {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {ι : Type u_2} {l : filter ι} {f : ι → set α} {x : α} :

filter.tendsto f l (v.filter_at x) ↔ (∀ᶠ (i : ι) in l, f i ∈ v.sets_at x) ∧ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (i : ι) in l, f i ⊆ metric.closed_ball x ε)

theorem vitali_family.eventually_filter_at_measurable_set {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (x : α) :

∀ᶠ (a : set α) in v.filter_at x, measurable_set a

theorem vitali_family.frequently_filter_at_iff {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {x : α} {P : set α → Prop} :

(∃ᶠ (a : set α) in v.filter_at x, P a) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (a : set α) (H : a ∈ v.sets_at x), a ⊆ metric.closed_ball x ε ∧ P a)

theorem vitali_family.eventually_filter_at_subset_of_nhds {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {x : α} {o : set α} (hx : o ∈ nhds x) :

∀ᶠ (a : set α) in v.filter_at x, a ⊆ o

theorem vitali_family.fine_subfamily_on_of_frequently {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (f : α → set (set α)) (s : set α) (h : ∀ (x : α), x ∈ s → (∃ᶠ (a : set α) in v.filter_at x, a ∈ f x)) :

v.fine_subfamily_on f s