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

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.

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.

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.

An auxiliary result en route to `blimsup_thickening_mul_ae_eq`

.

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`

.

`: Set α`

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