Documentation

Mathlib.MeasureTheory.Covering.LiminfLimsup

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

theorem blimsup_cthickening_ae_le_of_eventually_mul_le_aux {α : Type u_1} [MetricSpace α] [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} [MetricSpace α] [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} [MetricSpace α] [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} [MetricSpace α] [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 i0 < 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} [MetricSpace α] [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 i0 < 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} [MetricSpace α] [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.