English
The spectral norm is power-multiplicative: for all x and n ∈ ℕ, spectralNorm(x^n) = spectralNorm(x)^n.
Русский
Спектральная норма — степенная по умножению: для всех x и n ∈ ℕ выполняется spectralNorm(x^n) = spectralNorm(x)^n.
LaTeX
$$$\operatorname{IsPowMul}(\operatorname{spectralNorm}_{K,L})$; i.e., ∀x\in L, ∀n∈\mathbb{N}, \operatorname{spectralNorm}_{K,L}(x^n) = \operatorname{spectralNorm}_{K,L}(x)^n$$$
Lean4
/-- The spectral norm is a `K`-algebra norm on `L`. -/
def spectralAlgNorm : AlgebraNorm K L where
toFun := spectralNorm K L
map_zero' := spectralNorm_zero
add_le' _ _ := IsNonarchimedean.add_le spectralNorm_nonneg isNonarchimedean_spectralNorm
mul_le' x y := spectralNorm_mul (h_alg.isAlgebraic x) (h_alg.isAlgebraic y)
smul' k x := spectralNorm_smul k (h_alg.isAlgebraic x)
neg' x := spectralNorm_neg (h_alg.isAlgebraic x)
eq_zero_of_map_eq_zero' x hx := eq_zero_of_map_spectralNorm_eq_zero hx (h_alg.isAlgebraic x)
