English
A technical lemma showing that dilating radii by a positive factor M (>0) preserves a.e. thickening relation, under appropriate hypotheses.
Русский
Дополнительная лемма: увеличение радиусов на положительный коэффициент сохраняет a.e. отношение утолщения при соответствующих гипотезах.
LaTeX
$$$(\blimsup (i \mapsto cthickening (M \cdot r i) (s i)) atTop p) =ᵐ[μ] (\blimsup (i \mapsto cthickening (r i) (s i)) atTop p).$$$
Lean4
/-- An auxiliary result en route to `blimsup_thickening_mul_ae_eq`. -/
theorem blimsup_thickening_mul_ae_eq_aux (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 : Set α) =ᵐ[μ]
(blimsup (fun i => thickening (r i) (s i)) atTop p : Set α) :=
by
have h₁ := blimsup_cthickening_ae_eq_blimsup_thickening (s := s) μ hr hr'
have h₂ := blimsup_cthickening_mul_ae_eq μ p s hM r hr
replace hr : Tendsto (fun i => M * r i) atTop (𝓝 0) := by convert hr.const_mul M; simp
replace hr' : ∀ᶠ i in atTop, p i → 0 < M * r i := hr'.mono fun i hi hip ↦ mul_pos hM (hi hip)
have h₃ := blimsup_cthickening_ae_eq_blimsup_thickening (s := s) μ hr hr'
exact h₃.symm.trans (h₂.trans h₁)
