Theory infnorm

theory infnorm

imports 
  Main
  "Jordan_Normal_Form.Matrix"
  "LLL_Basis_Reduction.Norms"
begin

section ‹Maximum Norm›
text ‹The $\ell_\infty$ norm on vectors is exactly the maximum of the absolute value 
  of all entries.›

lemma linf_norm_vec_Max:
  "∥v∥⇩∞ = Max (insert 0 {¦v$i¦ | i. i< dim_vec v})"
proof (induct v)
  case (vCons a v)
  have "Missing_Lemmas.max_list (map abs (list_of_vec (vCons a v)) @ [0]) =
    Missing_Lemmas.max_list ((¦a¦) # (map abs (list_of_vec v) @ [0]))" by auto
  also have "… = max (¦a¦) (∥v∥⇩∞)" unfolding linf_norm_vec_def by (cases v, auto)
  also have "… = max (¦a¦) (Max (insert 0 {¦v$i¦ | i. i< dim_vec v}))" using vCons by auto
  also have "… = Max (insert (¦a¦) (insert 0 {¦v$i¦ | i. i< dim_vec v}))" by auto
  also have "… = Max (insert 0 (insert (¦a¦) {¦v$i¦ | i. i< dim_vec v}))"
    by (simp add: insert_commute)
  also have "insert (¦a¦){¦v$i¦ | i. i< dim_vec v} = 
    {¦(vCons a v)$i¦ | i. i< dim_vec (vCons a v)}"
  proof (safe, goal_cases)
    case (1 x)
    show ?case by (subst exI[of _ "0"], auto)
  next
    case (2 x i)
    then show ?case by (subst exI[of _ "Suc i"]) 
      (use vec_index_vCons_Suc[of a v i, symmetric] in ‹auto›)
  next
    case (3 x i)
    then show ?case by (subst vec_index_vCons) (subst exI[of _ "i-1"], auto)
  qed
  finally show ?case unfolding linf_norm_vec_def by auto
qed auto


end