# Theory Norms

```(*
Authors:    Jose Divasón
Maximilian Haslbeck
Sebastiaan Joosten
René Thiemann
*)

section ‹Norms›

text ‹In this theory we provide the basic definitions and properties of several
norms of vectors and polynomials.
›

theory Norms
imports "HOL-Computational_Algebra.Polynomial"
"Jordan_Normal_Form.Conjugate"
"Algebraic_Numbers.Resultant" (* only for poly_of_vec *)
Missing_Lemmas
begin

subsection ‹L-‹∞› Norms›

consts linf_norm :: "'a ⇒ 'b" ("∥(_)∥⇩∞")

definition linf_norm_vec where "linf_norm_vec v ≡ max_list (map abs (list_of_vec v) @ [0])"

definition linf_norm_poly where "linf_norm_poly f ≡ max_list (map abs (coeffs f) @ [0])"

lemma linf_norm_vec: "∥vec n f∥⇩∞ = max_list (map (abs ∘ f) [0..<n] @ [0])"
by (simp add: linf_norm_vec_def)

lemma linf_norm_vec_vCons[simp]: "∥vCons a v∥⇩∞ = max ¦a¦ ∥v∥⇩∞"
by (auto simp: linf_norm_vec_def max_list_Cons)

lemma linf_norm_vec_0 [simp]: "∥vec 0 f∥⇩∞ = 0" by (simp add: linf_norm_vec_def)

lemma linf_norm_zero_vec [simp]: "∥0⇩v n :: 'a :: ordered_ab_group_add_abs vec∥⇩∞ = 0"
by (induct n, simp add: zero_vec_def, auto simp: zero_vec_Suc)

lemma linf_norm_vec_ge_0 [intro!]:
fixes v :: "'a :: ordered_ab_group_add_abs vec"
shows "∥v∥⇩∞ ≥ 0"
by (induct v, auto simp: max_def)

lemma linf_norm_vec_eq_0 [simp]:
fixes v :: "'a :: ordered_ab_group_add_abs vec"
assumes "v ∈ carrier_vec n"
shows "∥v∥⇩∞ = 0 ⟷ v = 0⇩v n"
by (insert assms, induct rule: carrier_vec_induct, auto simp: zero_vec_Suc max_def)

lemma linf_norm_vec_greater_0 [simp]:
fixes v :: "'a :: ordered_ab_group_add_abs vec"
assumes "v ∈ carrier_vec n"
shows "∥v∥⇩∞ > 0 ⟷ v ≠ 0⇩v n"
by (insert assms, induct rule: carrier_vec_induct, auto simp: zero_vec_Suc max_def)

lemma linf_norm_poly_0 [simp]: "∥0::_ poly∥⇩∞ = 0"
by (simp add: linf_norm_poly_def)

lemma linf_norm_pCons [simp]:
fixes p :: "'a :: ordered_ab_group_add_abs poly"
shows "∥pCons a p∥⇩∞ = max ¦a¦ ∥p∥⇩∞"
by (cases "p = 0", cases "a = 0", auto simp: linf_norm_poly_def max_list_Cons)

lemma linf_norm_poly_ge_0 [intro!]:
fixes f :: "'a :: ordered_ab_group_add_abs poly"
shows "∥f∥⇩∞ ≥ 0"
by (induct f, auto simp: max_def)

lemma linf_norm_poly_eq_0 [simp]:
fixes f :: "'a :: ordered_ab_group_add_abs poly"
shows "∥f∥⇩∞ = 0 ⟷ f = 0"
by (induct f, auto simp: max_def)

lemma linf_norm_poly_greater_0 [simp]:
fixes f :: "'a :: ordered_ab_group_add_abs poly"
shows "∥f∥⇩∞ > 0 ⟷ f ≠ 0"
by (induct f, auto simp: max_def)

subsection ‹Square Norms›

consts sq_norm :: "'a ⇒ 'b" ("∥(_)∥⇧2")

abbreviation "sq_norm_conjugate x ≡ x * conjugate x"

subsubsection ‹Square norms for vectors›

text ‹We prefer sum\_list over sum because it is not essentially dependent on commutativity,
and easier for proving.
›
definition "sq_norm_vec v ≡ ∑x ← list_of_vec v. ∥x∥⇧2"

lemma sq_norm_vec_vCons[simp]: "∥vCons a v∥⇧2 = ∥a∥⇧2 + ∥v∥⇧2"
by (simp add: sq_norm_vec_def)

lemma sq_norm_vec_0[simp]: "∥vec 0 f∥⇧2 = 0"
by (simp add: sq_norm_vec_def)

lemma sq_norm_vec_as_cscalar_prod:
fixes v :: "'a :: conjugatable_ring vec"
shows "∥v∥⇧2 = v ∙c v"
by (induct v, simp_all add: sq_norm_vec_def)

lemma sq_norm_zero_vec[simp]: "∥0⇩v n :: 'a :: conjugatable_ring vec∥⇧2 = 0"
by (simp add: sq_norm_vec_as_cscalar_prod)

lemmas sq_norm_vec_ge_0 [intro!] = conjugate_square_ge_0_vec[folded sq_norm_vec_as_cscalar_prod]

lemmas sq_norm_vec_eq_0 [simp] = conjugate_square_eq_0_vec[folded sq_norm_vec_as_cscalar_prod]

lemmas sq_norm_vec_greater_0 [simp] = conjugate_square_greater_0_vec[folded sq_norm_vec_as_cscalar_prod]

subsubsection ‹Square norm for polynomials›

definition sq_norm_poly where "sq_norm_poly p ≡ ∑a←coeffs p. ∥a∥⇧2"

lemma sq_norm_poly_0 [simp]: "∥0::_poly∥⇧2 = 0"
by (auto simp: sq_norm_poly_def)

lemma sq_norm_poly_pCons [simp]:
fixes a :: "'a :: conjugatable_ring"
shows "∥pCons a p∥⇧2 = ∥a∥⇧2 + ∥p∥⇧2"
by (cases "p = 0"; cases "a = 0", auto simp: sq_norm_poly_def)

lemma sq_norm_poly_ge_0 [intro!]:
fixes p :: "'a :: conjugatable_ordered_ring poly"
shows "∥p∥⇧2 ≥ 0"
by (unfold sq_norm_poly_def, rule sum_list_nonneg, auto intro!:conjugate_square_positive)

lemma sq_norm_poly_eq_0 [simp]:
fixes p :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors} poly"
shows "∥p∥⇧2 = 0 ⟷ p = 0"
proof (induct p)
case IH: (pCons a p)
show ?case
proof (cases "a = 0")
case True
with IH show ?thesis by simp
next
case False
then have "∥a∥⇧2 + ∥p∥⇧2 > 0" by (intro add_pos_nonneg, auto)
then show ?thesis by auto
qed
qed simp

lemma sq_norm_poly_pos [simp]:
fixes p :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors} poly"
shows "∥p∥⇧2 > 0 ⟷ p ≠ 0"
by (auto simp: less_le)

lemma sq_norm_vec_of_poly [simp]:
fixes p :: "'a :: conjugatable_ring poly"
shows "∥vec_of_poly p∥⇧2 = ∥p∥⇧2"
apply (unfold sq_norm_poly_def sq_norm_vec_def)
apply (fold sum_mset_sum_list)
apply auto.

lemma sq_norm_poly_of_vec [simp]:
fixes v :: "'a :: conjugatable_ring vec"
shows "∥poly_of_vec v∥⇧2 = ∥v∥⇧2"
apply (unfold sq_norm_poly_def sq_norm_vec_def coeffs_poly_of_vec)
apply (fold rev_map)
apply (fold sum_mset_sum_list)
apply (unfold mset_rev)
apply (unfold sum_mset_sum_list)
by (auto intro: sum_list_map_dropWhile0)

subsection ‹Relating Norms›

text ‹A class where ordering around 0 is linear.›
abbreviation (in ordered_semiring) is_real where "is_real a ≡ a < 0 ∨ a = 0 ∨ 0 < a"

class semiring_real_line = ordered_semiring_strict + ordered_semiring_0 +
assumes add_pos_neg_is_real: "a > 0 ⟹ b < 0 ⟹ is_real (a + b)"
and mult_neg_neg: "a < 0 ⟹ b < 0 ⟹ 0 < a * b"
and pos_pos_linear: "0 < a ⟹ 0 < b ⟹ a < b ∨ a = b ∨ b < a"
and neg_neg_linear: "a < 0 ⟹ b < 0 ⟹ a < b ∨ a = b ∨ b < a"
begin

lemma add_neg_pos_is_real: "a < 0 ⟹ b > 0 ⟹ is_real (a + b)"
using add_pos_neg_is_real[of b a] by (simp add: ac_simps)

lemma nonneg_linorder_cases [consumes 2, case_names less eq greater]:
assumes "0 ≤ a" and "0 ≤ b"
and "a < b ⟹ thesis" "a = b ⟹ thesis" "b < a ⟹ thesis"
shows thesis
using assms pos_pos_linear by (auto simp: le_less)

lemma nonpos_linorder_cases [consumes 2, case_names less eq greater]:
assumes "a ≤ 0" "b ≤ 0"
and "a < b ⟹ thesis" "a = b ⟹ thesis" "b < a ⟹ thesis"
shows thesis
using assms neg_neg_linear by (auto simp: le_less)

lemma real_linear:
assumes "is_real a" and "is_real b" shows "a < b ∨ a = b ∨ b < a"
using pos_pos_linear neg_neg_linear assms by (auto dest: less_trans[of _ 0])

lemma real_linorder_cases [consumes 2, case_names less eq greater]:
assumes real: "is_real a" "is_real b"
and cases: "a < b ⟹ thesis" "a = b ⟹ thesis" "b < a ⟹ thesis"
shows thesis
using real_linear[OF real] cases by auto

lemma
assumes a: "is_real a" and b: "is_real b"
shows real_add_le_cancel_left_pos: "c + a ≤ c + b ⟷ a ≤ b"
and real_add_less_cancel_left_pos: "c + a < c + b ⟷ a < b"
and real_add_le_cancel_right_pos: "a + c ≤ b + c ⟷ a ≤ b"
and real_add_less_cancel_right_pos: "a + c < b + c ⟷ a < b"
using add_strict_left_mono[of b a c] add_strict_left_mono[of a b c]
using add_strict_right_mono[of b a c] add_strict_right_mono[of a b c]
by (atomize(full), cases rule: real_linorder_cases[OF a b], auto)

lemma
assumes a: "is_real a" and b: "is_real b" and c: "0 < c"
shows real_mult_le_cancel_left_pos: "c * a ≤ c * b ⟷ a ≤ b"
and real_mult_less_cancel_left_pos: "c * a < c * b ⟷ a < b"
and real_mult_le_cancel_right_pos: "a * c ≤ b * c ⟷ a ≤ b"
and real_mult_less_cancel_right_pos: "a * c < b * c ⟷ a < b"
using mult_strict_left_mono[of b a c] mult_strict_left_mono[of a b c] c
using mult_strict_right_mono[of b a c] mult_strict_right_mono[of a b c] c
by (atomize(full), cases rule: real_linorder_cases[OF a b], auto)

lemma
assumes a: "is_real a" and b: "is_real b"
shows not_le_real: "¬ a ≥ b ⟷ a < b"
and not_less_real: "¬ a > b ⟷ a ≤ b"
by (atomize(full), cases rule: real_linorder_cases[OF a b], auto simp: less_imp_le)

lemma real_mult_eq_0_iff:
assumes a: "is_real a" and b: "is_real b"
shows "a * b = 0 ⟷ a = 0 ∨ b = 0"
proof-
{ assume l: "a * b = 0" and "a ≠ 0" and "b ≠ 0"
with a b have "a < 0 ∨ 0 < a" and "b < 0 ∨ 0 < b" by auto
then have "False" using mult_pos_pos[of a b] mult_pos_neg[of a b] mult_neg_pos[of a b] mult_neg_neg[of a b]
by (auto simp:l)
} then show ?thesis by auto
qed

end

lemma real_pos_mult_max:
fixes a b c :: "'a :: semiring_real_line"
assumes c: "c > 0" and a: "is_real a" and b: "is_real b"
shows "c * max a b = max (c * a) (c * b)"
by (rule hom_max, simp add: real_mult_le_cancel_left_pos[OF a b c])

class ring_abs_real_line = ordered_ring_abs + semiring_real_line

class semiring_1_real_line = semiring_real_line + monoid_mult + zero_less_one
begin

subclass ordered_semiring_1 by (unfold_locales, auto)

lemma power_both_mono: "1 ≤ a ⟹ m ≤ n ⟹ a ≤ b ⟹ a ^ m ≤ b ^ n"
using power_mono[of a b n] power_increasing[of m n a]
by (auto simp: order.trans[OF zero_le_one])

lemma power_pos:
assumes a0: "0 < a" shows "0 < a ^ n"
by (induct n, insert mult_strict_mono[OF a0] a0, auto)

lemma power_neg:
assumes a0: "a < 0" shows "odd n ⟹ a ^ n < 0" and "even n ⟹ a ^ n > 0"
by (atomize(full), induct n, insert a0, auto simp add: mult_pos_neg2 mult_neg_neg)

lemma power_ge_0_iff:
assumes a: "is_real a"
shows "0 ≤ a ^ n ⟷ 0 ≤ a ∨ even n"
using a proof (elim disjE)
assume "a < 0"
with power_neg[OF this, of n] show ?thesis by(cases "even n", auto)
next
assume "0 < a"
with power_pos[OF this] show ?thesis by auto
next
assume "a = 0"
then show ?thesis by (auto simp:power_0_left)
qed

lemma nonneg_power_less:
assumes "0 ≤ a" and "0 ≤ b" shows "a^n < b^n ⟷ n > 0 ∧ a < b"
proof (insert assms, induct n arbitrary: a b)
case 0
then show ?case by auto
next
case (Suc n)
note a = ‹0 ≤ a›
note b = ‹0 ≤ b›
show ?case
proof (cases "n > 0")
case True
from a b show ?thesis
proof (cases rule: nonneg_linorder_cases)
case less
then show ?thesis by (auto simp: Suc.hyps[OF a b] True intro!:mult_strict_mono' a b zero_le_power)
next
case eq
then show ?thesis by simp
next
case greater
with Suc.hyps[OF b a] True have "b ^ n < a ^ n" by auto
with mult_strict_mono'[OF greater this] b greater
show ?thesis by auto
qed
qed auto
qed

lemma power_strict_mono:
shows "a < b ⟹ 0 ≤ a ⟹ 0 < n ⟹ a ^ n < b ^ n"
by (subst nonneg_power_less, auto)

lemma nonneg_power_le:
assumes "0 ≤ a" and "0 ≤ b" shows "a^n ≤ b^n ⟷ n = 0 ∨ a ≤ b"
using assms proof (cases rule: nonneg_linorder_cases)
case less
with power_strict_mono[OF this, of n] assms show ?thesis by (cases n, auto)
next
case eq
then show ?thesis by auto
next
case greater
with power_strict_mono[OF this, of n] assms show ?thesis by (cases n, auto)
qed

end

subclass (in linordered_idom) semiring_1_real_line
apply unfold_locales
by (auto simp: mult_strict_left_mono mult_strict_right_mono mult_neg_neg)

class ring_1_abs_real_line = ring_abs_real_line + semiring_1_real_line
begin

subclass ring_1..

lemma abs_cases:
assumes "a = 0 ⟹ thesis" and "¦a¦ > 0 ⟹ thesis" shows thesis
using assms by auto

lemma abs_linorder_cases[case_names less eq greater]:
assumes "¦a¦ < ¦b¦ ⟹ thesis" and "¦a¦ = ¦b¦ ⟹ thesis" and "¦b¦ < ¦a¦ ⟹ thesis"
shows thesis
apply (cases rule: nonneg_linorder_cases[of "¦a¦" "¦b¦"])
using assms by auto

lemma [simp]:
shows not_le_abs_abs: "¬ ¦a¦ ≥ ¦b¦ ⟷ ¦a¦ < ¦b¦"
and not_less_abs_abs: "¬ ¦a¦ > ¦b¦ ⟷ ¦a¦ ≤ ¦b¦"
by (atomize(full), cases a b rule: abs_linorder_cases, auto simp: less_imp_le)

lemma abs_power_less [simp]: "¦a¦^n < ¦b¦^n ⟷ n > 0 ∧ ¦a¦ < ¦b¦"
by (subst nonneg_power_less, auto)

lemma abs_power_le [simp]: "¦a¦^n ≤ ¦b¦^n ⟷ n = 0 ∨ ¦a¦ ≤ ¦b¦"
by (subst nonneg_power_le, auto)

lemma abs_power_pos [simp]: "¦a¦^n > 0 ⟷ a ≠ 0 ∨ n = 0"
using power_pos[of "¦a¦"] by (cases "n", auto)

lemma abs_power_nonneg [intro!]: "¦a¦^n ≥ 0" by auto

lemma abs_power_eq_0 [simp]: "¦a¦^n = 0 ⟷ a = 0 ∧ n ≠ 0"
apply (induct n, force)
apply (unfold power_Suc)
apply (subst real_mult_eq_0_iff, auto).

end

instance nat :: semiring_1_real_line by (intro_classes, auto)
instance int :: ring_1_abs_real_line..

lemma vec_index_vec_of_list [simp]: "vec_of_list xs \$ i = xs ! i"
by transfer (auto simp: mk_vec_def undef_vec_def dest: empty_nth)

lemma vec_of_list_append: "vec_of_list (xs @ ys) = vec_of_list xs @⇩v vec_of_list ys"
by (auto simp: nth_append)

lemma linf_norm_vec_of_list:
"∥vec_of_list xs∥⇩∞ = max_list (map abs xs @ [0])"
by (simp add: linf_norm_vec_def)

lemma linf_norm_vec_as_Greatest:
fixes v :: "'a :: ring_1_abs_real_line vec"
shows "∥v∥⇩∞ = (GREATEST a. a ∈ abs ` set (list_of_vec v) ∪ {0})"
unfolding linf_norm_vec_of_list[of "list_of_vec v", simplified]
by (subst max_list_as_Greatest, auto)

