[STATEMENT]
lemma \<kappa>_def:
  assumes "i < length fs" "l \<le> i"
  shows "sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) =
         sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
let ?P = "\<lambda> i l \<kappa>. (i < length fs \<longrightarrow> l \<le> i \<longrightarrow>
                  sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) =
                  sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
from ex_\<kappa>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i < length fs; ?l \<le> ?i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i j \<cdot>\<^sub>v gso j) [0..<?l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<?l])
[PROOF STEP]
have "\<And> i. \<forall> l. \<exists>\<kappa>. ?P i l \<kappa>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < length fs; ?l \<le> ?i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i j \<cdot>\<^sub>v gso j) [0..<?l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<?l])

goal (1 subgoal):
 1. \<And>i. \<forall>l. \<exists>\<kappa>. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>l. \<exists>\<kappa>. ?i1 < length fs \<longrightarrow> l \<le> ?i1 \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x. ?i2 < length fs \<longrightarrow> x \<le> ?i2 \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> ?i2 j \<cdot>\<^sub>v gso j) [0..<x]) = M.sumlist (map (\<lambda>j. f x j \<cdot>\<^sub>v fs ! j) [0..<x])
[PROOF STEP]
have "\<forall>i. \<exists>\<kappa>. \<forall> l. ?P i l (\<kappa> l)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x. ?i2 < length fs \<longrightarrow> x \<le> ?i2 \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> ?i2 j \<cdot>\<^sub>v gso j) [0..<x]) = M.sumlist (map (\<lambda>j. f x j \<cdot>\<^sub>v fs ! j) [0..<x])

goal (1 subgoal):
 1. \<forall>i. \<exists>\<kappa>. \<forall>l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>\<kappa>. \<forall>l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x l. x < length fs \<longrightarrow> l \<le> x \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> x j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. f x l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
have "\<exists>\<kappa>. \<forall>i l. ?P i l (\<kappa> i l)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x l. x < length fs \<longrightarrow> l \<le> x \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> x j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. f x l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (1 subgoal):
 1. \<exists>\<kappa>. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<kappa>. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
from someI_ex[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. (SOME x. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. x i l j \<cdot>\<^sub>v fs ! j) [0..<l])) i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. (SOME x. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. x i l j \<cdot>\<^sub>v fs ! j) [0..<l])) i l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
unfolding \<kappa>_SOME_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. (SOME x. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. x i l j \<cdot>\<^sub>v fs ! j) [0..<l])) i l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. (SOME \<kappa>. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. (SOME x. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. x i l j \<cdot>\<^sub>v fs ! j) [0..<l])) i l j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
l \<le> i

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. (SOME \<kappa>. \<forall>i l. i < length fs \<longrightarrow> l \<le> i \<longrightarrow> M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) i l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_lin_indpt) fs_i_sumlist_\<kappa>:
  assumes "i < m" "l \<le> i" "j < l"
  shows "(fs ! i + sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
have "fs ! i + sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])
        = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l])
[PROOF STEP]
using assms gso_carrier assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l])
[PROOF STEP]
by (subst \<kappa>_def[symmetric]) (auto simp add: dim_sumlist sumlist_nth sum_negf)
[PROOF STATE]
proof (state)
this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l])

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l])

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
have "\<dots> = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
have "fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
by (intro fi_is_sum_of_mu_gso) auto
[PROOF STATE]
proof (state)
this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])

goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])

goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
have "\<dots> = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) +
                  M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
have *: "[0..<Suc i] = [0..<l] @ [l..<Suc i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc i] = [0..<l] @ [l..<Suc i]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. [0..<Suc i] = [0..<l] @ [l..<Suc i]
[PROOF STEP]
by (metis diff_zero le_imp_less_Suc length_upt list_trisect upt_conv_Cons)
[PROOF STATE]
proof (state)
this:
[0..<Suc i] = [0..<l] @ [l..<Suc i]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
by (subst *, subst map_append, subst sumlist_append) (use gso_carrier assms in auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
using assms gso_carrier assms
[PROOF STATE]
proof (prove)
using this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
i < length fs
l \<le> i
j < l
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
by (auto simp add: algebra_simps dim_sumlist)
[PROOF STATE]
proof (state)
this:
fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
have "fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) =
                M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])"
[PROOF STATE]
proof (prove)
using this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal (1 subgoal):
 1. fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
have "\<dots> \<bullet> (fs ! j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
using assms gso_carrier assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
unfolding lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
by (subst scalar_prod_left_sum_distrib)
       (auto simp add: algebra_simps dim_sumlist gso_scalar_zero intro!: sum_list_zero)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i])
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [l..<Suc i]) \<bullet> fs ! j = (0::'a)
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ints_sum:
  assumes "\<And>a. a \<in> A \<Longrightarrow> f a \<in> \<int>"
  shows "sum f A \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f A \<in> \<int>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> A \<Longrightarrow> f ?a \<in> \<int>

goal (1 subgoal):
 1. sum f A \<in> \<int>
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma Ints_prod:
  assumes "\<And>a. a \<in> A \<Longrightarrow> f a \<in> \<int>"
  shows "prod f A \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod f A \<in> \<int>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> A \<Longrightarrow> f ?a \<in> \<int>

goal (1 subgoal):
 1. prod f A \<in> \<int>
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma Ints_scalar_prod:
  "v \<in> carrier_vec n \<Longrightarrow> w \<in> carrier_vec n
   \<Longrightarrow> (\<And> i. i < n \<Longrightarrow> v $ i \<in> \<int>) \<Longrightarrow> (\<And> i. i < n \<Longrightarrow> w $ i \<in> \<int>) \<Longrightarrow> v \<bullet> w \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> carrier_vec n; w \<in> carrier_vec n; \<And>i. i < n \<Longrightarrow> v $ i \<in> \<int>; \<And>i. i < n \<Longrightarrow> w $ i \<in> \<int>\<rbrakk> \<Longrightarrow> v \<bullet> w \<in> \<int>
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> carrier_vec n; w \<in> carrier_vec n; \<And>i. i < n \<Longrightarrow> v $ i \<in> \<int>; \<And>i. i < n \<Longrightarrow> w $ i \<in> \<int>\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<dim_vec w. v $ i * w $ i) \<in> \<int>
[PROOF STEP]
by (intro Ints_sum Ints_mult, auto)


[STATEMENT]
lemma Ints_det: assumes "\<And> i j. i < dim_row A \<Longrightarrow> j < dim_col A
  \<Longrightarrow> A $$ (i,j) \<in> \<int>"
  shows "det A \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A \<in> \<int>
