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: #

blimsup_cthickening_mul_ae_eq: the limsup of the closed thickening of a sequence of subsets of a metric space is unchanged almost everywhere for a uniformly locally doubling measure if the sequence of distances is multiplied by a positive scale factor. This is a generalisation of a result of Cassels, appearing as Lemma 9 on page 217 of J.W.S. Cassels, Some metrical theorems in Diophantine approximation. I.
blimsup_thickening_mul_ae_eq: a variant of blimsup_cthickening_mul_ae_eq for thickenings rather than closed thickenings.

source

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) :

filter.blimsup (λ (i : ℕ), metric.cthickening (r₁ i) (s i)) filter.at_top p ≤ᵐ[μ] filter.blimsup (λ (i : ℕ), metric.cthickening (r₂ i) (s i)) filter.at_top p

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.

source

theorem blimsup_cthickening_ae_le_of_eventually_mul_le {α : 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 α} {M : ℝ} (hM : 0 < M) {r₁ r₂ : ℕ → ℝ} (hr : filter.tendsto r₁ filter.at_top (nhds_within 0 (set.Ioi 0))) (hMr : ∀ᶠ (i : ℕ) in filter.at_top , M * r₁ i ≤ r₂ i) :

filter.blimsup (λ (i : ℕ), metric.cthickening (r₁ i) (s i)) filter.at_top p ≤ᵐ[μ] filter.blimsup (λ (i : ℕ), metric.cthickening (r₂ i) (s i)) filter.at_top p

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.

source

theorem blimsup_cthickening_mul_ae_eq {α : 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 α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ) (hr : filter.tendsto r filter.at_top (nhds 0)) :

filter.blimsup (λ (i : ℕ), metric.cthickening (M * r i) (s i)) filter.at_top p =ᵐ[μ] filter.blimsup (λ (i : ℕ), metric.cthickening (r i) (s i)) filter.at_top p

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.

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

source

theorem blimsup_cthickening_ae_eq_blimsup_thickening {α : 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 α} {r : ℕ → ℝ} (hr : filter.tendsto r filter.at_top (nhds 0)) (hr' : ∀ᶠ (i : ℕ) in filter.at_top , p i → 0 < r i) :

filter.blimsup (λ (i : ℕ), metric.cthickening (r i) (s i)) filter.at_top p =ᵐ[μ] filter.blimsup (λ (i : ℕ), metric.thickening (r i) (s i)) filter.at_top p

source

theorem blimsup_thickening_mul_ae_eq_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 α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ) (hr : filter.tendsto r filter.at_top (nhds 0)) (hr' : ∀ᶠ (i : ℕ) in filter.at_top , p i → 0 < r i) :

filter.blimsup (λ (i : ℕ), metric.thickening (M * r i) (s i)) filter.at_top p =ᵐ[μ] filter.blimsup (λ (i : ℕ), metric.thickening (r i) (s i)) filter.at_top p

An auxiliary result en route to blimsup_thickening_mul_ae_eq.

source

theorem blimsup_thickening_mul_ae_eq {α : 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 α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ) (hr : filter.tendsto r filter.at_top (nhds 0)) :

filter.blimsup (λ (i : ℕ), metric.thickening (M * r i) (s i)) filter.at_top p =ᵐ[μ] filter.blimsup (λ (i : ℕ), metric.thickening (r i) (s i)) filter.at_top p

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.

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