lemma vec_of_poly_pCons:
assumes "f ≠ 0"
shows "vec_of_poly (pCons a f) = vec_of_poly f @⇩v vec_of_list [a]"
using assms
by (auto simp: vec_eq_iff Suc_diff_le)

lemma vec_of_poly_as_vec_of_list:
assumes "f ≠ 0"
shows "vec_of_poly f = vec_of_list (rev (coeffs f))"
proof (insert assms, induct f)
case 0
then show ?case by auto
next
case (pCons a f)
then show ?case
by (cases "f = 0", auto simp: vec_of_list_append vec_of_poly_pCons)
qed

lemma linf_norm_vec_of_poly [simp]:
fixes f :: "'a :: ring_1_abs_real_line poly"
shows "∥vec_of_poly f∥⇩∞ = ∥f∥⇩∞"
proof (cases "f = 0")
case False
then show ?thesis
apply (unfold vec_of_poly_as_vec_of_list linf_norm_vec_of_list linf_norm_poly_def)
apply (subst (1 2) max_list_as_Greatest, auto).
qed simp

lemma linf_norm_poly_as_Greatest:
fixes f :: "'a :: ring_1_abs_real_line poly"
shows "∥f∥⇩∞ = (GREATEST a. a ∈ abs ` set (coeffs f) ∪ {0})"
using linf_norm_vec_as_Greatest[of "vec_of_poly f"]
by simp

