English
Given hμ1 and hna, smoothingSeminorm μ hμ1 hna is a RingSeminorm on R, i.e., a seminorm with algebraic compatibility.
Русский
При заданных hμ1 и hna, сглаживающая семиноморма μ обладает структурой кольцевой семиномормы на R.
LaTeX
$$smoothingSeminorm μ hμ1 hna : RingSeminorm R$$
Lean4
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingFun` is a ring seminorm. -/
def smoothingSeminorm (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean μ) : RingSeminorm R
where
toFun := smoothingFun μ
map_zero' :=
by
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 0) tendsto_const_nhds
simp only [EventuallyEq, eventually_atTop, ge_iff_le]
use 1
intro n hn
simp only [smoothingSeminormSeq]
rw [zero_pow (pos_iff_ne_zero.mp hn), map_zero, zero_rpow]
exact one_div_ne_zero (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn))
add_le' _ _ := (isNonarchimedean_smoothingFun μ hμ1 hna).add_le (smoothingFun_nonneg μ hμ1)
neg'
n := by
simp only [smoothingFun]
congr
ext n
rw [neg_pow]
rcases neg_one_pow_eq_or R n with hpos | hneg
· rw [hpos, one_mul]
· rw [hneg, neg_one_mul, map_neg_eq_map μ]
mul_le' x
y :=
by
apply
le_of_tendsto_of_tendsto' (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (x * y))
(Tendsto.mul (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x) (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y))
intro n
have hn : 0 ≤ 1 / (n : ℝ) := by simp only [one_div, inv_nonneg, cast_nonneg]
simp only [smoothingSeminormSeq]
rw [← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _), mul_pow]
exact rpow_le_rpow (apply_nonneg μ _) (map_mul_le_mul μ _ _) hn
