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∥_\<infinity> = 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∥_\<infinity>)" 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