lemma vec_index_le_linf_norm:
fixes v :: "'a :: ring_1_abs_real_line vec"
assumes "i < dim_vec v"
shows "¦v\$i¦ ≤ ∥v∥⇩∞"
apply (unfold linf_norm_vec_def, rule le_max_list) using assms
apply (auto simp:  in_set_conv_nth intro!: imageI exI[of _ i]).

lemma coeff_le_linf_norm:
fixes f :: "'a :: ring_1_abs_real_line poly"
shows "¦coeff f i¦ ≤ ∥f∥⇩∞"
using vec_index_le_linf_norm[of "degree f - i" "vec_of_poly f"]
by (cases "i ≤ degree f", auto simp: coeff_eq_0)

class conjugatable_ring_1_abs_real_line = conjugatable_ring + ring_1_abs_real_line + power +
assumes sq_norm_as_sq_abs [simp]: "∥a∥⇧2 = ¦a¦⇧2"
begin
subclass conjugatable_ordered_ring by (unfold_locales, simp)
end

instance int :: conjugatable_ring_1_abs_real_line
by (intro_classes, simp add: numeral_2_eq_2)

instance rat :: conjugatable_ring_1_abs_real_line
by (intro_classes, simp add: numeral_2_eq_2)

instance real :: conjugatable_ring_1_abs_real_line
by (intro_classes, simp add: numeral_2_eq_2)

