English
If f is a ring homomorphism bounded with respect to a ring seminorm nα and a powMul nβ, then for every x, nβ(f(x)) ≤ nα(x).
Русский
Если гомоморф f ограничена относительно норм-остатка nα и powMul nβ, тогда для любого x верно nβ(f(x)) ≤ nα(x).
LaTeX
$$nβ (f x) ≤ nα x$$
Lean4
/-- If `f : α →+* β` is bounded with respect to a ring seminorm `nα` on `α` and a
power-multiplicative function `nβ : β → ℝ`, then `∀ x : α, nβ (f x) ≤ nα x`. -/
theorem contraction_of_isPowMul_of_boundedWrt {F : Type*} {α : outParam (Type*)} [Ring α] [FunLike F α ℝ]
[RingSeminormClass F α ℝ] {β : Type*} [Ring β] (nα : F) {nβ : β → ℝ} (hβ : IsPowMul nβ) {f : α →+* β}
(hf : f.IsBoundedWrt nα nβ) (x : α) : nβ (f x) ≤ nα x :=
by
obtain ⟨C, hC0, hC⟩ := hf
have hlim : Tendsto (fun n : ℕ => C ^ (1 / (n : ℝ)) * nα x) atTop (𝓝 (nα x)) :=
by
nth_rewrite 2 [← one_mul (nα x)]
exact
((rpow_zero C ▸ ContinuousAt.tendsto (continuousAt_const_rpow (ne_of_gt hC0))).comp
(tendsto_const_div_atTop_nhds_zero_nat 1)).mul
tendsto_const_nhds
apply ge_of_tendsto hlim
simp only [eventually_atTop, ge_iff_le]
use 1
intro n hn
have h : (C ^ (1 / n : ℝ)) ^ n = C :=
by
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn)
rw [← rpow_natCast, ← rpow_mul (le_of_lt hC0), one_div, inv_mul_cancel₀ hn0, rpow_one]
apply le_of_pow_le_pow_left₀ (ne_of_gt hn) (mul_nonneg (rpow_nonneg (le_of_lt hC0) _) (apply_nonneg _ _))
· rw [mul_pow, h, ← hβ _ hn, ← RingHom.map_pow]
apply le_trans (hC (x ^ n))
rw [mul_le_mul_iff_right₀ hC0]
exact map_pow_le_pow _ _ (Nat.one_le_iff_ne_zero.mp hn)
