English
Uniformly locally doubling, scaling radii by a constant factor preserves almost-everywhere thickening behavior.
Русский
Универсально локально удваиваемая мера сохраняет поведение утолщения под умножением радиуса на константу.
LaTeX
$$$\forall M>0,\ (\blimsup (i \mapsto thickening (M \cdot r i) (s i)) atTop\ p) =ᵐ[μ] (\blimsup (i \mapsto thickening (r i) (s i)) atTop\ p).$$$
Lean4
/-- This is really 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. -/
theorem blimsup_cthickening_ae_le_of_eventually_mul_le (p : ℕ → Prop) {s : ℕ → Set α} {M : ℝ} (hM : 0 < M)
{r₁ r₂ : ℕ → ℝ} (hr : Tendsto r₁ atTop (𝓝[>] 0)) (hMr : ∀ᶠ i in atTop, M * r₁ i ≤ r₂ i) :
(blimsup (fun i => cthickening (r₁ i) (s i)) atTop p : Set α) ≤ᵐ[μ]
(blimsup (fun i => cthickening (r₂ i) (s i)) atTop p : Set α) :=
by
let R₁ i := max 0 (r₁ i)
let R₂ i := max 0 (r₂ i)
have hRp : 0 ≤ R₁ := fun i => le_max_left 0 (r₁ i)
replace hMr : ∀ᶠ i in atTop, M * R₁ i ≤ R₂ i :=
by
refine hMr.mono fun i hi ↦ ?_
rw [mul_max_of_nonneg _ _ hM.le, mul_zero]
exact max_le_max (le_refl 0) hi
simp_rw [← cthickening_max_zero (r₁ _), ← cthickening_max_zero (r₂ _)]
rcases le_or_gt 1 M with hM' | hM'
· apply HasSubset.Subset.eventuallyLE
change _ ≤ _
refine mono_blimsup' (hMr.mono fun i hi _ => cthickening_mono ?_ (s i))
exact (le_mul_of_one_le_left (hRp i) hM').trans hi
· simp only [← @cthickening_closure _ _ _ (s _)]
have hs : ∀ i, IsClosed (closure (s i)) := fun i => isClosed_closure
exact blimsup_cthickening_ae_le_of_eventually_mul_le_aux μ p hs (tendsto_nhds_max_right hr) hRp hM hM' hMr