instance complex :: semiring_1_real_line
apply intro_classes
by (auto simp: complex_eq_iff mult_le_cancel_left mult_le_cancel_right mult_neg_neg less_complex_def less_eq_complex_def)

text ‹
Due to the assumption @{thm abs_ge_self} from Groups.thy,
@{type complex} cannot be @{class ring_1_abs_real_line}!
›
instance complex :: ordered_ab_group_add_abs oops

lemma sq_norm_as_sq_abs [simp]: "(sq_norm :: 'a :: conjugatable_ring_1_abs_real_line ⇒ 'a) = power2 ∘ abs"
by auto

lemma sq_norm_vec_le_linf_norm:
fixes v :: "'a :: {conjugatable_ring_1_abs_real_line} vec"
assumes "v ∈ carrier_vec n"
shows "∥v∥⇧2 ≤ of_nat n * ∥v∥⇩∞⇧2"
proof (insert assms, induct rule: carrier_vec_induct)
case (Suc n a v)
have [dest!]: "¬ ¦a¦ ≤ ∥v∥⇩∞ ⟹ of_nat n * ∥v∥⇩∞⇧2 ≤ of_nat n * ¦a¦⇧2"
by (rule real_linorder_cases[of "¦a¦" "∥v∥⇩∞"], insert Suc, auto simp: less_le intro!: power_mono mult_left_mono)
from Suc show ?case
by (auto simp: ring_distribs max_def intro!:add_mono power_mono)
qed simp

