isNonarchimedean_spectralNorm_of_finiteDimensional_normal

English

The spectral norm is nonarchimedean, i.e., it satisfies the ultrametric inequality: for all x,y in L, spectralNorm(x+y) ≤ max(spectralNorm(x), spectralNorm(y)).

Русский

Спектральная норма удовлетворяет неархимедовуне неравенство: для любых x,y ∈ L выполняется 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 when `L/K` is finite and normal.
  See also `isNonarchimedean_spectralNorm` for a more general result. -/
theorem isNonarchimedean_spectralNorm_of_finiteDimensional_normal [IsUltrametricDist K] :
    IsNonarchimedean (spectralNorm K L) :=
  by
  rw [spectralNorm_eq_invariantExtension]
  exact isNonarchimedean_invariantExtension K L

Похожие утверждения