English
For any r in R, spectralValue(X − C r) = ∥r∥.
Русский
Для любого r∈R спектральное значение X − C r равно ∥r∥.
LaTeX
$$$$\operatorname{spectralValue}(X - C r) = \|r\|.$$$$
Lean4
/-- The polynomial `X - r` has spectral value `‖ r ‖`. -/
theorem spectralValue_X_sub_C (r : R) : spectralValue (X - C r) = ‖r‖ :=
by
rw [spectralValue]
unfold spectralValueTerms
simp only [natDegree_X_sub_C, lt_one_iff, coeff_sub, cast_one, one_div]
suffices (⨆ n : ℕ, ite (n = 0) ‖r‖ 0) = ‖r‖ by
rw [← this]
apply congr_arg
ext n
by_cases hn : n = 0
·
rw [if_pos hn, if_pos hn, hn, cast_zero, sub_zero, coeff_X_zero, coeff_C_zero, zero_sub, norm_neg, inv_one,
rpow_one]
· rw [if_neg hn, if_neg hn]
· apply ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun n ↦ ?_) (fun _ hx ↦ ⟨0, by simp only [if_true, hx]⟩)
split_ifs
· exact le_refl _
· exact norm_nonneg _
