English
If v and w are equivalent absolute values, then the associated WithAbs.equivWithAbs is a homeomorphism.
Русский
Если v и w эквивалентны, то соответствующая WithAbs.equivWithAbs является гомеоморфизмом.
LaTeX
$$$ (v IsEquiv w) \Rightarrow IsHomeomorph (WithAbs.equivWithAbs v w)$$$
Lean4
/-- If `v` and `w` are two real absolute values on a field `F`, then `v` and `w` are equivalent if
and only if there exists a positive real constant `c` such that for all `x : R`, `(f x)^c = g x`.
-/
theorem isEquiv_iff_exists_rpow_eq {v w : AbsoluteValue F ℝ} : v.IsEquiv w ↔ ∃ c : ℝ, 0 < c ∧ (v · ^ c) = w :=
by
refine ⟨fun h ↦ ?_, fun ⟨t, ht, h⟩ ↦ isEquiv_iff_lt_one_iff.2 fun x ↦ h ▸ (rpow_lt_one_iff' (v.nonneg x) ht).symm⟩
by_cases hw : w.IsNontrivial
· let ⟨a, ha₀, ha₁⟩ := hw
refine ⟨(w a).log / (v a).log, h.log_div_log_pos ha₀ ha₁, funext fun b ↦ ?_⟩
rcases eq_or_ne b 0 with rfl | hb₀; · simp [zero_rpow (by linarith [h.log_div_log_pos ha₀ ha₁])]
rcases eq_or_ne (w b) 1 with hb₁ | hb₁; · simp [hb₁, h.eq_one_iff.2 hb₁]
rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
·
exact
⟨1, zero_lt_one, funext fun x ↦ by rcases eq_or_ne x 0 with rfl | h₀ <;> aesop (add simp [h.isNontrivial_congr])⟩