lemma sq_norm_poly_le_linf_norm:
fixes p :: "'a :: {conjugatable_ring_1_abs_real_line} poly"
shows "∥p∥⇧2 ≤ of_nat (degree p + 1) * ∥p∥⇩∞⇧2"
using sq_norm_vec_le_linf_norm[of "vec_of_poly p" "degree p + 1"]
by (auto simp: carrier_dim_vec)

lemma coeff_le_sq_norm:
fixes f :: "'a :: {conjugatable_ring_1_abs_real_line} poly"
shows "¦coeff f i¦⇧2 ≤ ∥f∥⇧2"
proof (induct f arbitrary: i)
case (pCons a f)
show ?case
proof (cases i)
case (Suc ii)
note pCons(2)[of ii]
also have "∥f∥⇧2 ≤ ¦a¦⇧2 + ∥f∥⇧2" by auto
finally show ?thesis unfolding Suc by auto
qed auto
qed simp

lemma max_norm_witness:
fixes f :: "'a :: ordered_ring_abs poly"
shows "∃ i. ∥f∥⇩∞ = ¦coeff f i¦"
by (induct f, auto simp add: max_def intro: exI[of _ "Suc _"] exI[of _ 0])

lemma max_norm_le_sq_norm:
fixes f ::  "'a :: conjugatable_ring_1_abs_real_line poly"
shows "∥f∥⇩∞⇧2 ≤ ∥f∥⇧2"
proof -
from max_norm_witness[of f] obtain i where id: "∥f∥⇩∞ = ¦coeff f i¦" by auto
show ?thesis unfolding id using coeff_le_sq_norm[of f i] by auto
qed

