# Theory Algebraic_Number_Tests

```(*
Author:      René Thiemann
*)
section ‹Algebraic Number Tests›

text ‹We provide a sequence of examples which demonstrate what can be done with
the implementation of algebraic numbers.›

theory Algebraic_Number_Tests
imports
Jordan_Normal_Form.Char_Poly
Jordan_Normal_Form.Determinant_Impl
Show.Show_Complex
"HOL-Library.Code_Target_Nat"
"HOL-Library.Code_Target_Int"
Berlekamp_Zassenhaus.Factorize_Rat_Poly
Complex_Algebraic_Numbers
Show_Real_Precise
begin

subsection ‹Stand-Alone Examples›

abbreviation (input) "show_lines x ≡ shows_lines x Nil"

fun show_factorization :: "'a :: {semiring_1,show} × (('a poly × nat)list) ⇒ string" where
"show_factorization (c,[]) = show c"
| "show_factorization (c,((p,i) # ps)) = show_factorization (c,ps) @ '' * ('' @ show p @ '')'' @
(if i = 1 then [] else ''^'' @ show i)"

definition show_sf_factorization :: "'a :: {semiring_1,show} × (('a poly × nat)list) ⇒ string" where
"show_sf_factorization x = show_factorization (map_prod id (map (map_prod id Suc)) x)
"

text ‹Determine the roots over the rational, real, and complex numbers.›

definition "testpoly = [:5/2, -7/2, 1/2, -5, 7, -1, 5/2, -7/2, 1/2:]"
definition "test = show_lines (   real_roots_of_rat_poly testpoly)"

value [code] "show_lines (        roots_of_rat_poly testpoly)"
value [code] "show_lines (   real_roots_of_rat_poly testpoly)"
value [code] "show_lines (complex_roots_of_rat_poly testpoly)"

text ‹Compute real and complex roots of a polynomial with rational coefficients.›

value [code] "show (complex_roots_of_rat_poly testpoly)"
value [code] "show (real_roots_of_rat_poly testpoly)"

text ‹A sequence of calculations.›

value [code] "show (- sqrt 2 - sqrt 3)"
lemma "root 3 4 > sqrt (root 4 3) + ⌊1/10 * root 3 7⌋" by eval
lemma "csqrt (4 + 3 * 𝗂) ∉ ℝ" by eval
value [code] "show (csqrt (4 + 3 * 𝗂))"
value [code] "show (csqrt (1 + 𝗂))"

subsection ‹Example Application: Compute Norms of Eigenvalues›

text ‹For complexity analysis of some matrix \$A\$ it is important to compute the spectral
radius of a matrix, i.e., the maximal norm of all complex eigenvalues,
the growth rates of matrix-powers \$A^n\$, cf.~\<^cite>‹"JNF-AFP"› for a formalized statement
of this fact.›

definition eigenvalues :: "rat mat ⇒ complex list" where
"eigenvalues A = complex_roots_of_rat_poly (char_poly A)"

definition "testmat = mat_of_rows_list 3 [
[1,-4,2],
[1/5,7,9],
[7,1,5 :: rat]
]"

definition "spectral_radius_test = show (Max (set [ norm ev. ev ← eigenvalues testmat]))"
value [code] "char_poly testmat"