English
The spectral norm is submultiplicative: spectralNorm(x y) ≤ spectralNorm(x) · spectralNorm(y) for algebraic x,y.
Русский
Спектральная норма субумножима: spectralNorm(xy) ≤ spectralNorm(x) · spectralNorm(y) для алгебраических x, y.
LaTeX
$$$\operatorname{spectralNorm}_{K,L}(xy) \le \operatorname{spectralNorm}_{K,L}(x)\cdot \operatorname{spectralNorm}_{K,L}(y)$$$
Lean4
/-- The spectral norm is submultiplicative. -/
theorem spectralNorm_mul {x y : L} (hx : IsAlgebraic K x) (hy : IsAlgebraic K y) :
spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y :=
by
set E := K⟮x, y⟯
haveI h_finiteDimensional_E : FiniteDimensional K E :=
IntermediateField.finiteDimensional_adjoin_pair hx.isIntegral hy.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), map_mul, ←
spectralAlgNorm_of_finiteDimensional_normal_def]
exact map_mul_le_mul _ _ _
