English
For nonnegative v, if u ~ v, then u^r ~ v^r for any real r.
Русский
При двум функциями u и v, где u ≈ v и v ≥ 0, возведение в степень r сохраняет эквивалентность: u^r ~ v^r.
LaTeX
$$$u^r \sim_l v^r$ given $u \sim_l v$ and $v \ge 0$$$
Lean4
theorem rpow {α : Type*} {u v : α → ℝ} {l : Filter α} (hv : 0 ≤ v) (h : u ~[l] v) {r : ℝ} : u ^ r ~[l] v ^ r :=
by
obtain ⟨φ, hφ, huφv⟩ := IsEquivalent.exists_eq_mul h
rw [isEquivalent_iff_exists_eq_mul]
have hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1) :=
by
rw [← Real.one_rpow r]
exact Tendsto.comp (Real.continuousAt_rpow_const _ _ (by left; norm_num)) hφ
use (· ^ r) ∘ φ, hφr
conv => enter [3]; change fun x ↦ φ x ^ r * v x ^ r
filter_upwards [Tendsto.eventually_const_lt (zero_lt_one) hφ, huφv] with x hφ_pos huv'
simp [← Real.mul_rpow (le_of_lt hφ_pos) (hv x), huv']
