English
If f is not bounded and not trivial, then f is equivalent to the real absolute value.
Русский
Если f не ограничено и не тривиально, то f эквивалентно действительному абсолютному значению.
LaTeX
$$f IsEquiv real$$
Lean4
/-- If `f` is not bounded and not trivial, then it is equivalent to the standard absolute value on
`ℚ`. -/
theorem equiv_real_of_unbounded : f.IsEquiv real :=
by
obtain ⟨m, hm⟩ := Classical.exists_not_of_not_forall notbdd
have oneltm : 1 < m := by
contrapose! hm
rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl <;> simp
rw [← exists_nat_rpow_iff_isEquiv]
set s := logb m (f m) with hs
refine ⟨s⁻¹, inv_pos.mpr (logb_pos (Nat.one_lt_cast.mpr oneltm) (one_lt_of_not_bounded notbdd oneltm)), fun n ↦ ?_⟩
rcases lt_trichotomy n 1 with h | rfl | h
· obtain rfl : n = 0 := by cutsat
have : (logb (↑m) (f ↑m))⁻¹ ≠ 0 :=
by
simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero, not_or]
exact
⟨ne_zero_of_lt oneltm, oneltm.ne', by norm_cast, ne_zero_of_lt oneltm, ne_of_not_le hm, by
linarith only [apply_nonneg f ↑m]⟩
simp [hs, this]
· simp
· simp only [real_eq_abs, abs_cast, Rat.cast_natCast]
rw [rpow_inv_eq (apply_nonneg f ↑n) (Nat.cast_nonneg n)
(logb_ne_zero_of_pos_of_ne_one (one_lt_cast.mpr oneltm) (by linarith only [hm]) (by linarith only [hm]))]
have hfm : f m = m ^ s := by
rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]
have hfn : f n = n ^ logb n (f n) := by
rw [rpow_logb (mod_cast zero_lt_of_lt h) (mod_cast h.ne')
(by apply map_pos_of_ne_zero; exact_mod_cast ne_zero_of_lt h)]
rwa [← hs, eq_of_eq_pow oneltm h notbdd hfm hfn]