[PROOF STEP]
proof (cases "dim_row A = dim_col A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dim_row A = dim_col A \<Longrightarrow> det A \<in> \<int>
 2. dim_row A \<noteq> dim_col A \<Longrightarrow> det A \<in> \<int>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dim_row A = dim_col A

goal (2 subgoals):
 1. dim_row A = dim_col A \<Longrightarrow> det A \<in> \<int>
 2. dim_row A \<noteq> dim_col A \<Longrightarrow> det A \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A \<in> \<int>
[PROOF STEP]
unfolding Determinant.det_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if dim_row A = dim_col A then \<Sum>p | p permutes {0..<dim_row A}. of_int (sign p) * (\<Prod>i = 0..<dim_row A. A $$ (i, p i)) else (0::'a)) \<in> \<int>
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A
\<lbrakk>?i < dim_row A; ?j < dim_col A\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) \<in> \<int>

goal (1 subgoal):
 1. (if dim_row A = dim_col A then \<Sum>p | p permutes {0..<dim_row A}. of_int (sign p) * (\<Prod>i = 0..<dim_row A. A $$ (i, p i)) else (0::'a)) \<in> \<int>
[PROOF STEP]
by (auto intro!: Ints_mult Ints_prod)
[PROOF STATE]
proof (state)
this:
det A \<in> \<int>

goal (1 subgoal):
 1. dim_row A \<noteq> dim_col A \<Longrightarrow> det A \<in> \<int>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim_row A \<noteq> dim_col A \<Longrightarrow> det A \<in> \<int>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
dim_row A \<noteq> dim_col A

goal (1 subgoal):
 1. dim_row A \<noteq> dim_col A \<Longrightarrow> det A \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A \<in> \<int>
[PROOF STEP]
unfolding Determinant.det_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if dim_row A = dim_col A then \<Sum>p | p permutes {0..<dim_row A}. of_int (sign p) * (\<Prod>i = 0..<dim_row A. A $$ (i, p i)) else (0::'a)) \<in> \<int>
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
dim_row A \<noteq> dim_col A

goal (1 subgoal):
 1. (if dim_row A = dim_col A then \<Sum>p | p permutes {0..<dim_row A}. of_int (sign p) * (\<Prod>i = 0..<dim_row A. A $$ (i, p i)) else (0::'a)) \<in> \<int>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det A \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_Rn) Gramian_matrix_alt_alt_def:
  assumes "k \<le> m"
  shows "Gramian_matrix fs k = mat k k (\<lambda>(i,j). fs ! i \<bullet> fs ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_matrix fs k = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gramian_matrix fs k = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)
[PROOF STEP]
have *: "vec n (($) (fs ! i)) = fs ! i" if "i < m" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec n (($) (fs ! i)) = fs ! i
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. vec n (($) (fs ! i)) = fs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < length fs \<Longrightarrow> vec n (($) (fs ! ?i1)) = fs ! ?i1

goal (1 subgoal):
 1. Gramian_matrix fs k = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i1 < length fs \<Longrightarrow> vec n (($) (fs ! ?i1)) = fs ! ?i1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> vec n (($) (fs ! ?i1)) = fs ! ?i1

goal (1 subgoal):
 1. Gramian_matrix fs k = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)
[PROOF STEP]
unfolding Gramian_matrix_def
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> vec n (($) (fs ! ?i1)) = fs ! ?i1

goal (1 subgoal):
 1. (let M = mat k n (\<lambda>(i, y). fs ! i $ y) in M * M\<^sup>T) = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> vec n (($) (fs ! ?i1)) = fs ! ?i1
k \<le> length fs

goal (1 subgoal):
 1. (let M = mat k n (\<lambda>(i, y). fs ! i $ y) in M * M\<^sup>T) = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)
[PROOF STEP]
by (intro eq_matI) (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
Gramian_matrix fs k = mat k k (\<lambda>(i, j). fs ! i \<bullet> fs ! j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_int) fs_scalar_Ints:
  assumes "i < m" "j < m"
  shows "fs ! i \<bullet> fs ! j \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i \<bullet> fs ! j \<in> \<int>
[PROOF STEP]
by (rule Ints_scalar_prod[of _ n], insert fs_int assms, auto)


[STATEMENT]
lemma (in gram_schmidt_fs_lin_indpt) fs_i_fs_j_sum_\<kappa> :
  assumes "i < m" "l \<le> i" "j < l"
  shows "- (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have [simp]: "M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<in> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<in> carrier_vec n
[PROOF STEP]
by (auto intro!: sumlist_carrier simp add: dim_sumlist)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<in> carrier_vec n

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have "0  = (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) = (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j
[PROOF STEP]
using fs_i_sumlist_\<kappa> assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < length fs; ?l \<le> ?i; ?j < ?l\<rbrakk> \<Longrightarrow> (fs ! ?i + M.sumlist (map (\<lambda>j. \<kappa> ?i ?l j \<cdot>\<^sub>v fs ! j) [0..<?l])) \<bullet> fs ! ?j = (0::'a)
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. (0::'a) = (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) = (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) = (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have "\<dots> = fs ! i \<bullet> fs ! j + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = fs ! i \<bullet> fs ! j + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = fs ! i \<bullet> fs ! j + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j
[PROOF STEP]
by (subst add_scalar_prod_distrib[of _ n]) (auto)
[PROOF STATE]
proof (state)
this:
(fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = fs ! i \<bullet> fs ! j + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(fs ! i + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l])) \<bullet> fs ! j = fs ! i \<bullet> fs ! j + M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have "M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j =
             (\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j = (\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j = (\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j)
[PROOF STEP]
by (intro scalar_prod_left_sum_distrib) (auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j = (\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<bullet> fs ! j = (\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have "\<dots> = (\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j) = (\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)
[PROOF STEP]
by (rule arg_cong[where f=sum_list]) (auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j) = (\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<kappa> i l j \<cdot>\<^sub>v fs ! j) [0..<l]. v \<bullet> fs ! j) = (\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have "\<dots> =  (\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) = (\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)
[PROOF STEP]
by (subst interv_sum_list_conv_sum_set_nat) (auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) = (\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>t\<leftarrow>[0..<l]. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) = (\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
have "\<dots> = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. (\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
by (intro sum.cong) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>t = 0..<l. (\<kappa> i l t \<cdot>\<^sub>v fs ! t) \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) = fs ! i \<bullet> fs ! j + (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) = fs ! i \<bullet> fs ! j + (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
- (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_lin_indpt) Gramian_matrix_times_\<kappa> :
  assumes "i < m" "l \<le> i"
  shows "Gramian_matrix fs l *\<^sub>v (vec l (\<lambda>t. \<kappa> i l t)) = (vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l) = vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l) = vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j))
[PROOF STEP]
have "- (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)" if "j < l" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
using fs_i_fs_j_sum_\<kappa> assms that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < length fs; ?l \<le> ?i; ?j < ?l\<rbrakk> \<Longrightarrow> - (fs ! ?i \<bullet> fs ! ?j) = (\<Sum>t = 0..<?l. fs ! t \<bullet> fs ! ?j * \<kappa> ?i ?l t)
i < length fs
l \<le> i
j < l

goal (1 subgoal):
 1. - (fs ! i \<bullet> fs ! j) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! j * \<kappa> i l t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?j1 < l \<Longrightarrow> - (fs ! i \<bullet> fs ! ?j1) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! ?j1 * \<kappa> i l t)

goal (1 subgoal):
 1. Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l) = vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j1 < l \<Longrightarrow> - (fs ! i \<bullet> fs ! ?j1) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! ?j1 * \<kappa> i l t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?j1 < l \<Longrightarrow> - (fs ! i \<bullet> fs ! ?j1) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! ?j1 * \<kappa> i l t)

goal (1 subgoal):
 1. Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l) = vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?j1 < l \<Longrightarrow> - (fs ! i \<bullet> fs ! ?j1) = (\<Sum>t = 0..<l. fs ! t \<bullet> fs ! ?j1 * \<kappa> i l t)
i < length fs
l \<le> i

goal (1 subgoal):
 1. Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l) = vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j))
[PROOF STEP]
by (subst Gramian_matrix_alt_alt_def) (auto simp add: scalar_prod_def algebra_simps)
[PROOF STATE]
proof (state)
this:
Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l) = vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_int) d_\<kappa>_Ints :
  assumes "i < m" "l \<le> i" "t < l"
  shows "d l * \<kappa> i l t \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
let ?A = "Gramian_matrix fs l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
let ?B = "replace_col ?A (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
have deteq: "d l = det ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d l = det (Gramian_matrix fs l)
[PROOF STEP]
unfolding Gramian_determinant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gramian_matrix fs l) = det (Gramian_matrix fs l)
[PROOF STEP]
using Gramian_determinant_Ints
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<le> length fs; \<And>i j. \<lbrakk>i < n; j < length fs\<rbrakk> \<Longrightarrow> fs ! j $ i \<in> \<int>\<rbrakk> \<Longrightarrow> d ?k \<in> \<int>

goal (1 subgoal):
 1. det (Gramian_matrix fs l) = det (Gramian_matrix fs l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d l = det (Gramian_matrix fs l)

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
have **: "Gramian_matrix fs l \<in> carrier_mat l l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_matrix fs l \<in> carrier_mat l l
[PROOF STEP]
unfolding Gramian_matrix_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat l n (\<lambda>(i, y). fs ! i $ y) * (mat l n (\<lambda>(i, y). fs ! i $ y))\<^sup>T \<in> carrier_mat l l
[PROOF STEP]
using fs_carrier
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mat l n (\<lambda>(i, y). fs ! i $ y) * (mat l n (\<lambda>(i, y). fs ! i $ y))\<^sup>T \<in> carrier_mat l l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gramian_matrix fs l \<in> carrier_mat l l

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Gramian_matrix fs l \<in> carrier_mat l l
[PROOF STEP]
have " \<kappa> i l t * det ?A = det ?B"
[PROOF STATE]
proof (prove)
using this:
Gramian_matrix fs l \<in> carrier_mat l l

goal (1 subgoal):
 1. \<kappa> i l t * det (Gramian_matrix fs l) = det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t)
[PROOF STEP]
using assms fs_carrier cramer_lemma_mat[of ?A l " (vec l (\<lambda>t. \<kappa> i l t))" t]
[PROOF STATE]
proof (prove)
using this:
Gramian_matrix fs l \<in> carrier_mat l l
i < length fs
l \<le> i
t < l
set fs \<subseteq> carrier_vec n
\<lbrakk>Gramian_matrix fs l \<in> carrier_mat l l; vec l (\<kappa> i l) \<in> carrier_vec l; t < l\<rbrakk> \<Longrightarrow> det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) = vec l (\<kappa> i l) $ t * det (Gramian_matrix fs l)

goal (1 subgoal):
 1. \<kappa> i l t * det (Gramian_matrix fs l) = det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<kappa> i l t * det (Gramian_matrix fs l) = det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t)

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<kappa> i l t * det (Gramian_matrix fs l) = det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t)

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
have " ... \<in> \<int> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
have *: "t<l \<Longrightarrow> (?A *\<^sub>v vec l (\<kappa> i l)) $ t \<in> \<int>" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ t \<in> \<int>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i
t < l

