Theory Norms

(*
    Authors:    Jose Divasón
                Maximilian Haslbeck
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

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" 
    "HOL-Library.Adhoc_Overloading"
    "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])"
adhoc_overloading linf_norm linf_norm_vec

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

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"
adhoc_overloading sq_norm sq_norm_conjugate

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"
adhoc_overloading sq_norm sq_norm_vec

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"

adhoc_overloading sq_norm sq_norm_poly

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"
  by (unfold diff_conv_add_uminus conjugate_dist_add conjugate_neg, rule)

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)
    by (metis conjugate_1 conjugate_dist_add one_add_one)
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