[STATEMENT]
lemma lattice_of_of_int: assumes G: "set F \<subseteq> carrier_vec n"
  and "f \<in> vec_module.lattice_of n F"
shows "map_vec rat_of_int f \<in> vec_module.lattice_of n (map (map_vec of_int) F)"
  (is "?f \<in> vec_module.lattice_of _ ?F")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
let ?sl = "abelian_monoid.sumlist (module_vec TYPE('a::semiring_1) n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
note d = vec_module.lattice_of_def
[PROOF STATE]
proof (state)
this:
vec_module.lattice_of ?n ?fs = range (\<lambda>c. abelian_monoid.sumlist (module_vec TYPE(?'a) ?n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v ?fs ! i) [0..<length ?fs]))

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
note dim = vec_module.sumlist_dim
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> set ?xs \<Longrightarrow> x \<in> carrier_vec ?n) \<Longrightarrow> dim_vec (abelian_monoid.sumlist (module_vec TYPE(?'a) ?n) ?xs) = ?n

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
note sumlist_vec_index = vec_module.sumlist_vec_index
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>x. x \<in> set ?xs \<Longrightarrow> x \<in> carrier_vec ?n; ?i < ?n\<rbrakk> \<Longrightarrow> abelian_monoid.sumlist (module_vec TYPE(?'a) ?n) ?xs $ ?i = (\<Sum>x\<leftarrow>?xs. x $ ?i)

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
from G
[PROOF STATE]
proof (chain)
picking this:
set F \<subseteq> carrier_vec n
[PROOF STEP]
have Gi: "\<And> i. i < length F \<Longrightarrow> F ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set F \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < length F \<Longrightarrow> F ! i \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < length F \<Longrightarrow> F ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
from Gi
[PROOF STATE]
proof (chain)
picking this:
?i1 < length F \<Longrightarrow> F ! ?i1 \<in> carrier_vec n
[PROOF STEP]
have Gid: "\<And> i. i < length F \<Longrightarrow> dim_vec (F ! i) = n"
[PROOF STATE]
proof (prove)
using this:
?i1 < length F \<Longrightarrow> F ! ?i1 \<in> carrier_vec n

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

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
from assms(2)[unfolded d]
[PROOF STATE]
proof (chain)
picking this:
f \<in> range (\<lambda>c. abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F]))
[PROOF STEP]
obtain c where
    ffc: "f = ?sl (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F])" (is "_ = ?g")
[PROOF STATE]
proof (prove)
using this:
f \<in> range (\<lambda>c. abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F]))

goal (1 subgoal):
 1. (\<And>c. f = abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F])

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
have "?f = ?sl (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v ?F ! i) [0..<length ?F])" (is "_ = ?gg")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])
[PROOF STEP]
have d1[simp]: "dim_vec ?g = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F])) = n
[PROOF STEP]
by (subst dim, auto simp: Gi)
[PROOF STATE]
proof (state)
this:
dim_vec (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F])) = n

goal (1 subgoal):
 1. of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])
[PROOF STEP]
have d2[simp]: "dim_vec ?gg = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])) = n
[PROOF STEP]
unfolding length_map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])) = n
[PROOF STEP]
by (subst vec_module.sumlist_dim, auto simp: Gi G)
[PROOF STATE]
proof (state)
this:
dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])) = n

goal (1 subgoal):
 1. of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])
[PROOF STEP]
unfolding ffc length_map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F])) = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])
[PROOF STEP]
apply (rule eq_vecI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])) \<Longrightarrow> of_int_hom.vec_hom (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F])) $ i = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F]) $ i
 2. dim_vec (of_int_hom.vec_hom (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v F ! i) [0..<length F]))) = dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F]))
