Liminf, limsup, and uniformly locally doubling measures.

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.

theorem blimsup_cthickening_ae_le_of_eventually_mul_le_aux {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) {s : ℕ → Set α} (hs : ∀ (i : ℕ), IsClosed (s i)) {r₁ : ℕ → ℝ} {r₂ : ℕ → ℝ} (hr : Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (hrp : 0 ≤ r₁) {M : ℝ} (hM : 0 < M) (hM' : M < 1) (hMr : ∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) : Filter.blimsup (fun (i : ℕ) => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ] Filter.blimsup (fun (i : ℕ) => Metric.cthickening (r₂ i) (s i)) Filter.atTop 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 https://github.com/leanprover-community/mathlib/issues/16932.

theorem blimsup_cthickening_ae_le_of_eventually_mul_le {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) {s : ℕ → Set α} {M : ℝ} (hM : 0 < M) {r₁ : ℕ → ℝ} {r₂ : ℕ → ℝ} (hr : Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (hMr : ∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) : Filter.blimsup (fun (i : ℕ) => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ] Filter.blimsup (fun (i : ℕ) => Metric.cthickening (r₂ i) (s i)) Filter.atTop p

This is really an auxiliary result en route to blimsup_cthickening_mul_ae_eq.

NB: The : Set α type ascription is present because of https://github.com/leanprover-community/mathlib/issues/16932.

theorem blimsup_cthickening_mul_ae_eq {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.blimsup (fun (i : ℕ) => Metric.cthickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun (i : ℕ) => Metric.cthickening (r i) (s i)) Filter.atTop 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.

See also blimsup_thickening_mul_ae_eq.

NB: The : Set α type ascription is present because of https://github.com/leanprover-community/mathlib/issues/16932.

theorem blimsup_cthickening_ae_eq_blimsup_thickening {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] {p : ℕ → Prop} {s : ℕ → Set α} {r : ℕ → ℝ} (hr : Filter.Tendsto r Filter.atTop (nhds 0)) (hr' : ∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i) : Filter.blimsup (fun (i : ℕ) => Metric.cthickening (r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun (i : ℕ) => Metric.thickening (r i) (s i)) Filter.atTop p

theorem blimsup_thickening_mul_ae_eq_aux {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) (hr' : ∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i) : Filter.blimsup (fun (i : ℕ) => Metric.thickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun (i : ℕ) => Metric.thickening (r i) (s i)) Filter.atTop p

An auxiliary result en route to blimsup_thickening_mul_ae_eq.

theorem blimsup_thickening_mul_ae_eq {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.blimsup (fun (i : ℕ) => Metric.thickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun (i : ℕ) => Metric.thickening (r i) (s i)) Filter.atTop 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.

See also blimsup_cthickening_mul_ae_eq.

NB: The : Set α type ascription is present because of https://github.com/leanprover-community/mathlib/issues/16932.