English
For any a and sequence u, the limsup of a times u equals a times the limsup of u (with a case split if a = ⊤).
Русский
Для любых a и последовательности u верно, что limsup (a·u) = a·limsup u (разделение случая, если a = ⊤).
LaTeX
$$$\\\\forall f : α \\\\to \\\\mathbb{R}_{\\\\ge 0,\\\\infty},\\\\; f.limsup (a \\\\cdot u) = a \\\\cdot f.limsup u$$$
Lean4
theorem limsup_const_mul [CountableInterFilter f] {u : α → ℝ≥0∞} {a : ℝ≥0∞} : f.limsup (a * u ·) = a * f.limsup u :=
by
by_cases ha_top : a ≠ ⊤
· exact limsup_const_mul_of_ne_top ha_top
push_neg at ha_top
by_cases hu : u =ᶠ[f] 0
· have hau : (a * u ·) =ᶠ[f] 0 := hu.mono fun x hx => by simp [hx]
simp only [limsup_congr hu, limsup_congr hau, Pi.zero_def, ← ENNReal.bot_eq_zero, limsup_const_bot]
simp
· have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ :=
by
rw [EventuallyEq, not_eventually] at hu
refine hu.mono fun x hx => ?_
rw [Pi.zero_apply] at hx
simp [hx]
have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
have hfu : f.limsup u ≠ 0 := mt limsup_eq_zero_iff.1 hu
simp only [ha_top, top_mul', h_top_le, hfu, ite_false]