goal (1 subgoal):
 1. t < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ t \<in> \<int>
[PROOF STEP]
apply(subst Gramian_matrix_times_\<kappa>, force, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t < l; i < length fs; l \<le> i; t < l\<rbrakk> \<Longrightarrow> vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j)) $ t \<in> \<int>
[PROOF STEP]
using fs_int fs_carrier
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < n; ?j < length fs\<rbrakk> \<Longrightarrow> fs ! ?j $ ?i \<in> \<int>
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<lbrakk>t < l; i < length fs; l \<le> i; t < l\<rbrakk> \<Longrightarrow> vec l (\<lambda>j. - (fs ! i \<bullet> fs ! j)) $ t \<in> \<int>
[PROOF STEP]
by (auto intro!: fs_scalar_Ints Ints_minus)
[PROOF STATE]
proof (state)
this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
define B where "B = ?B"
[PROOF STATE]
proof (state)
this:
B = replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
have Bint: "t1<l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1,s1) \<in> \<int>" for t1 s1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
proof (cases "s1 = t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s1 = t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
 2. s1 \<noteq> t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s1 = t

goal (2 subgoals):
 1. s1 = t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
 2. s1 \<noteq> t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
from * ** this
[PROOF STATE]
proof (chain)
picking this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>
Gramian_matrix fs l \<in> carrier_mat l l
s1 = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>
Gramian_matrix fs l \<in> carrier_mat l l
s1 = t

goal (1 subgoal):
 1. t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
unfolding replace_col_def B_def
[PROOF STATE]
proof (prove)
using this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>
Gramian_matrix fs l \<in> carrier_mat l l
s1 = t

goal (1 subgoal):
 1. t1 < l \<longrightarrow> s1 < l \<longrightarrow> mat (dim_row (Gramian_matrix fs l)) (dim_col (Gramian_matrix fs l)) (\<lambda>(ia, j). if j = t then (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ia else Gramian_matrix fs l $$ (ia, j)) $$ (t1, s1) \<in> \<int>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>

goal (1 subgoal):
 1. s1 \<noteq> t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1 \<noteq> t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s1 \<noteq> t

goal (1 subgoal):
 1. s1 \<noteq> t \<Longrightarrow> t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
from * ** Gramian_matrix_def this fs_carrier assms
[PROOF STATE]
proof (chain)
picking this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>
Gramian_matrix fs l \<in> carrier_mat l l
Gramian_matrix ?G ?k = (let M = mat ?k n (\<lambda>(i, j). ?G ! i $ j) in M * M\<^sup>T)
s1 \<noteq> t
set fs \<subseteq> carrier_vec n
i < length fs
l \<le> i
t < l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>
Gramian_matrix fs l \<in> carrier_mat l l
Gramian_matrix ?G ?k = (let M = mat ?k n (\<lambda>(i, j). ?G ! i $ j) in M * M\<^sup>T)
s1 \<noteq> t
set fs \<subseteq> carrier_vec n
i < length fs
l \<le> i
t < l

goal (1 subgoal):
 1. t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>
[PROOF STEP]
unfolding replace_col_def B_def
[PROOF STATE]
proof (prove)
using this:
?t1 < l \<Longrightarrow> (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ?t1 \<in> \<int>
Gramian_matrix fs l \<in> carrier_mat l l
Gramian_matrix ?G ?k = (let M = mat ?k n (\<lambda>(i, j). ?G ! i $ j) in M * M\<^sup>T)
s1 \<noteq> t
set fs \<subseteq> carrier_vec n
i < length fs
l \<le> i
t < l

goal (1 subgoal):
 1. t1 < l \<longrightarrow> s1 < l \<longrightarrow> mat (dim_row (Gramian_matrix fs l)) (dim_col (Gramian_matrix fs l)) (\<lambda>(ia, j). if j = t then (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) $ ia else Gramian_matrix fs l $$ (ia, j)) $$ (t1, s1) \<in> \<int>
[PROOF STEP]
by (auto simp: Gramian_matrix_def Let_def scalar_prod_def intro!: Ints_sum Ints_mult fs_int)
[PROOF STATE]
proof (state)
this:
t1 < l \<longrightarrow> s1 < l \<longrightarrow> B $$ (t1, s1) \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?t1.1 < l \<longrightarrow> ?s1.1 < l \<longrightarrow> B $$ (?t1.1, ?s1.1) \<in> \<int>

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
have B: "B \<in> carrier_mat l l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> carrier_mat l l
[PROOF STEP]
using ** replace_col_def
[PROOF STATE]
proof (prove)
using this:
Gramian_matrix fs l \<in> carrier_mat l l
replace_col ?A ?b ?k = mat (dim_row ?A) (dim_col ?A) (\<lambda>(i, j). if j = ?k then ?b $ i else ?A $$ (i, j))

goal (1 subgoal):
 1. B \<in> carrier_mat l l
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
Gramian_matrix fs l \<in> carrier_mat l l
replace_col ?A ?b ?k = mat (dim_row ?A) (dim_col ?A) (\<lambda>(i, j). if j = ?k then ?b $ i else ?A $$ (i, j))

goal (1 subgoal):
 1. replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t \<in> carrier_mat l l
[PROOF STEP]
by (auto simp: replace_col_def)
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat l l

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
have "det B \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det B \<in> \<int>
[PROOF STEP]
using B Bint assms  det_col[of B l]
[PROOF STATE]
proof (prove)
using this:
B \<in> carrier_mat l l
?t1.1 < l \<longrightarrow> ?s1.1 < l \<longrightarrow> B $$ (?t1.1, ?s1.1) \<in> \<int>
i < length fs
l \<le> i
t < l
B \<in> carrier_mat l l \<Longrightarrow> det B = (\<Sum>p | p permutes {0..<l}. of_int (sign p) * (\<Prod>j<l. B $$ (p j, j)))

goal (1 subgoal):
 1. det B \<in> \<int>
[PROOF STEP]
by (auto intro!: Ints_sum Ints_mult Ints_prod)
[PROOF STATE]
proof (state)
this:
det B \<in> \<int>

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
det B \<in> \<int>

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>

goal (1 subgoal):
 1. det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (replace_col (Gramian_matrix fs l) (Gramian_matrix fs l *\<^sub>v vec l (\<kappa> i l)) t) \<in> \<int>

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<kappa> i l t * det (Gramian_matrix fs l) \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<kappa> i l t * det (Gramian_matrix fs l) \<in> \<int>

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
using deteq
[PROOF STATE]
proof (prove)
using this:
\<kappa> i l t * det (Gramian_matrix fs l) \<in> \<int>
d l = det (Gramian_matrix fs l)

goal (1 subgoal):
 1. d l * \<kappa> i l t \<in> \<int>
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
d l * \<kappa> i l t \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_int) d_gso_Ints:
  assumes "i < n" "k < m"
  shows "(d k \<cdot>\<^sub>v (gso k)) $ i \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
note d_\<kappa>_Ints[intro!]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < length fs; ?l \<le> ?i; ?t < ?l\<rbrakk> \<Longrightarrow> d ?l * \<kappa> ?i ?l ?t \<in> \<int>

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i < length fs; ?l \<le> ?i; ?t < ?l\<rbrakk> \<Longrightarrow> d ?l * \<kappa> ?i ?l ?t \<in> \<int>
[PROOF STEP]
have "(d k * \<kappa> k k j) * fs ! j $ i \<in> \<int>" if "j < k" for j
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < length fs; ?l \<le> ?i; ?t < ?l\<rbrakk> \<Longrightarrow> d ?l * \<kappa> ?i ?l ?t \<in> \<int>

goal (1 subgoal):
 1. d k * \<kappa> k k j * fs ! j $ i \<in> \<int>
[PROOF STEP]
using that fs_int assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < length fs; ?l \<le> ?i; ?t < ?l\<rbrakk> \<Longrightarrow> d ?l * \<kappa> ?i ?l ?t \<in> \<int>
j < k
\<lbrakk>?i < n; ?j < length fs\<rbrakk> \<Longrightarrow> fs ! ?j $ ?i \<in> \<int>
i < n
k < length fs

goal (1 subgoal):
 1. d k * \<kappa> k k j * fs ! j $ i \<in> \<int>
[PROOF STEP]
by (auto intro: Ints_mult )
[PROOF STATE]
proof (state)
this:
?j1 < k \<Longrightarrow> d k * \<kappa> k k ?j1 * fs ! ?j1 $ i \<in> \<int>

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?j1 < k \<Longrightarrow> d k * \<kappa> k k ?j1 * fs ! ?j1 $ i \<in> \<int>

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
have "(d k * \<kappa> k k j) * fs ! j $ i = d k * \<kappa> k k j * fs ! j $ i" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d k * \<kappa> k k j * fs ! j $ i = d k * \<kappa> k k j * fs ! j $ i
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
d k * \<kappa> k k ?j1 * fs ! ?j1 $ i = d k * \<kappa> k k ?j1 * fs ! ?j1 $ i

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?j1 < k \<Longrightarrow> d k * \<kappa> k k ?j1 * fs ! ?j1 $ i \<in> \<int>
d k * \<kappa> k k ?j1 * fs ! ?j1 $ i = d k * \<kappa> k k ?j1 * fs ! ?j1 $ i
[PROOF STEP]
have "d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>"
[PROOF STATE]
proof (prove)
using this:
?j1 < k \<Longrightarrow> d k * \<kappa> k k ?j1 * fs ! ?j1 $ i \<in> \<int>
d k * \<kappa> k k ?j1 * fs ! ?j1 $ i = d k * \<kappa> k k ?j1 * fs ! ?j1 $ i

goal (1 subgoal):
 1. d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>
[PROOF STEP]
by (subst sum_distrib_left) (auto simp add: field_simps intro!: Ints_sum)
[PROOF STATE]
proof (state)
this:
d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
have "(gso k) $ i = fs ! k $ i + sum (\<lambda>j. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i) {0..<k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
[PROOF STEP]
have " i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < n
k < length fs

goal (1 subgoal):
 1. i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))
