Theorems · Theorem · measure theory

blimsup_cthickening_ae_le_of_eventually_mul_le_aux

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

Defined in

Mathlib.MeasureTheory.Covering.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsLocallyFiniteMeasureIsUnifLocDoublingMeasure