[PROOF STEP]
apply (insert d1 d2, auto)[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. c i \<cdot>\<^sub>v F ! i) [0..<length F])) = n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])) = n\<rbrakk> \<Longrightarrow> rat_of_int (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. c i \<cdot>\<^sub>v F ! i) [0..<length F]) $ i) = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F]) $ i
[PROOF STEP]
apply (subst (1 2) sumlist_vec_index, auto simp: o_def Gi G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. c i \<cdot>\<^sub>v F ! i) [0..<length F])) = n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])) = n\<rbrakk> \<Longrightarrow> rat_of_int (\<Sum>x\<leftarrow>[0..<length F]. (c x \<cdot>\<^sub>v F ! x) $ i) = (\<Sum>x\<leftarrow>[0..<length F]. (rat_of_int (c x) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! x) $ i)
[PROOF STEP]
apply (unfold of_int_hom.hom_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. c i \<cdot>\<^sub>v F ! i) [0..<length F])) = n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])) = n\<rbrakk> \<Longrightarrow> sum_list (map rat_of_int (map (\<lambda>x. (c x \<cdot>\<^sub>v F ! x) $ i) [0..<length F])) = (\<Sum>x\<leftarrow>[0..<length F]. (rat_of_int (c x) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! x) $ i)
[PROOF STEP]
apply (intro arg_cong[of _ _ sum_list] map_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(int) n) (map (\<lambda>i. c i \<cdot>\<^sub>v F ! i) [0..<length F])) = n; dim_vec (abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length F])) = n\<rbrakk> \<Longrightarrow> map rat_of_int (map (\<lambda>x. (c x \<cdot>\<^sub>v F ! x) $ i) [0..<length F]) = map (\<lambda>x. (rat_of_int (c x) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! x) $ i) [0..<length F]
[PROOF STEP]
by (auto simp: G Gi, (subst index_smult_vec, simp add: Gid)+,
         subst index_map_vec, auto simp: Gid)
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
thus "?f \<in> vec_module.lattice_of n ?F"
[PROOF STATE]
proof (prove)
using this:
of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
using this:
of_int_hom.vec_hom f = abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)])

goal (1 subgoal):
 1. of_int_hom.vec_hom f \<in> range (\<lambda>c. abelian_monoid.sumlist (module_vec TYPE(rat) n) (map (\<lambda>i. rat_of_int (c i) \<cdot>\<^sub>v map of_int_hom.vec_hom F ! i) [0..<length (map of_int_hom.vec_hom F)]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom f \<in> vec_module.lattice_of n (map of_int_hom.vec_hom F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Hadamard's_inequality:
  fixes A::"real mat"
  assumes A: "A \<in> carrier_mat n n"
  shows  "abs (det A) \<le> sqrt (prod_list (map sq_norm (rows A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
let ?us = "map (row A) [0 ..< n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
interpret gso: gram_schmidt_fs n ?us
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have len: "length ?us = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (row A) [0..<n]) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map (row A) [0..<n]) = n

goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have us: "set ?us \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (row A) [0..<n]) \<subseteq> carrier_vec n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. set (map (row A) [0..<n]) \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map (row A) [0..<n]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
let ?vs = "map gso.gso [0..<n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
proof (cases "carrier_vec n \<subseteq> gso.span (set ?us)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n]))

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
with us len
[PROOF STATE]
proof (chain)
picking this:
set (map (row A) [0..<n]) \<subseteq> carrier_vec n
length (map (row A) [0..<n]) = n
carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n]))
[PROOF STEP]
have basis: "gso.basis_list ?us"
[PROOF STATE]
proof (prove)
using this:
set (map (row A) [0..<n]) \<subseteq> carrier_vec n
length (map (row A) [0..<n]) = n
carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n]))

goal (1 subgoal):
 1. gso.basis_list (map (row A) [0..<n])
[PROOF STEP]
unfolding gso.basis_list_def
[PROOF STATE]
proof (prove)
using this:
set (map (row A) [0..<n]) \<subseteq> carrier_vec n
length (map (row A) [0..<n]) = n
carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n]))