[PROOF STEP]
by (subst sumlist_dim) auto
[PROOF STATE]
proof (state)
this:
i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))

goal (1 subgoal):
 1. gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))

goal (1 subgoal):
 1. gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (M.sumlist (map (\<lambda>j. \<kappa> k k j \<cdot>\<^sub>v fs ! j) [0..<k]))
i < n
k < length fs

goal (1 subgoal):
 1. gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
[PROOF STEP]
by (subst gso.simps) (auto simp add: sumlist_nth sumlist_dim \<kappa>_def)
[PROOF STATE]
proof (state)
this:
gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>
gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>
gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d k * (\<Sum>j = 0..<k. \<kappa> k k j * fs ! j $ i) \<in> \<int>
gso k $ i = fs ! k $ i + (\<Sum>j = 0..<k. (\<kappa> k k j \<cdot>\<^sub>v fs ! j) $ i)
i < n
k < length fs

goal (1 subgoal):
 1. (d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>
[PROOF STEP]
by (auto simp add: distrib_left Gramian_determinant_Ints fs_int intro!: Ints_mult Ints_add)
[PROOF STATE]
proof (state)
this:
(d k \<cdot>\<^sub>v gso k) $ i \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_int) d_mu_Ints:
  assumes "l \<le> k" "k < m"
  shows "d (Suc l) * \<mu> k l \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
