English
For a more complex finite index set, a constructive procedure yields a common a with prescribed inequivalent behavior across all indices.
Русский
Для более сложного конечного множества индексов существует конструктивная процедура, задающая единое a с требуемым поведением по отношению к всем индексам.
LaTeX
$$$ \forall \text{finite } I, \exists a, \bigwedge_{i \in I} (1 < v_i(a) \text{ or } v_i(a) < 1) $$$
Lean4
/-- If $v$ and $w$ are two real absolute values on a field $F$, equivalent in the sense that
$v(x) \leq v(y)$ if and only if $w(x) \leq w(y)$, then $\frac{\log (v(a))}{\log (w(a))}$ is
constant for all $0 \neq a\in F$ with $v(a) \neq 1$.
-/
theorem log_div_log_eq_log_div_log (h : v.IsEquiv w) {a : F} (ha₀ : a ≠ 0) (ha₁ : v a ≠ 1) {b : F} (hb₀ : b ≠ 0)
(hb₁ : v b ≠ 1) : (v b).log / (w b).log = (v a).log / (w a).log :=
by
by_contra! h_ne
wlog ha : 1 < v a generalizing a b
· apply this (inv_ne_zero ha₀) (by simpa) hb₀ hb₁ (by simpa)
simpa using one_lt_inv_iff₀.2 ⟨v.pos ha₀, ha₁.lt_of_le (not_lt.1 ha)⟩
wlog hb : 1 < v b generalizing a b
· apply this ha₀ ha₁ (inv_ne_zero hb₀) (by simpa) (by simpa) ha
simpa using one_lt_inv_iff₀.2 ⟨v.pos hb₀, hb₁.lt_of_le (not_lt.1 hb)⟩
wlog h_lt : (v b).log / (w b).log < (v a).log / (w a).log generalizing a b
· exact this hb₀ hb₁ ha₀ ha₁ h_ne.symm hb ha <| lt_of_le_of_ne (not_lt.1 h_lt) h_ne.symm
have hwa := h.one_lt_iff.1 ha
have hwb := h.one_lt_iff.1 hb
rw [div_lt_div_iff₀ (log_pos hwb) (log_pos hwa), mul_comm (v a).log, ←
div_lt_div_iff₀ (log_pos ha) (log_pos hwa)] at h_lt
let ⟨q, ⟨hq₁, hq₂⟩⟩ := exists_rat_btwn h_lt
rw [← Rat.num_div_den q, Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast] at hq₁ hq₂
rw [div_lt_div_iff₀ (log_pos ha) (by simp [q.den_pos]), mul_comm, ← log_pow, ← log_zpow,
log_lt_log_iff (pow_pos (by linarith) _) (zpow_pos (by linarith) _), ← div_lt_one (zpow_pos (by linarith) _), ←
map_pow, ← map_zpow₀, ← map_div₀] at hq₁
rw [div_lt_div_iff₀ (by simp [q.den_pos]) (log_pos hwa), mul_comm (w _).log, ← log_pow, ← log_zpow,
log_lt_log_iff (zpow_pos (by linarith) _) (pow_pos (by linarith) _), ← one_lt_div (zpow_pos (by linarith) _), ←
map_pow, ← map_zpow₀, ← map_div₀] at hq₂
exact not_lt_of_gt (h.lt_one_iff.1 hq₁) hq₂