goal (1 subgoal):
 1. set (map (row A) [0..<n]) \<subseteq> carrier_vec n \<and> length (map (row A) [0..<n]) = n \<and> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gso.basis_list (map (row A) [0..<n])

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
note in_dep = gso.basis_list_imp_lin_indpt_list[OF basis]
[PROOF STATE]
proof (state)
this:
gso.lin_indpt_list (map (row A) [0..<n])

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
interpret gso: gram_schmidt_fs_lin_indpt n ?us
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_fs_lin_indpt n (map (row A) [0..<n])
[PROOF STEP]
by (standard) (use in_dep gso.lin_indpt_list_def in auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have last: "0 \<le> prod_list (map sq_norm ?vs) \<and> prod_list (map sq_norm ?vs) \<le> prod_list (map sq_norm ?us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> prod_list (map sq_norm (map gso.gso [0..<n])) \<and> prod_list (map sq_norm (map gso.gso [0..<n])) \<le> prod_list (map sq_norm (map (row A) [0..<n]))
[PROOF STEP]
proof (rule prod_list_le_mono, force, unfold length_map length_upt)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
assume "i < n - 0"
[PROOF STATE]
proof (state)
this:
i < n - 0

goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
hence i: "i < n"
[PROOF STATE]
proof (prove)
using this:
i < n - 0

goal (1 subgoal):
 1. i < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
have vsi: "map sq_norm ?vs ! i = sq_norm (?vs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map sq_norm (map gso.gso [0..<n]) ! i = \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. map sq_norm (map gso.gso [0..<n]) ! i = \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map sq_norm (map gso.gso [0..<n]) ! i = \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
have usi: "map sq_norm ?us ! i = sq_norm (row A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map sq_norm (map (row A) [0..<n]) ! i = \<parallel>row A i\<parallel>\<^sup>2
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. map sq_norm (map (row A) [0..<n]) ! i = \<parallel>row A i\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map sq_norm (map (row A) [0..<n]) ! i = \<parallel>row A i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
have zero: "0 \<le> sq_norm (?vs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
have le: "sq_norm (?vs ! i) \<le> sq_norm (row A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<le> \<parallel>row A i\<parallel>\<^sup>2
[PROOF STEP]
using gso.sq_norm_gso_le_f i
[PROOF STATE]
proof (prove)
using this:
?i < length (map (row A) [0..<n]) \<Longrightarrow> \<parallel>gso.gso ?i\<parallel>\<^sup>2 \<le> \<parallel>map (row A) [0..<n] ! ?i\<parallel>\<^sup>2
i < n

goal (1 subgoal):
 1. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<le> \<parallel>row A i\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<le> \<parallel>row A i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. i < n - 0 \<Longrightarrow> 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
show "0 \<le> map sq_norm ?vs ! i \<and> map sq_norm ?vs ! i \<le> map sq_norm ?us ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i
[PROOF STEP]
unfolding vsi usi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<and> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<le> \<parallel>row A i\<parallel>\<^sup>2
[PROOF STEP]
using zero le
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2
\<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<le> \<parallel>row A i\<parallel>\<^sup>2

goal (1 subgoal):
 1. 0 \<le> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<and> \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2 \<le> \<parallel>row A i\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> map sq_norm (map gso.gso [0..<n]) ! i \<and> map sq_norm (map gso.gso [0..<n]) ! i \<le> map sq_norm (map (row A) [0..<n]) ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> prod_list (map sq_norm (map gso.gso [0..<n])) \<and> prod_list (map sq_norm (map gso.gso [0..<n])) \<le> prod_list (map sq_norm (map (row A) [0..<n]))

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have Fs: "gso.FF \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n (map (row A) [0..<n]) \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_rows n (map (row A) [0..<n]) \<in> carrier_mat n n

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have A_Fs: "A = gso.FF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = mat_of_rows n (map (row A) [0..<n])
[PROOF STEP]
by (rule eq_matI, subst gso.FF_index, insert A, auto)
[PROOF STATE]
proof (state)
this:
A = mat_of_rows n (map (row A) [0..<n])

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
hence "abs (det A) = abs (det (gso.FF))"
[PROOF STATE]
proof (prove)
using this:
A = mat_of_rows n (map (row A) [0..<n])

goal (1 subgoal):
 1. \<bar>det A\<bar> = \<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>det A\<bar> = \<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar>

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
(* the following three steps are based on a discussion with Bertram Felgenhauer *)
[PROOF STATE]
proof (state)
this:
\<bar>det A\<bar> = \<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar>

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>det A\<bar> = \<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar>

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "\<dots> = abs (sqrt (det (gso.FF) * det (gso.FF)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar> = \<bar>sqrt (det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])))\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar> = \<bar>sqrt (det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])))\<bar>

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>det (mat_of_rows n (map (row A) [0..<n]))\<bar> = \<bar>sqrt (det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])))\<bar>

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "det (gso.FF) * det (gso.FF) = det (gso.FF) * det (gso.FF)\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])) = det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))\<^sup>T
[PROOF STEP]
unfolding det_transpose[OF Fs]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])) = det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])) = det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))\<^sup>T

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n])) = det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))\<^sup>T

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "\<dots> = det (gso.FF * (gso.FF)\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))\<^sup>T = det (mat_of_rows n (map (row A) [0..<n]) * (mat_of_rows n (map (row A) [0..<n]))\<^sup>T)
[PROOF STEP]
by (subst det_mult[OF Fs], insert Fs, auto)
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))\<^sup>T = det (mat_of_rows n (map (row A) [0..<n]) * (mat_of_rows n (map (row A) [0..<n]))\<^sup>T)

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n (map (row A) [0..<n])) * det (mat_of_rows n (map (row A) [0..<n]))\<^sup>T = det (mat_of_rows n (map (row A) [0..<n]) * (mat_of_rows n (map (row A) [0..<n]))\<^sup>T)

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "\<dots> = gso.Gramian_determinant ?us n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n (map (row A) [0..<n]) * (mat_of_rows n (map (row A) [0..<n]))\<^sup>T) = gso.Gramian_determinant (map (row A) [0..<n]) n
[PROOF STEP]
unfolding gso.Gramian_matrix_def gso.Gramian_determinant_def Let_def A_Fs[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (A * A\<^sup>T) = det (mat n n (\<lambda>(i, y). map (row A) [0..<n] ! i $ y) * (mat n n (\<lambda>(i, y). map (row A) [0..<n] ! i $ y))\<^sup>T)
[PROOF STEP]
by (rule arg_cong[of _ _ det], rule arg_cong2[of _ _ _ _ "(*)"], insert A, auto)
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n (map (row A) [0..<n]) * (mat_of_rows n (map (row A) [0..<n]))\<^sup>T) = gso.Gramian_determinant (map (row A) [0..<n]) n

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n (map (row A) [0..<n]) * (mat_of_rows n (map (row A) [0..<n]))\<^sup>T) = gso.Gramian_determinant (map (row A) [0..<n]) n

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "\<dots> = (\<Prod>j \<in> set [0 ..< n]. \<parallel>?vs ! j\<parallel>\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso.Gramian_determinant (map (row A) [0..<n]) n = (\<Prod>j\<in>set [0..<n]. \<parallel>map gso.gso [0..<n] ! j\<parallel>\<^sup>2)
[PROOF STEP]
by (subst gso.Gramian_determinant) (auto intro!: prod.cong)
[PROOF STATE]
proof (state)
this:
gso.Gramian_determinant (map (row A) [0..<n]) n = (\<Prod>j\<in>set [0..<n]. \<parallel>map gso.gso [0..<n] ! j\<parallel>\<^sup>2)

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso.Gramian_determinant (map (row A) [0..<n]) n = (\<Prod>j\<in>set [0..<n]. \<parallel>map gso.gso [0..<n] ! j\<parallel>\<^sup>2)

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "\<dots> = prod_list (map (\<lambda> i. sq_norm (?vs ! i)) [0 ..< n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j\<in>set [0..<n]. \<parallel>map gso.gso [0..<n] ! j\<parallel>\<^sup>2) = (\<Prod>i\<leftarrow>[0..<n]. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2)
[PROOF STEP]
by (subst prod.distinct_set_conv_list, auto)
[PROOF STATE]
proof (state)
this:
(\<Prod>j\<in>set [0..<n]. \<parallel>map gso.gso [0..<n] ! j\<parallel>\<^sup>2) = (\<Prod>i\<leftarrow>[0..<n]. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2)

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>j\<in>set [0..<n]. \<parallel>map gso.gso [0..<n] ! j\<parallel>\<^sup>2) = (\<Prod>i\<leftarrow>[0..<n]. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2)

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "map (\<lambda> i. sq_norm (?vs ! i)) [0 ..< n] = map sq_norm ?vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2) [0..<n] = map sq_norm (map gso.gso [0..<n])
[PROOF STEP]
by (intro nth_equalityI, auto)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2) [0..<n] = map sq_norm (map gso.gso [0..<n])

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. \<parallel>map gso.gso [0..<n] ! i\<parallel>\<^sup>2) [0..<n] = map sq_norm (map gso.gso [0..<n])

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "abs (sqrt (prod_list \<dots>)) \<le> sqrt (prod_list (map sq_norm ?us))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>sqrt (prod_list (map sq_norm (map gso.gso [0..<n])))\<bar> \<le> sqrt (prod_list (map sq_norm (map (row A) [0..<n])))
[PROOF STEP]
using last
[PROOF STATE]
proof (prove)
using this:
0 \<le> prod_list (map sq_norm (map gso.gso [0..<n])) \<and> prod_list (map sq_norm (map gso.gso [0..<n])) \<le> prod_list (map sq_norm (map (row A) [0..<n]))

