English
The definition of algNormFromConst equates the constructed normFromConst with the semicircular form built from spectralNorm.
Русский
Определение algNormFromConst совпадает с нормой, строимой через spectralNorm и соответствующими константами.
LaTeX
$$algNormFromConst(h1 hx y) = seminormFromConst(h1 hx' isPowMul_spectralNorm y)$$
Lean4
/-- Given a nonzero `x : L`, and assuming that `(spectralAlgNorm h_alg hna) 1 ≤ 1`, this is
the real-valued function sending `y ∈ L` to the limit of `(f (y * x^n))/((f x)^n)`,
regarded as an algebra norm. -/
def algNormFromConst (h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1) {x : L} (hx : x ≠ 0) : AlgebraNorm K L :=
have hx' : spectralAlgNorm K L x ≠ 0 := ne_of_gt (spectralNorm_zero_lt hx (Algebra.IsAlgebraic.isAlgebraic x))
{ normFromConst h1 hx' spectralAlgNorm_isPowMul with
smul' k
y :=
by
have h_mul :
∀ y : L, spectralNorm K L (algebraMap K L k * y) = spectralNorm K L (algebraMap K L k) * spectralNorm K L y :=
fun y ↦ by
rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def, map_smul_eq_mul _ _ _, spectralAlgNorm_def]
have h :
spectralNorm K L (algebraMap K L k) = seminormFromConst' h1 hx' isPowMul_spectralNorm (algebraMap K L k) := by
rw [seminormFromConst_apply_of_isMul h1 hx' _ h_mul]; rfl
rw [← @spectralNorm_extends K _ L _ _ k, Algebra.smul_def, h]
exact seminormFromConst_isMul_of_isMul _ _ _ h_mul _ }
