Theorems · Theorem · measure theory

blimsup_cthickening_mul_ae_eq

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  (s : ℕ → Set α) {M : ℝ},
  0 < M →
    ∀ (r : ℕ → ℝ),
      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](cassels1950). See also blimsup_thickening_mul_ae_eq. NB: The : Set α type ascription is present because of https://github.com/leanprover-community/mathlib/issues/16932.

Defined in

Mathlib.MeasureTheory.Covering.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

Depth 222 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsLocallyFiniteMeasureIsUnifLocDoublingMeasure