English
The spectral norm is nonarchimedean in general: for any x,y ∈ L, spectralNorm(x+y) ≤ max(spectralNorm(x), spectralNorm(y)).
Русский
Спектральная норма в общем случае удовлетворяет неархимедову неравенство: spectralNorm(x+y) ≤ max(spectralNorm(x), spectralNorm(y)).
LaTeX
$$$\forall x,y \in L,\; \operatorname{spectralNorm}_{K,L}(x+y) \le \max\big(\operatorname{spectralNorm}_{K,L}(x), \operatorname{spectralNorm}_{K,L}(y)\big)$$$
Lean4
/-- The spectral norm is nonarchimedean. -/
theorem isNonarchimedean_spectralNorm : IsNonarchimedean (spectralNorm K L) :=
by
intro x y
set E := K⟮x, y⟯
haveI h_finiteDimensional_E : FiniteDimensional K E :=
IntermediateField.finiteDimensional_adjoin_pair (h_alg.isAlgebraic x).isIntegral (h_alg.isAlgebraic y).isIntegral
set gx := IntermediateField.AdjoinPair.gen₁ K x y
set gy := IntermediateField.AdjoinPair.gen₂ K x y
have hxy : x + y = (algebraMap K⟮x, y⟯ L) (gx + gy) := rfl
rw [hxy, ← spectralNorm.eq_of_normalClosure (gx + gy) hxy, ←
spectralNorm.eq_of_normalClosure gx (IntermediateField.AdjoinPair.algebraMap_gen₁ K x y), ←
spectralNorm.eq_of_normalClosure gy (IntermediateField.AdjoinPair.algebraMap_gen₂ K x y), _root_.map_add]
apply isNonarchimedean_spectralNorm_of_finiteDimensional_normal