goal (1 subgoal):
 1. \<bar>sqrt (prod_list (map sq_norm (map gso.gso [0..<n])))\<bar> \<le> sqrt (prod_list (map sq_norm (map (row A) [0..<n])))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>sqrt (prod_list (map sq_norm (map gso.gso [0..<n])))\<bar> \<le> sqrt (prod_list (map sq_norm (map (row A) [0..<n])))

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>sqrt (prod_list (map sq_norm (map gso.gso [0..<n])))\<bar> \<le> sqrt (prod_list (map sq_norm (map (row A) [0..<n])))

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have "?us = rows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (row A) [0..<n] = rows A
[PROOF STEP]
unfolding rows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (row A) [0..<n] = map (row A) [0..<dim_row A]
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. map (row A) [0..<n] = map (row A) [0..<dim_row A]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (row A) [0..<n] = rows A

goal (2 subgoals):
 1. carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
 2. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))

goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))

goal (1 subgoal):
 1. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n]))

goal (1 subgoal):
 1. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
from mat_of_rows_rows[unfolded rows_def,of A] A gram_schmidt.non_span_det_zero[OF len False us]
[PROOF STATE]
proof (chain)
picking this:
mat_of_rows (dim_col A) (map (row A) [0..<dim_row A]) = A
A \<in> carrier_mat n n
det (mat_of_rows n (map (row A) [0..<n])) = 0
[PROOF STEP]
have zero: "det A = 0"
[PROOF STATE]
proof (prove)
using this:
mat_of_rows (dim_col A) (map (row A) [0..<dim_row A]) = A
A \<in> carrier_mat n n
det (mat_of_rows n (map (row A) [0..<n])) = 0