(*TODO MOVE*)
lemma (in conjugatable_ring) conjugate_minus: "conjugate (x - y) = conjugate x - conjugate y"

lemma conjugate_1[simp]: "(conjugate 1 :: 'a :: {conjugatable_ring, ring_1}) = 1"
proof-
have "conjugate 1 * 1 = (conjugate 1 :: 'a)" by simp
also have "conjugate … = 1" by simp
finally show ?thesis by (unfold conjugate_dist_mul, simp)
qed

lemma conjugate_of_int [simp]:
"(conjugate (of_int x) :: 'a :: {conjugatable_ring,ring_1}) = of_int x"
proof (induct x)
case (nonneg n)
then show ?case by (induct n, auto simp: conjugate_dist_add)
next
case (neg n)
then show ?case apply (induct n, auto simp: conjugate_minus conjugate_neg)
qed

lemma sq_norm_of_int: "∥map_vec of_int v :: 'a :: {conjugatable_ring,ring_1} vec∥⇧2 = of_int ∥v∥⇧2"
unfolding sq_norm_vec_as_cscalar_prod scalar_prod_def
unfolding hom_distribs
by (rule sum.cong, auto)

definition "norm1 p = sum_list (map abs (coeffs p))"

lemma norm1_ge_0: "norm1 (f :: 'a :: {abs,ordered_semiring_0,ordered_ab_group_add_abs}poly) ≥ 0"
unfolding norm1_def by (rule sum_list_nonneg, auto)

