Theorems · Theorem · measure theory

blimsup_cthickening_ae_eq_blimsup_thickening

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] {p : ℕ → Prop}
  {s : ℕ → Set α} {r : ℕ → ℝ},
  Filter.Tendsto r Filter.atTop (nhds 0) →
    (∀ᶠ (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

Defined in

Mathlib.MeasureTheory.Covering.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsLocallyFiniteMeasureIsUnifLocDoublingMeasure