proof (cases "l < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l < k

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
have ll: "d l * gso l $ i = (d l \<cdot>\<^sub>v gso l) $ i" if "i < n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d l * gso l $ i = (d l \<cdot>\<^sub>v gso l) $ i
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
i < n
l \<le> k
k < length fs

goal (1 subgoal):
 1. d l * gso l $ i = (d l \<cdot>\<^sub>v gso l) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < n \<Longrightarrow> d l * gso l $ ?i1 = (d l \<cdot>\<^sub>v gso l) $ ?i1

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
have "d (Suc l) * \<mu> k l =d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (Suc l) * \<mu> k l = d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
using assms True
[PROOF STATE]
proof (prove)
using this:
l \<le> k
k < length fs
l < k

goal (1 subgoal):
 1. d (Suc l) * \<mu> k l = d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
unfolding \<mu>.simps
[PROOF STATE]
proof (prove)
using this:
l \<le> k
k < length fs
l < k

goal (1 subgoal):
 1. d (Suc l) * (if l < k then fs ! k \<bullet> gso l / \<parallel>gso l\<parallel>\<^sup>2 else if k = l then 1::'a else (0::'a)) = d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d (Suc l) * \<mu> k l = d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (Suc l) * \<mu> k l = d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
have "\<dots> = fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2 = fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l)
[PROOF STEP]
using assms Gramian_determinant(2)[of "Suc l"]
[PROOF STATE]
proof (prove)
using this:
l \<le> k
k < length fs
Suc l \<le> length fs \<Longrightarrow> (0::'a) < d (Suc l)

goal (1 subgoal):
 1. d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2 = fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l)
[PROOF STEP]
by (subst Gramian_determinant_div[symmetric]) (auto)
[PROOF STATE]
proof (state)
this:
d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2 = fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l)

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (Suc l) * (fs ! k \<bullet> gso l) / \<parallel>gso l\<parallel>\<^sup>2 = fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l)

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
have "\<dots> \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>
[PROOF STEP]
have "d l * gso l $ i \<in> \<int>" if "i < n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d l * gso l $ i \<in> \<int>
[PROOF STEP]
using assms d_gso_Ints that ll
[PROOF STATE]
proof (prove)
using this:
l \<le> k
k < length fs
\<lbrakk>?i < n; ?k < length fs\<rbrakk> \<Longrightarrow> (d ?k \<cdot>\<^sub>v gso ?k) $ ?i \<in> \<int>
i < n
?i1 < n \<Longrightarrow> d l * gso l $ ?i1 = (d l \<cdot>\<^sub>v gso l) $ ?i1

goal (1 subgoal):
 1. d l * gso l $ i \<in> \<int>
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
?i1 < n \<Longrightarrow> d l * gso l $ ?i1 \<in> \<int>

goal (1 subgoal):
 1. fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i1 < n \<Longrightarrow> d l * gso l $ ?i1 \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i1 < n \<Longrightarrow> d l * gso l $ ?i1 \<in> \<int>

goal (1 subgoal):
 1. fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i1 < n \<Longrightarrow> d l * gso l $ ?i1 \<in> \<int>
l \<le> k
k < length fs

goal (1 subgoal):
 1. fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>
[PROOF STEP]
by (auto intro!: Ints_sum simp add: fs_int scalar_prod_def)
[PROOF STATE]
proof (state)
this:
fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fs ! k \<bullet> (d l \<cdot>\<^sub>v gso l) \<in> \<int>

goal (2 subgoals):
 1. l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
 2. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d (Suc l) * \<mu> k l \<in> \<int>

goal (1 subgoal):
 1. d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d (Suc l) * \<mu> k l \<in> \<int>

goal (1 subgoal):
 1. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> l < k

goal (1 subgoal):
 1. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
l \<le> k
k < length fs
\<not> l < k
[PROOF STEP]
have l: "l = k"
[PROOF STATE]
proof (prove)
using this:
l \<le> k
k < length fs
\<not> l < k

goal (1 subgoal):
 1. l = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = k

goal (1 subgoal):
 1. \<not> l < k \<Longrightarrow> d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (Suc l) * \<mu> k l \<in> \<int>
[PROOF STEP]
unfolding l \<mu>.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (Suc k) * (if k < k then fs ! k \<bullet> gso k / \<parallel>gso k\<parallel>\<^sup>2 else if k = k then 1::'a else (0::'a)) \<in> \<int>
[PROOF STEP]
using Gramian_determinant_Ints fs_int assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<le> length fs; \<And>i j. \<lbrakk>i < n; j < length fs\<rbrakk> \<Longrightarrow> fs ! j $ i \<in> \<int>\<rbrakk> \<Longrightarrow> d ?k \<in> \<int>
\<lbrakk>?i < n; ?j < length fs\<rbrakk> \<Longrightarrow> fs ! ?j $ ?i \<in> \<int>
l \<le> k
k < length fs

