α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
have h₁ := blimsup_cthickening_ae_eq_blimsup_thickening (s := s) μ hr hr'
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
have h₂ := blimsup_cthickening_mul_ae_eq μ p s hM r hr
case hr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
⊢ Tendsto (fun i => M * r i) atTop (𝓝 0)

α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
replace hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
replace hr' : ∀ᶠ i in atTop, p i → 0 < M * r i := hr'.mono fun i hi hip => mul_pos hM (hi hip)
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i
h₃ :
  (blimsup (fun i => cthickening (M * r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (M * r i) (s i)) atTop fun i => p i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
have h₃ := blimsup_cthickening_ae_eq_blimsup_thickening (s := s) μ hr hr'
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
hr : Tendsto (fun i => M * r i) atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i
h₃ :
  (blimsup (fun i => cthickening (M * r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (M * r i) (s i)) atTop fun i => p i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
exact h₃.symm.trans (h₂.trans h₁)
case h.e'_5.h.e'_3
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
⊢ 0 = M * 0
case hr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
⊢ Tendsto (fun i => M * r i) atTop (𝓝 0)
convert hr.const_mul M
no goals
case h.e'_5.h.e'_3
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i) =ᵐ[μ]
    blimsup (fun i => thickening (r i) (s i)) atTop fun i => p i
h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
⊢ 0 = M * 0
simp