lemma norm2_norm1_main_equality: fixes f :: "nat ⇒ 'a :: linordered_idom"
shows "(∑i = 0..<n. ¦f i¦)⇧2 = (∑i = 0..<n. f i * f i)
+ (∑i = 0..<n. ∑j = 0..<n. if i = j then 0 else ¦f i¦ * ¦f j¦)"
proof (induct n)
case (Suc n)
have id: "{0 ..< Suc n} = insert n {0 ..< n}" by auto
have id: "sum f {0 ..< Suc n} = f n + sum f {0 ..< n}" for f :: "nat ⇒ 'a"
unfolding id by (rule sum.insert, auto)
show ?case unfolding id power2_sum unfolding Suc
by (auto simp: power2_eq_square sum_distrib_left sum.distrib ac_simps)
qed auto

lemma norm2_norm1_main_inequality: fixes f :: "nat ⇒ 'a :: linordered_idom"
shows "(∑i = 0..<n. f i * f i) ≤ (∑i = 0..<n. ¦f i¦)⇧2"
unfolding norm2_norm1_main_equality
by (auto intro!: sum_nonneg)

lemma norm2_le_norm1_int: "∥f :: int poly∥⇧2 ≤ (norm1 f)^2"
proof -
define F where "F = (!) (coeffs f)"
define n where "n = length (coeffs f)"
have 1: "∥f∥⇧2 = (∑i = 0..<n. F i * F i)"
unfolding norm1_def sq_norm_poly_def sum_list_sum_nth F_def n_def
by (subst sum.cong, auto simp: power2_eq_square)
have 2: "norm1 f = (∑i = 0..<n. ¦F i¦)"
unfolding norm1_def sq_norm_poly_def sum_list_sum_nth F_def n_def
by (subst sum.cong, auto)
show ?thesis unfolding 1 2 by (rule norm2_norm1_main_inequality)
qed

lemma sq_norm_smult_vec: "sq_norm ((c :: 'a :: {conjugatable_ring,comm_semiring_0}) ⋅⇩v v) = (c * conjugate c) * sq_norm v"
unfolding sq_norm_vec_as_cscalar_prod
by (subst scalar_prod_smult_left, force, unfold conjugate_smult_vec,
subst scalar_prod_smult_right, force, simp add: ac_simps)

