English
If a is a non-top ENNReal number, then limsup of a times a sequence equals a times limsup of the sequence.
Русский
Если a ≠ ⊤, то limsup a·u = a·limsup u.
LaTeX
$$$\\\\forall f : α \\\\to \\\\mathbb{R}_{\\\\ge 0,\\\\infty},\\\\; a \\\\neq \\\\top \\\\Rightarrow f.limsup (a \\\\cdot u) = a \\\\cdot f.limsup u$$$
Lean4
theorem limsup_const_mul_of_ne_top {u : α → ℝ≥0∞} {a : ℝ≥0∞} (ha_top : a ≠ ⊤) :
(f.limsup fun x : α => a * u x) = a * f.limsup u :=
by
by_cases ha_zero : a = 0
· simp_rw [ha_zero, zero_mul, ← ENNReal.bot_eq_zero]
exact limsup_const_bot
let g := fun x : ℝ≥0∞ => a * x
have hg_bij : Function.Bijective g :=
Function.bijective_iff_has_inverse.mpr
⟨fun x => a⁻¹ * x,
⟨fun x => by simp [g, ← mul_assoc, ENNReal.inv_mul_cancel ha_zero ha_top], fun x => by
simp [g, ← mul_assoc, ENNReal.mul_inv_cancel ha_zero ha_top]⟩⟩
have hg_mono : StrictMono g :=
Monotone.strictMono_of_injective (fun _ _ _ => by rwa [mul_le_mul_left ha_zero ha_top]) hg_bij.1
let g_iso := StrictMono.orderIsoOfSurjective g hg_mono hg_bij.2
exact (OrderIso.limsup_apply g_iso).symm
