mathlib3 documentation

measure_theory.covering.liminf_limsup

Liminf, limsup, and uniformly locally doubling measures. #

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

This file is a place to collect lemmas about liminf and limsup for subsets of a metric space carrying a uniformly locally doubling measure.

Main results: #

theorem blimsup_cthickening_ae_le_of_eventually_mul_le_aux {α : Type u_1} [metric_space α] [topological_space.second_countable_topology α] [measurable_space α] [borel_space α] (μ : measure_theory.measure α) [measure_theory.is_locally_finite_measure μ] [is_unif_loc_doubling_measure μ] (p : Prop) {s : set α} (hs : (i : ), is_closed (s i)) {r₁ r₂ : } (hr : filter.tendsto r₁ filter.at_top (nhds_within 0 (set.Ioi 0))) (hrp : 0 r₁) {M : } (hM : 0 < M) (hM' : M < 1) (hMr : ∀ᶠ (i : ) in filter.at_top, M * r₁ i r₂ i) :

This is really an auxiliary result en route to blimsup_cthickening_ae_le_of_eventually_mul_le (which is itself an auxiliary result en route to blimsup_cthickening_mul_ae_eq).

NB: The set : α type ascription is present because of issue #16932 on GitHub.

This is really an auxiliary result en route to blimsup_cthickening_mul_ae_eq.

NB: The set : α type ascription is present because of issue #16932 on GitHub.

Given a sequence of subsets sᵢ of a metric space, together with a sequence of radii rᵢ such that rᵢ → 0, the set of points which belong to infinitely many of the closed rᵢ-thickenings of sᵢ is unchanged almost everywhere for a uniformly locally doubling measure if the rᵢ are all scaled by a positive constant.

This lemma is a generalisation of Lemma 9 appearing on page 217 of J.W.S. Cassels, Some metrical theorems in Diophantine approximation. I.

See also blimsup_thickening_mul_ae_eq.

NB: The set : α type ascription is present because of issue #16932 on GitHub.

Given a sequence of subsets sᵢ of a metric space, together with a sequence of radii rᵢ such that rᵢ → 0, the set of points which belong to infinitely many of the rᵢ-thickenings of sᵢ is unchanged almost everywhere for a uniformly locally doubling measure if the rᵢ are all scaled by a positive constant.

This lemma is a generalisation of Lemma 9 appearing on page 217 of J.W.S. Cassels, Some metrical theorems in Diophantine approximation. I.

See also blimsup_cthickening_mul_ae_eq.

NB: The set : α type ascription is present because of issue #16932 on GitHub.