English
If hv is nontrivial and the implication from v’s unit ball to w’s unit ball holds for all x, then v is equivalent to w.
Русский
Если hv не тривиально и выполняется переход от единичной области v к единичной области w для всех x, то v эквивалентно w.
LaTeX
$$$ (hv: v.IsNontrivial) \rightarrow (\forall x, v(x) < 1 \Rightarrow w(x) < 1) \Rightarrow (v IsEquiv w)$$$
Lean4
theorem isEquiv_of_lt_one_imp (hv : v.IsNontrivial) (h : ∀ x, v x < 1 → w x < 1) : v.IsEquiv w :=
by
refine isEquiv_iff_lt_one_iff.2 fun a ↦ ?_
rcases eq_or_ne a 0 with (rfl | ha₀)
· simp
refine ⟨h a, fun hw ↦ ?_⟩
let ⟨x₀, hx₀⟩ := hv.exists_abv_lt_one
have hpow (n : ℕ) (hv : 1 ≤ v a) : w x₀ < w a ^ n :=
by
rw [← one_mul (_ ^ _), ← mul_inv_lt_iff₀ (pow_pos (by simp_all) _), ← map_pow, ← map_inv₀, ← map_mul]
apply h
rw [map_mul, map_inv₀, map_pow, mul_inv_lt_iff₀ (pow_pos (by simp [ha₀]) _), one_mul]
exact lt_of_lt_of_le hx₀.2 <| one_le_pow₀ hv
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one (w.pos hx₀.1) hw
exact not_le.1 <| mt (hpow n) <| not_lt.2 hn.le