lemma vec_le_sq_norm:
fixes v :: "'a :: conjugatable_ring_1_abs_real_line vec"
assumes "v ∈ carrier_vec n" "i < n"
shows "¦v \$ i¦⇧2 ≤ ∥v∥⇧2"
using assms proof (induction v arbitrary: i)
case (Suc n a v i)
note IH = Suc
show ?case
proof (cases i)
case (Suc ii)
then show ?thesis
using IH IH(2)[of ii] le_add_same_cancel2 order_trans by fastforce
qed auto
qed auto

class trivial_conjugatable =
conjugate +
assumes conjugate_id [simp]: "conjugate x = x"

class trivial_conjugatable_ordered_field =
conjugatable_ordered_field + trivial_conjugatable

class trivial_conjugatable_linordered_field =
trivial_conjugatable_ordered_field + linordered_field
begin
subclass conjugatable_ring_1_abs_real_line
by (standard) (auto simp add: semiring_normalization_rules)
end

instance rat :: trivial_conjugatable_linordered_field
by (standard, auto)

instance real :: trivial_conjugatable_linordered_field
by (standard, auto)

lemma scalar_prod_ge_0: "(x :: 'a :: linordered_idom vec) ∙ x ≥ 0"
unfolding scalar_prod_def
by (rule sum_nonneg, auto)

lemma cscalar_prod_is_scalar_prod[simp]: "(x :: 'a :: trivial_conjugatable_ordered_field vec) ∙c y = x ∙ y"
unfolding conjugate_id
by (rule arg_cong[of _ _ "scalar_prod x"], auto)

lemma scalar_prod_Cauchy:
fixes u v::"'a :: {trivial_conjugatable_linordered_field} Matrix.vec"
assumes "u ∈ carrier_vec n" "v ∈ carrier_vec n"
shows "(u ∙ v)⇧2 ≤ ∥u∥⇧2 * ∥v∥⇧2 "
proof -
{ assume v_0: "v ≠ 0⇩v n"
have "0 ≤ (u - r ⋅⇩v v) ∙ (u - r ⋅⇩v v)" for r
by (simp add: scalar_prod_ge_0)
also have "(u - r ⋅⇩v v) ∙ (u - r ⋅⇩v v) = u ∙ u - r * (u ∙ v) - r * (u ∙ v) + r * r * (v ∙ v)" for r::'a
proof -
have "(u - r ⋅⇩v v) ∙ (u - r ⋅⇩v v) = (u - r ⋅⇩v v) ∙ u - (u - r ⋅⇩v v) ∙ (r ⋅⇩v v)"
using assms by (subst scalar_prod_minus_distrib) auto
also have "… = u ∙ u - (r ⋅⇩v v) ∙ u - r * ((u - r ⋅⇩v v) ∙ v)"
using assms by (subst minus_scalar_prod_distrib) auto
also have "… = u ∙ u - r * (v ∙ u) - r * (u ∙ v - r * (v ∙ v))"
using assms by (subst minus_scalar_prod_distrib) auto
also have "… = u ∙ u - r * (u ∙ v) - r * (u ∙ v) + r * r * (v ∙ v)"
using assms comm_scalar_prod by (auto simp add: field_simps)
finally show ?thesis
by simp
qed
also have "u ∙ u - r * (u ∙ v) - r * (u ∙ v) + r * r * (v ∙ v) = sq_norm u - (u ∙ v)⇧2 / sq_norm v"
if "r = (u ∙ v) / (v ∙ v)" for r
unfolding that by (auto simp add: sq_norm_vec_as_cscalar_prod power2_eq_square)
finally have "0 ≤ ∥u∥⇧2 - (u ∙ v)⇧2 / ∥v∥⇧2"
by auto
then have "(u ∙ v)⇧2 / ∥v∥⇧2 ≤ ∥u∥⇧2"
by auto
then have "(u ∙ v)⇧2 ≤ ∥u∥⇧2 * ∥v∥⇧2"
using pos_divide_le_eq[of "∥v∥⇧2"] v_0 assms by (auto)
}
then show ?thesis
by (fastforce simp add: assms)
qed

end
```