Theorems · Theorem · measure theory

blimsup_thickening_mul_ae_eq_aux

∀ {α : 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) →
        (∀ᶠ (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.

Defined in

Mathlib.MeasureTheory.Covering.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsLocallyFiniteMeasureIsUnifLocDoublingMeasure