goal (1 subgoal):
 1. d (Suc k) * (if k < k then fs ! k \<bullet> gso k / \<parallel>gso k\<parallel>\<^sup>2 else if k = k then 1::'a else (0::'a)) \<in> \<int>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d (Suc l) * \<mu> k l \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_list_Max: "ls \<noteq> [] \<Longrightarrow> max_list ls = Max (set ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list ls = Max (set ls)
[PROOF STEP]
by (induction ls) (auto simp add: max_list_Cons)


[STATEMENT]
lemma N_ge_0:
  assumes "0 < m"
  shows "0 \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) \<le> N
[PROOF STEP]
have "x \<in> sq_norm ` set fs \<Longrightarrow> 0 \<le> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> sq_norm ` set fs \<Longrightarrow> (0::'a) \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> sq_norm ` set fs \<Longrightarrow> (0::'a) \<le> ?x1

goal (1 subgoal):
 1. (0::'a) \<le> N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x1 \<in> sq_norm ` set fs \<Longrightarrow> (0::'a) \<le> ?x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> sq_norm ` set fs \<Longrightarrow> (0::'a) \<le> ?x1

goal (1 subgoal):
 1. (0::'a) \<le> N
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> sq_norm ` set fs \<Longrightarrow> (0::'a) \<le> ?x1
0 < length fs

goal (1 subgoal):
 1. (0::'a) \<le> N
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> sq_norm ` set fs \<Longrightarrow> (0::'a) \<le> ?x1
0 < length fs

goal (1 subgoal):
 1. (0::'a) \<le> Max (sq_norm ` set fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_fs:
  assumes "i < m"
  shows "\<parallel>fs ! i\<parallel>\<^sup>2 \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. \<parallel>fs ! i\<parallel>\<^sup>2 \<le> Max (sq_norm ` set fs)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma N_gso:
  assumes "i < m"
  shows "\<parallel>gso i\<parallel>\<^sup>2 \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> N
[PROOF STEP]
using assms N_fs sq_norm_gso_le_f
[PROOF STATE]
proof (prove)
using this:
i < length fs
?i < length fs \<Longrightarrow> \<parallel>fs ! ?i\<parallel>\<^sup>2 \<le> N
?i < length fs \<Longrightarrow> \<parallel>gso ?i\<parallel>\<^sup>2 \<le> \<parallel>fs ! ?i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> N
[PROOF STEP]
by fastforce


[STATEMENT]
lemma N_d:
  assumes "i \<le> m"
  shows "Gramian_determinant fs i \<le> N ^ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d i \<le> N ^ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d i \<le> N ^ i
[PROOF STEP]
have "(\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)
[PROOF STEP]
using assms N_gso
[PROOF STATE]
proof (prove)
using this:
i \<le> length fs
?i < length fs \<Longrightarrow> \<parallel>gso ?i\<parallel>\<^sup>2 \<le> N

goal (1 subgoal):
 1. (\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)
[PROOF STEP]
by (intro prod_mono) auto
[PROOF STATE]
proof (state)
this:
(\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)

goal (1 subgoal):
 1. d i \<le> N ^ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)

goal (1 subgoal):
 1. d i \<le> N ^ i
[PROOF STEP]
using assms Gramian_determinant
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j<i. \<parallel>gso j\<parallel>\<^sup>2) \<le> (\<Prod>j<i. N)
i \<le> length fs
?k \<le> length fs \<Longrightarrow> d ?k = (\<Prod>j<?k. \<parallel>gso j\<parallel>\<^sup>2)
?k \<le> length fs \<Longrightarrow> (0::'a) < d ?k

goal (1 subgoal):
 1. d i \<le> N ^ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d i \<le> N ^ i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_MAXIMUM: assumes "finite A" "A \<noteq> {}"
  shows "\<exists>a \<in> A. Max (f ` A) = f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>A. Max (f ` A) = f a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a\<in>A. Max (f ` A) = f a
[PROOF STEP]
have "Max (f ` A) \<in> f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (f ` A) \<in> f ` A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}

goal (1 subgoal):
 1. Max (f ` A) \<in> f ` A
[PROOF STEP]
by (auto intro!: Max_in)
[PROOF STATE]
proof (state)
this:
Max (f ` A) \<in> f ` A

goal (1 subgoal):
 1. \<exists>a\<in>A. Max (f ` A) = f a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max (f ` A) \<in> f ` A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Max (f ` A) \<in> f ` A

goal (1 subgoal):
 1. \<exists>a\<in>A. Max (f ` A) = f a
[PROOF STEP]
using assms imageE
[PROOF STATE]
proof (prove)
using this:
Max (f ` A) \<in> f ` A
finite A
A \<noteq> {}
\<lbrakk>?b \<in> ?f ` ?A; \<And>x. \<lbrakk>?b = ?f x; x \<in> ?A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>a\<in>A. Max (f ` A) = f a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>A. Max (f ` A) = f a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fs_int': "k < n \<Longrightarrow> f \<in> set fs \<Longrightarrow> f $ k \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < n; f \<in> set fs\<rbrakk> \<Longrightarrow> f $ k \<in> \<int>
[PROOF STEP]
by (metis fs_int in_set_conv_nth)


[STATEMENT]
lemma N_mu:
  assumes "i < m" "j \<le> i"
  shows "(\<mu> i j)\<^sup>2 \<le> N ^ (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
assume ji: "j < i"
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "(\<mu> i j)\<^sup>2 \<le> Gramian_determinant fs j * \<parallel>fs ! i\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> d j * \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
using assms ji
[PROOF STATE]
proof (prove)
using this:
i < length fs
j \<le> i
j < i

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> d j * \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
by (intro mu_bound_Gramian_determinant) auto
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 \<le> d j * \<parallel>fs ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 \<le> d j * \<parallel>fs ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "\<dots> \<le> N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
using assms N_d N_ge_0
[PROOF STATE]
proof (prove)
using this:
i < length fs
j \<le> i
?i \<le> length fs \<Longrightarrow> d ?i \<le> N ^ ?i
0 < length fs \<Longrightarrow> (0::'a) \<le> N

goal (1 subgoal):
 1. d j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
by (intro mult_mono) fastforce+
[PROOF STATE]
proof (state)
this:
d j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * N
[PROOF STEP]
using assms N_fs N_ge_0
[PROOF STATE]
proof (prove)
using this:
i < length fs
j \<le> i
?i < length fs \<Longrightarrow> \<parallel>fs ! ?i\<parallel>\<^sup>2 \<le> N
0 < length fs \<Longrightarrow> (0::'a) \<le> N

goal (1 subgoal):
 1. N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * N
[PROOF STEP]
by (intro mult_mono) fastforce+
[PROOF STATE]
proof (state)
this:
N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * N

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N ^ j * \<parallel>fs ! i\<parallel>\<^sup>2 \<le> N ^ j * N

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "\<dots> = N ^ (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N ^ j * N = N ^ Suc j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N ^ j * N = N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
assume ji: "j = i"
[PROOF STATE]
proof (state)
this:
j = i

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "(\<mu> i j)\<^sup>2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 = (1::'a)
[PROOF STEP]
using ji
[PROOF STATE]
proof (prove)
using this:
j = i

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 = (1::'a)
[PROOF STEP]
by (simp add: \<mu>.simps)
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 = (1::'a)

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 = (1::'a)

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "\<dots> \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> N
[PROOF STEP]
using assms N_1
[PROOF STATE]
proof (prove)
using this:
i < length fs
j \<le> i
set fs \<noteq> {} \<Longrightarrow> (1::'a) \<le> N

goal (1 subgoal):
 1. (1::'a) \<le> N
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> N

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> N

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have "\<dots> \<le> N ^ (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N \<le> N ^ Suc j
[PROOF STEP]
using assms N_1
[PROOF STATE]
proof (prove)
using this:
i < length fs
j \<le> i
set fs \<noteq> {} \<Longrightarrow> (1::'a) \<le> N

goal (1 subgoal):
 1. N \<le> N ^ Suc j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
N \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
j = i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j < i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
j = i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j < i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
j = i \<Longrightarrow> (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
i < length fs
j \<le> i

goal (1 subgoal):
 1. (\<mu> i j)\<^sup>2 \<le> N ^ Suc j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<mu> i j)\<^sup>2 \<le> N ^ Suc j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_hom_Ints:
  assumes "i < n" "xs \<in> carrier_vec n"
  shows "of_int_hom.vec_hom xs $ i \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom xs $ i \<in> \<int>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < n
xs \<in> carrier_vec n

goal (1 subgoal):
 1. of_int_hom.vec_hom xs $ i \<in> \<int>
[PROOF STEP]
by auto


[STATEMENT]
lemma division_to_div: "(of_int x  :: 'a :: floor_ceiling) = of_int y / of_int z \<Longrightarrow> x = y div z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int x = of_int y / of_int z \<Longrightarrow> x = y div z
[PROOF STEP]
by (metis floor_divide_of_int_eq floor_of_int)


[STATEMENT]
lemma exact_division: assumes "of_int x / (of_int y  :: 'a :: floor_ceiling) \<in> \<int>"
  shows "of_int (x div y) = of_int x / (of_int y :: 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (x div y) = of_int x / of_int y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
of_int x / of_int y \<in> \<int>

goal (1 subgoal):
 1. of_int (x div y) = of_int x / of_int y
[PROOF STEP]
by (metis Ints_cases division_to_div)


[STATEMENT]
lemma int_via_rat_eqI: "rat_of_int x = rat_of_int y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int x = rat_of_int y \<Longrightarrow> x = y
[PROOF STEP]
by auto


[STATEMENT]
lemma of_int_Gramian_determinant:
  assumes "k \<le> length F" "\<And>i. i < length F \<Longrightarrow> dim_vec (F ! i) = n"
  shows "gs.Gramian_determinant (map of_int_hom.vec_hom F) k = of_int (gs.Gramian_determinant F k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.Gramian_determinant (map of_int_hom.vec_hom F) k = of_int (gs.Gramian_determinant F k)
[PROOF STEP]
unfolding gs.Gramian_determinant_def of_int_hom.hom_det[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (gs.Gramian_matrix (map of_int_hom.vec_hom F) k) = det (of_int_hom.mat_hom (gs.Gramian_matrix F k))
[PROOF STEP]
proof (rule arg_cong[of _ _ det])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gs.Gramian_matrix (map of_int_hom.vec_hom F) k = of_int_hom.mat_hom (gs.Gramian_matrix F k)
[PROOF STEP]
let ?F = "map of_int_hom.vec_hom F"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gs.Gramian_matrix (map of_int_hom.vec_hom F) k = of_int_hom.mat_hom (gs.Gramian_matrix F k)
[PROOF STEP]
have cong: "\<And> a b c d. a = b \<Longrightarrow> c = d \<Longrightarrow> a * c = b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> a * c = b * d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 = ?b2; ?c2 = ?d2\<rbrakk> \<Longrightarrow> ?a2 * ?c2 = ?b2 * ?d2

goal (1 subgoal):
 1. gs.Gramian_matrix (map of_int_hom.vec_hom F) k = of_int_hom.mat_hom (gs.Gramian_matrix F k)
[PROOF STEP]
show "gs.Gramian_matrix ?F k = map_mat of_int (gs.Gramian_matrix F k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.Gramian_matrix (map of_int_hom.vec_hom F) k = of_int_hom.mat_hom (gs.Gramian_matrix F k)
[PROOF STEP]
unfolding gs.Gramian_matrix_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, y). map of_int_hom.vec_hom F ! i $ y) * (mat k n (\<lambda>(i, y). map of_int_hom.vec_hom F ! i $ y))\<^sup>T = of_int_hom.mat_hom (mat k n (\<lambda>(i, y). F ! i $ y) * (mat k n (\<lambda>(i, y). F ! i $ y))\<^sup>T)
[PROOF STEP]
proof (subst of_int_hom.mat_hom_mult[of _ k n _ k], (auto)[2], rule cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mat k n (\<lambda>(i, y). map of_int_hom.vec_hom F ! i $ y) = of_int_hom.mat_hom (mat k n (\<lambda>(i, y). F ! i $ y))
 2. (mat k n (\<lambda>(i, y). map of_int_hom.vec_hom F ! i $ y))\<^sup>T = of_int_hom.mat_hom (mat k n (\<lambda>(i, y). F ! i $ y))\<^sup>T
[PROOF STEP]
show id: "mat k n (\<lambda> (i,j). ?F ! i $ j) = map_mat of_int (mat k n (\<lambda> (i, j). F ! i $ j))" (is "?L = map_mat _ ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))
[PROOF STEP]
proof (rule eq_matI, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))); j < dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))\<rbrakk> \<Longrightarrow> mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) $$ (i, j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)) $$ (i, j)
 2. dim_row (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
 3. dim_col (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
[PROOF STEP]
case (1 i j)
[PROOF STATE]
proof (state)
this:
i < dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
j < dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))); j < dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))\<rbrakk> \<Longrightarrow> mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) $$ (i, j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)) $$ (i, j)
 2. dim_row (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
 3. dim_col (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
[PROOF STEP]
hence ij: "i < k" "j < n" "i < length F" "dim_vec (F ! i) = n"
[PROOF STATE]
proof (prove)
using this:
i < dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
j < dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))

goal (1 subgoal):
 1. (i < k &&& j < n) &&& i < length F &&& dim_vec (F ! i) = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
j < dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
k \<le> length F
?i1 < length F \<Longrightarrow> dim_vec (F ! ?i1) = n

goal (1 subgoal):
 1. (i < k &&& j < n) &&& i < length F &&& dim_vec (F ! i) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < k
j < n
i < length F
dim_vec (F ! i) = n

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))); j < dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))\<rbrakk> \<Longrightarrow> mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) $$ (i, j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)) $$ (i, j)
 2. dim_row (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
 3. dim_col (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) $$ (i, j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)) $$ (i, j)
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i < k
j < n
i < length F
dim_vec (F ! i) = n

goal (1 subgoal):
 1. mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) $$ (i, j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) $$ (i, j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)) $$ (i, j)

goal (2 subgoals):
 1. dim_row (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_row (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
 2. dim_col (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j)) = dim_col (of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j)))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j) = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))

goal (1 subgoal):
 1. (mat k n (\<lambda>(i, y). map of_int_hom.vec_hom F ! i $ y))\<^sup>T = of_int_hom.mat_hom (mat k n (\<lambda>(i, y). F ! i $ y))\<^sup>T
[PROOF STEP]
show "?L\<^sup>T = map_mat of_int ?R\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j))\<^sup>T = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))\<^sup>T
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_hom.mat_hom (mat k n (\<lambda>(i, y). F ! i $ y)))\<^sup>T = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))\<^sup>T
[PROOF STEP]
by (rule eq_matI, auto)
[PROOF STATE]
proof (state)
this:
(mat k n (\<lambda>(i, j). map of_int_hom.vec_hom F ! i $ j))\<^sup>T = of_int_hom.mat_hom (mat k n (\<lambda>(i, j). F ! i $ j))\<^sup>T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gs.Gramian_matrix (map of_int_hom.vec_hom F) k = of_int_hom.mat_hom (gs.Gramian_matrix F k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gramian_determinant:
  assumes k: "k \<le> m"
  shows "of_int (gs.Gramian_determinant fs k) = (\<Prod> j<k. sq_norm (gs.gso j))" (is ?g1)
    "gs.Gramian_determinant fs k > 0" (is ?g2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (gs.Gramian_determinant fs k) = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2) &&& 0 < gs.Gramian_determinant fs k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rat_of_int (gs.Gramian_determinant fs k) = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
 2. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
have hom: "gs.Gramian_determinant (RAT fs) k = of_int (gs.Gramian_determinant fs k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.d k = rat_of_int (gs.Gramian_determinant fs k)
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs

goal (1 subgoal):
 1. gs.d k = rat_of_int (gs.Gramian_determinant fs k)
[PROOF STEP]
by (intro of_int_Gramian_determinant) auto
[PROOF STATE]
proof (state)
this:
gs.d k = rat_of_int (gs.Gramian_determinant fs k)

goal (2 subgoals):
 1. rat_of_int (gs.Gramian_determinant fs k) = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
 2. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
show ?g1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (gs.Gramian_determinant fs k) = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
unfolding hom[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.d k = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
using gs.Gramian_determinant assms
[PROOF STATE]
proof (prove)
using this:
?k \<le> length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.d ?k = (\<Prod>j<?k. \<parallel>gs.gso j\<parallel>\<^sup>2)
?k \<le> length (map of_int_hom.vec_hom fs) \<Longrightarrow> 0 < gs.d ?k
k \<le> length fs

goal (1 subgoal):
 1. gs.d k = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rat_of_int (gs.Gramian_determinant fs k) = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)

goal (1 subgoal):
 1. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
show ?g2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
using hom gs.Gramian_determinant assms
[PROOF STATE]
proof (prove)
using this:
gs.d k = rat_of_int (gs.Gramian_determinant fs k)
?k \<le> length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.d ?k = (\<Prod>j<?k. \<parallel>gs.gso j\<parallel>\<^sup>2)
?k \<le> length (map of_int_hom.vec_hom fs) \<Longrightarrow> 0 < gs.d ?k
k \<le> length fs

goal (1 subgoal):
 1. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < gs.Gramian_determinant fs k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fs_int_d_pos [intro]:
  assumes k: "k \<le> m"
shows "d fs k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < d fs k
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
using Gramian_determinant[OF k]
[PROOF STATE]
proof (prove)
using this:
rat_of_int (gs.Gramian_determinant fs k) = (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
0 < gs.Gramian_determinant fs k

goal (1 subgoal):
 1. 0 < gs.Gramian_determinant fs k
[PROOF STEP]
by auto


[STATEMENT]
lemma fs_int_d_Suc:
  assumes k: "k < m"
shows "of_int (d fs (Suc k)) = sq_norm (gs.gso k) * of_int (d fs k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc k)) = \<parallel>gs.gso k\<parallel>\<^sup>2 * rat_of_int (d fs k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc k)) = \<parallel>gs.gso k\<parallel>\<^sup>2 * rat_of_int (d fs k)
[PROOF STEP]
from k
[PROOF STATE]
proof (chain)
picking this:
k < length fs
[PROOF STEP]
have k: "k \<le> m" "Suc k \<le> m"
[PROOF STATE]
proof (prove)
using this:
k < length fs

goal (1 subgoal):
 1. k \<le> length fs &&& Suc k \<le> length fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<le> length fs
Suc k \<le> length fs

goal (1 subgoal):
 1. rat_of_int (d fs (Suc k)) = \<parallel>gs.gso k\<parallel>\<^sup>2 * rat_of_int (d fs k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc k)) = \<parallel>gs.gso k\<parallel>\<^sup>2 * rat_of_int (d fs k)
[PROOF STEP]
unfolding Gramian_determinant[OF k(1)] Gramian_determinant[OF k(2)] d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j<Suc k. \<parallel>gs.gso j\<parallel>\<^sup>2) = \<parallel>gs.gso k\<parallel>\<^sup>2 * (\<Prod>j<k. \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
by (subst prod.remove[of _ k], force+, rule arg_cong[of _ _ "\<lambda> x. _ * x"], rule prod.cong, auto)
[PROOF STATE]
proof (state)
this:
rat_of_int (d fs (Suc k)) = \<parallel>gs.gso k\<parallel>\<^sup>2 * rat_of_int (d fs k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fs_int_D_pos:
shows "D fs > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < D fs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < D fs
[PROOF STEP]
have "(\<Prod> j < m. d fs j) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < prod (d fs) {..<length fs}
[PROOF STEP]
by (rule prod_pos, insert fs_int_d_pos, auto)
[PROOF STATE]
proof (state)
this:
0 < prod (d fs) {..<length fs}

goal (1 subgoal):
 1. 0 < D fs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < prod (d fs) {..<length fs}

goal (1 subgoal):
 1. 0 < D fs
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
using this:
0 < prod (d fs) {..<length fs}

goal (1 subgoal):
 1. 0 < nat (prod (d fs) {..<length fs})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < D fs

goal:
No subgoals!
[PROOF STEP]
qed