goal (1 subgoal):
 1. det A = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det A = 0

goal (1 subgoal):
 1. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
have ge: "prod_list (map sq_norm (rows A)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> prod_list (map sq_norm (rows A))
[PROOF STEP]
by (rule prod_list_nonneg, auto simp: sq_norm_vec_ge_0)
[PROOF STATE]
proof (state)
this:
0 \<le> prod_list (map sq_norm (rows A))

goal (1 subgoal):
 1. \<not> carrier_vec n \<subseteq> gso.span (set (map (row A) [0..<n])) \<Longrightarrow> \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
unfolding zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>0\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
using ge
[PROOF STATE]
proof (prove)
using this:
0 \<le> prod_list (map sq_norm (rows A))

goal (1 subgoal):
 1. \<bar>0\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>det A\<bar> \<le> sqrt (prod_list (map sq_norm (rows A)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_gram_schmidt_int : "snd (gram_schmidt_int n us) = gram_schmidt n (map (map_vec of_int) us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (gram_schmidt_int n us) = gram_schmidt n (map of_int_hom.vec_hom us)
[PROOF STEP]
unfolding gram_schmidt_int_def gram_schmidt_wit_def gram_schmidt_fs.gso_connect
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt n (map of_int_hom.vec_hom us) = gram_schmidt n (map of_int_hom.vec_hom us)
[PROOF STEP]
by metis


[STATEMENT]
lemma gram_schmidt_sub_triv: "gram_schmidt_sub_triv n ((map (\<lambda> x. (x,sq_norm x)) us)) ws =
  map (\<lambda> x. (x, sq_norm x)) (gram_schmidt_sub n us ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_sub_triv n (map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) us) ws = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) (gram_schmidt_sub n us ws)
[PROOF STEP]
by (rule sym, induct ws arbitrary: us, auto simp: adjuster_triv o_def Let_def)


[STATEMENT]
lemma gram_schmidt_triv[simp]: "gram_schmidt_triv n ws = map (\<lambda> x. (x,sq_norm x)) (gram_schmidt n ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_triv n ws = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) (gram_schmidt n ws)
[PROOF STEP]
unfolding gram_schmidt_def gram_schmidt_triv_def rev_map[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (gram_schmidt_sub_triv n [] ws) = rev (map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) (gram_schmidt_sub n [] ws))
[PROOF STEP]
by (auto simp: gram_schmidt_sub_triv[symmetric])


[STATEMENT]
lemma adjuster_wit_carrier_vec:
  assumes "f \<in> carrier_vec n" "set gs \<subseteq> carrier_vec n"
  shows "snd (adjuster_wit mus f gs) \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (adjuster_wit mus f gs) \<in> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. snd (adjuster_wit mus f gs) \<in> carrier_vec n
[PROOF STEP]
by (induction mus f gs rule: adjuster_wit.induct) (auto simp add: Let_def case_prod_beta')


[STATEMENT]
lemma adjuster_wit'':
  assumes "adjuster_wit mus_acc f gs = (mus, g')" "n_gs = map (\<lambda>x. (x, sq_norm_vec x)) gs"
 "f \<in> carrier_vec n" "acc \<in> carrier_vec n" "set gs \<subseteq> carrier_vec n"
  shows "mus_adjuster f n_gs mus_acc acc = (mus, acc + g')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc acc = (mus, acc + g')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
adjuster_wit mus_acc f gs = (mus, g')
n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc acc = (mus, acc + g')
[PROOF STEP]
proof(induction f n_gs mus_acc acc arbitrary: g' gs mus rule: mus_adjuster.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f mus g' g'a gs musa. \<lbrakk>adjuster_wit mus f gs = (musa, g'a); [] = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f [] mus g' = (musa, g' + g'a)
 2. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
case (1 mus' f acc g)
[PROOF STATE]
proof (state)
this:
adjuster_wit f mus' gs = (mus, g)
[] = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
mus' \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (2 subgoals):
 1. \<And>f mus g' g'a gs musa. \<lbrakk>adjuster_wit mus f gs = (musa, g'a); [] = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f [] mus g' = (musa, g' + g'a)
 2. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjuster_wit f mus' gs = (mus, g)
[] = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
mus' \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
adjuster_wit f mus' gs = (mus, g)
[] = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
mus' \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster mus' [] f acc = (mus, acc + g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mus_adjuster mus' [] f acc = (mus, acc + g)

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
case (2 f g n_g n_gs mus_acc acc g' gs mus)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
let ?gg = "snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n
[PROOF STEP]
have l: "gs = g # tl gs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. gs = g # tl gs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gs = g # tl gs

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
have gg: "?gg \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n
[PROOF STEP]
by (auto intro!: adjuster_wit_carrier_vec)
[PROOF STATE]
proof (state)
this:
snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n
[PROOF STEP]
have [simp]: "g' = (- (f \<bullet> g / \<parallel>g\<parallel>\<^sup>2) \<cdot>\<^sub>v g + ?gg)"
[PROOF STATE]
proof (prove)
using this:
snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n

goal (1 subgoal):
 1. g' = - (f \<bullet> g / \<parallel>g\<parallel>\<^sup>2) \<cdot>\<^sub>v g + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. g' = - (f \<bullet> g / \<parallel>g\<parallel>\<^sup>2) \<cdot>\<^sub>v g + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs))
[PROOF STEP]
by (auto simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
g' = - (f \<bullet> g / \<parallel>g\<parallel>\<^sup>2) \<cdot>\<^sub>v g + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs))

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
have "mus_adjuster f ((g, n_g) # n_gs) mus_acc acc =
        mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc)
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc)

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc)

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
have "\<dots> = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + ?gg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
have "adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, ?gg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
by (subst (asm) l) (auto simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))

goal (1 subgoal):
 1. mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))

goal (1 subgoal):
 1. mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs) = (mus, snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
by (subst 2(1)[of _ "tl gs"]) (auto simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mus_adjuster f n_gs (f \<bullet> g / n_g # mus_acc) (- (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc) = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))

goal (1 subgoal):
 1. \<And>f g ng n_gs mus g' g'a gs musa. \<lbrakk>\<And>x g'a gs musa. \<lbrakk>x = f \<bullet> g / ng; adjuster_wit (x # mus) f gs = (musa, g'a); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; - x \<cdot>\<^sub>v g + g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (x # mus) (- x \<cdot>\<^sub>v g + g') = (musa, - x \<cdot>\<^sub>v g + g' + g'a); adjuster_wit mus f gs = (musa, g'a); (g, ng) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs; f \<in> carrier_vec n; g' \<in> carrier_vec n; set gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f ((g, ng) # n_gs) mus g' = (musa, g' + g'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))

goal (1 subgoal):
 1. mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = (mus, acc + g')
[PROOF STEP]
using 2 gg
[PROOF STATE]
proof (prove)
using this:
mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = (mus, - (f \<bullet> g / n_g) \<cdot>\<^sub>v g + acc + snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)))
\<lbrakk>?x3 = f \<bullet> g / n_g; adjuster_wit (?x3 # mus_acc) f ?gs3 = (?mus3, ?g'3); n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs3; f \<in> carrier_vec n; - ?x3 \<cdot>\<^sub>v g + acc \<in> carrier_vec n; set ?gs3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> mus_adjuster f n_gs (?x3 # mus_acc) (- ?x3 \<cdot>\<^sub>v g + acc) = (?mus3, - ?x3 \<cdot>\<^sub>v g + acc + ?g'3)
adjuster_wit mus_acc f gs = (mus, g')
(g, n_g) # n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
acc \<in> carrier_vec n
set gs \<subseteq> carrier_vec n
snd (adjuster_wit (f \<bullet> g / n_g # mus_acc) f (tl gs)) \<in> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = (mus, acc + g')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mus_adjuster f ((g, n_g) # n_gs) mus_acc acc = (mus, acc + g')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjuster_wit':
  assumes "n_gs = map (\<lambda>x. (x, sq_norm_vec x)) gs" "f \<in> carrier_vec n" "set gs \<subseteq> carrier_vec n"
  shows "mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
let ?g = "snd (adjuster_wit mus_acc f gs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
let ?mus = "fst (adjuster_wit mus_acc f gs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
have "?g \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (adjuster_wit mus_acc f gs) \<in> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. snd (adjuster_wit mus_acc f gs) \<in> carrier_vec n
[PROOF STEP]
by (auto intro!: adjuster_wit_carrier_vec)
[PROOF STATE]
proof (state)
this:
snd (adjuster_wit mus_acc f gs) \<in> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd (adjuster_wit mus_acc f gs) \<in> carrier_vec n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
snd (adjuster_wit mus_acc f gs) \<in> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
snd (adjuster_wit mus_acc f gs) \<in> carrier_vec n
n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs
f \<in> carrier_vec n
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs
[PROOF STEP]
by (subst adjuster_wit''[of _ _ gs ?mus ?g]) (auto simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
mus_adjuster f n_gs mus_acc (0\<^sub>v n) = adjuster_wit mus_acc f gs

goal:
No subgoals!
[PROOF STEP]
qed