[STATEMENT]
lemma Gramian_determinant:
  assumes k: "k \<le> m"
  shows "Gramian_determinant fs k = (\<Prod> j<k. sq_norm (gso j))"
    "Gramian_determinant fs k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2) &&& (0::'a) < Gramian_determinant fs k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
define Gk where "Gk = mat k n (\<lambda> (i,j). fs ! i $ j)"
[PROOF STATE]
proof (state)
this:
Gk = mat k n (\<lambda>(i, j). fs ! i $ j)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have Gk: "Gk \<in> carrier_mat k n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gk \<in> carrier_mat k n
[PROOF STEP]
unfolding Gk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, y). fs ! i $ y) \<in> carrier_mat k n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gk \<in> carrier_mat k n

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
define Mk where "Mk = mat k k (\<lambda> (i,j). \<mu> i j)"
[PROOF STATE]
proof (state)
this:
Mk = mat k k (\<lambda>(x, y). \<mu> x y)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have Mk_\<mu>: "i < k \<Longrightarrow> j < k \<Longrightarrow> Mk $$ (i,j) = \<mu> i j" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < k; j < k\<rbrakk> \<Longrightarrow> Mk $$ (i, j) = \<mu> i j
[PROOF STEP]
unfolding Mk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < k; j < k\<rbrakk> \<Longrightarrow> mat k k (\<lambda>(x, y). \<mu> x y) $$ (i, j) = \<mu> i j
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs

goal (1 subgoal):
 1. \<lbrakk>i < k; j < k\<rbrakk> \<Longrightarrow> mat k k (\<lambda>(x, y). \<mu> x y) $$ (i, j) = \<mu> i j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 < k; ?j1 < k\<rbrakk> \<Longrightarrow> Mk $$ (?i1, ?j1) = \<mu> ?i1 ?j1

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have Mk: "Mk \<in> carrier_mat k k" and [simp]: "dim_row Mk = k" "dim_col Mk = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mk \<in> carrier_mat k k &&& dim_row Mk = k &&& dim_col Mk = k
[PROOF STEP]
unfolding Mk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k k (\<lambda>(x, y). \<mu> x y) \<in> carrier_mat k k &&& dim_row (mat k k (\<lambda>(x, y). \<mu> x y)) = k &&& dim_col (mat k k (\<lambda>(x, y). \<mu> x y)) = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mk \<in> carrier_mat k k
dim_row Mk = k
dim_col Mk = k

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "det Mk = prod_list (diag_mat Mk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det Mk = prod_list (diag_mat Mk)
[PROOF STEP]
by (rule det_lower_triangular[OF _ Mk], auto simp: Mk_\<mu> \<mu>.simps)
[PROOF STATE]
proof (state)
this:
det Mk = prod_list (diag_mat Mk)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det Mk = prod_list (diag_mat Mk)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (diag_mat Mk) = (1::'a)
[PROOF STEP]
by (rule prod_list_neutral, auto simp: diag_mat_def Mk_\<mu> \<mu>.simps)
[PROOF STATE]
proof (state)
this:
prod_list (diag_mat Mk) = (1::'a)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det Mk = (1::'a)
[PROOF STEP]
have detMk: "det Mk = 1"
[PROOF STATE]
proof (prove)
using this:
det Mk = (1::'a)

goal (1 subgoal):
 1. det Mk = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det Mk = (1::'a)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
define Gsk where "Gsk = mat k n (\<lambda> (i,j). gso i $ j)"
[PROOF STATE]
proof (state)
this:
Gsk = mat k n (\<lambda>(i, j). gso i $ j)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have Gsk: "Gsk \<in> carrier_mat k n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gsk \<in> carrier_mat k n
[PROOF STEP]
unfolding Gsk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, y). gso i $ y) \<in> carrier_mat k n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gsk \<in> carrier_mat k n

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have Gsk': "Gsk\<^sup>T \<in> carrier_mat n k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gsk\<^sup>T \<in> carrier_mat n k
[PROOF STEP]
using Gsk
[PROOF STATE]
proof (prove)
using this:
Gsk \<in> carrier_mat k n

goal (1 subgoal):
 1. Gsk\<^sup>T \<in> carrier_mat n k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gsk\<^sup>T \<in> carrier_mat n k

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
let ?Rn = "carrier_vec n"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have id: "Gk = Mk * Gsk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gk = Mk * Gsk
[PROOF STEP]
proof (rule eq_matI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
 2. dim_row Gk = dim_row (Mk * Gsk)
 3. dim_col Gk = dim_col (Mk * Gsk)
[PROOF STEP]
from Gk Mk Gsk
[PROOF STATE]
proof (chain)
picking this:
Gk \<in> carrier_mat k n
Mk \<in> carrier_mat k k
Gsk \<in> carrier_mat k n
[PROOF STEP]
have dim: "dim_row Gk = k" "dim_row (Mk * Gsk) = k" "dim_col Gk = n" "dim_col (Mk * Gsk) = n"
[PROOF STATE]
proof (prove)
using this:
Gk \<in> carrier_mat k n
Mk \<in> carrier_mat k k
Gsk \<in> carrier_mat k n

goal (1 subgoal):
 1. (dim_row Gk = k &&& dim_row (Mk * Gsk) = k) &&& dim_col Gk = n &&& dim_col (Mk * Gsk) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row Gk = k
dim_row (Mk * Gsk) = k
dim_col Gk = n
dim_col (Mk * Gsk) = n

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
 2. dim_row Gk = dim_row (Mk * Gsk)
 3. dim_col Gk = dim_col (Mk * Gsk)
[PROOF STEP]
from dim
[PROOF STATE]
proof (chain)
picking this:
dim_row Gk = k
dim_row (Mk * Gsk) = k
dim_col Gk = n
dim_col (Mk * Gsk) = n
[PROOF STEP]
show "dim_row Gk = dim_row (Mk * Gsk)" "dim_col Gk = dim_col (Mk * Gsk)"
[PROOF STATE]
proof (prove)
using this:
dim_row Gk = k
dim_row (Mk * Gsk) = k
dim_col Gk = n
dim_col (Mk * Gsk) = n

goal (1 subgoal):
 1. dim_row Gk = dim_row (Mk * Gsk) &&& dim_col Gk = dim_col (Mk * Gsk)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row Gk = dim_row (Mk * Gsk)
dim_col Gk = dim_col (Mk * Gsk)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
assume "i < dim_row (Mk * Gsk)" "j < dim_col (Mk * Gsk)"
[PROOF STATE]
proof (state)
this:
i < dim_row (Mk * Gsk)
j < dim_col (Mk * Gsk)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
hence ij: "i < k" "j < n" and i: "i < m"
[PROOF STATE]
proof (prove)
using this:
i < dim_row (Mk * Gsk)
j < dim_col (Mk * Gsk)

goal (1 subgoal):
 1. (i < k &&& j < n) &&& i < length fs
[PROOF STEP]
using dim k
[PROOF STATE]
proof (prove)
using this:
i < dim_row (Mk * Gsk)
j < dim_col (Mk * Gsk)
dim_row Gk = k
dim_row (Mk * Gsk) = k
dim_col Gk = n
dim_col (Mk * Gsk) = n
k \<le> length fs

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have Gi: "fs ! i \<in> ?Rn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i \<in> carrier_vec n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. fs ! i \<in> carrier_vec n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "Gk $$ (i, j) = fs ! i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gk $$ (i, j) = fs ! i $ j
[PROOF STEP]
unfolding Gk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, y). fs ! i $ y) $$ (i, j) = fs ! i $ j
[PROOF STEP]
using ij k Gi
[PROOF STATE]
proof (prove)
using this:
i < k
j < n
k \<le> length fs
fs ! i \<in> carrier_vec n

goal (1 subgoal):
 1. mat k n (\<lambda>(i, y). fs ! i $ y) $$ (i, j) = fs ! i $ j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gk $$ (i, j) = fs ! i $ j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gk $$ (i, j) = fs ! i $ j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "... = FF $$ (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i $ j = mat_of_rows n fs $$ (i, j)
[PROOF STEP]
using ij i
[PROOF STATE]
proof (prove)
using this:
i < k
j < n
i < length fs

goal (1 subgoal):
 1. fs ! i $ j = mat_of_rows n fs $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i $ j = mat_of_rows n fs $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fs ! i $ j = mat_of_rows n fs $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "FF = (M m) * Fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])
[PROOF STEP]
by (rule matrix_equality)
[PROOF STATE]
proof (state)
this:
mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "\<dots> $$ (i,j) = row (M m) i \<bullet> col Fs j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j
[PROOF STEP]
by (rule index_mult_mat(1), insert i ij, auto simp: mat_of_rows_list_def)
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "row (M m) i = vec m (\<lambda> j. if j < k then Mk $$ (i,j) else 0)"
      (is "_ = vec m ?Mk")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (M (length fs)) i = vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a))
[PROOF STEP]
unfolding Mk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (M (length fs)) i = vec (length fs) (\<lambda>j. if j < k then mat k k (\<lambda>(x, y). \<mu> x y) $$ (i, j) else (0::'a))
[PROOF STEP]
using ij i
[PROOF STATE]
proof (prove)
using this:
i < k
j < n
i < length fs

goal (1 subgoal):
 1. row (M (length fs)) i = vec (length fs) (\<lambda>j. if j < k then mat k k (\<lambda>(x, y). \<mu> x y) $$ (i, j) else (0::'a))
[PROOF STEP]
by (auto simp: mat_of_rows_list_def \<mu>.simps)
[PROOF STATE]
proof (state)
this:
row (M (length fs)) i = vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row (M (length fs)) i = vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "col Fs j = vec m (\<lambda> i'. if i' < k then Gsk $$ (i',j) else (Fs $$ (i',j)))"
      (is "_ = vec m ?Gsk")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (mat_of_rows n (map gso [0..<length fs])) j = vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j))
[PROOF STEP]
unfolding Gsk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (mat_of_rows n (map gso [0..<length fs])) j = vec (length fs) (\<lambda>i'. if i' < k then mat k n (\<lambda>(i, y). gso i $ y) $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j))
[PROOF STEP]
using ij i
[PROOF STATE]
proof (prove)
using this:
i < k
j < n
i < length fs

goal (1 subgoal):
 1. col (mat_of_rows n (map gso [0..<length fs])) j = vec (length fs) (\<lambda>i'. if i' < k then mat k n (\<lambda>(i, y). gso i $ y) $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j))
[PROOF STEP]
by (auto simp: mat_of_rows_def)
[PROOF STATE]
proof (state)
this:
col (mat_of_rows n (map gso [0..<length fs])) j = vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (mat_of_rows n (map gso [0..<length fs])) j = vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "vec m ?Mk \<bullet> vec m ?Gsk = (\<Sum> i \<in> {0 ..< m}. ?Mk i * ?Gsk i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a)) \<bullet> vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j)) = (\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<dim_vec (vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j))). vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a)) $ ia * vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j)) $ ia) = (\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a)) \<bullet> vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j)) = (\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec (length fs) (\<lambda>j. if j < k then Mk $$ (i, j) else (0::'a)) \<bullet> vec (length fs) (\<lambda>i'. if i' < k then Gsk $$ (i', j) else mat_of_rows n (map gso [0..<length fs]) $$ (i', j)) = (\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "\<dots> = (\<Sum> i \<in> {0 ..< k} \<union> {k ..< m}. ?Mk i * ?Gsk i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>ia\<in>{0..<k} \<union> {k..<length fs}. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))
[PROOF STEP]
by (rule sum.cong, insert k, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>ia\<in>{0..<k} \<union> {k..<length fs}. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>ia\<in>{0..<k} \<union> {k..<length fs}. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "\<dots> = (\<Sum> i \<in> {0 ..< k}. ?Mk i * ?Gsk i) + (\<Sum> i \<in> {k ..< m}. ?Mk i * ?Gsk i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{0..<k} \<union> {k..<length fs}. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>ia = 0..<k. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) + (\<Sum>ia = k..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))
[PROOF STEP]
by (rule sum.union_disjoint, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia\<in>{0..<k} \<union> {k..<length fs}. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>ia = 0..<k. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) + (\<Sum>ia = k..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia\<in>{0..<k} \<union> {k..<length fs}. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>ia = 0..<k. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) + (\<Sum>ia = k..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "(\<Sum> i \<in> {k ..< m}. ?Mk i * ?Gsk i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = k..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (0::'a)
[PROOF STEP]
by (rule sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = k..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (0::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = k..<length fs. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (0::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "(\<Sum> i \<in> {0 ..< k}. ?Mk i * ?Gsk i) = (\<Sum> i' \<in> {0 ..< k}. Mk $$ (i,i') * Gsk $$ (i',j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<k. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<k. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<k. (if ia < k then Mk $$ (i, ia) else (0::'a)) * (if ia < k then Gsk $$ (ia, j) else mat_of_rows n (map gso [0..<length fs]) $$ (ia, j))) = (\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "\<dots> = row Mk i \<bullet> col Gsk j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j)) = row Mk i \<bullet> col Gsk j
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j)) = (\<Sum>ia = 0..<dim_vec (col Gsk j). row Mk i $ ia * col Gsk j $ ia)
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i < k
j < n

goal (1 subgoal):
 1. (\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j)) = (\<Sum>ia = 0..<dim_vec (col Gsk j). row Mk i $ ia * col Gsk j $ ia)
[PROOF STEP]
by (auto simp: Gsk_def Mk_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j)) = row Mk i \<bullet> col Gsk j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i' = 0..<k. Mk $$ (i, i') * Gsk $$ (i', j)) = row Mk i \<bullet> col Gsk j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
have "\<dots> = (Mk * Gsk) $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row Mk i \<bullet> col Gsk j = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
using ij Mk Gsk
[PROOF STATE]
proof (prove)
using this:
i < k
j < n
Mk \<in> carrier_mat k k
Gsk \<in> carrier_mat k n

goal (1 subgoal):
 1. row Mk i \<bullet> col Gsk j = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
row Mk i \<bullet> col Gsk j = (Mk * Gsk) $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Mk * Gsk); j < dim_col (Mk * Gsk)\<rbrakk> \<Longrightarrow> Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Gk $$ (i, j) = (Mk * Gsk) $$ (i, j) + (0::'a)
[PROOF STEP]
show "Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
Gk $$ (i, j) = (Mk * Gsk) $$ (i, j) + (0::'a)

goal (1 subgoal):
 1. Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gk = Mk * Gsk

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs 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 (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "Gramian_determinant fs k = det (Gk * Gk\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs k = det (Gk * Gk\<^sup>T)
[PROOF STEP]
unfolding Gramian_determinant_def Gramian_matrix_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat k n (\<lambda>(i, y). fs ! i $ y) * (mat k n (\<lambda>(i, y). fs ! i $ y))\<^sup>T) = det (Gk * Gk\<^sup>T)
[PROOF STEP]
by (rule arg_cong[of _ _ det], rule cong, insert k, auto simp: Gk_def)
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs k = det (Gk * Gk\<^sup>T)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs k = det (Gk * Gk\<^sup>T)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "Gk\<^sup>T = Gsk\<^sup>T * Mk\<^sup>T" (is "_ = ?TGsk * ?TMk")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gk\<^sup>T = Gsk\<^sup>T * Mk\<^sup>T
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Mk * Gsk)\<^sup>T = Gsk\<^sup>T * Mk\<^sup>T
[PROOF STEP]
by (rule transpose_mult[OF Mk Gsk])
[PROOF STATE]
proof (state)
this:
Gk\<^sup>T = Gsk\<^sup>T * Mk\<^sup>T

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gk\<^sup>T = Gsk\<^sup>T * Mk\<^sup>T

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "Gk = Mk * Gsk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gk = Mk * Gsk
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Gk = Mk * Gsk

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gk = Mk * Gsk

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "\<dots> * (?TGsk * ?TMk) = Mk * (Gsk * (?TGsk * ?TMk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mk * Gsk * (Gsk\<^sup>T * Mk\<^sup>T) = Mk * (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))
[PROOF STEP]
by (rule assoc_mult_mat[OF Mk Gsk, of _ k], insert Gsk Mk, auto)
[PROOF STATE]
proof (state)
this:
Mk * Gsk * (Gsk\<^sup>T * Mk\<^sup>T) = Mk * (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Mk * Gsk * (Gsk\<^sup>T * Mk\<^sup>T) = Mk * (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "det \<dots> = det Mk * det (Gsk * (?TGsk * ?TMk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Mk * (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))) = det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))
[PROOF STEP]
by (rule det_mult[OF Mk], insert Gsk Mk, auto)
[PROOF STATE]
proof (state)
this:
det (Mk * (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))) = det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Mk * (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))) = det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "\<dots> = det (Gsk * (?TGsk * ?TMk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T)) = det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))
[PROOF STEP]
using detMk
[PROOF STATE]
proof (prove)
using this:
det Mk = (1::'a)

goal (1 subgoal):
 1. det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T)) = det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T)) = det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det Mk * det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T)) = det (Gsk * (Gsk\<^sup>T * Mk\<^sup>T))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "Gsk * (?TGsk * ?TMk) = (Gsk * ?TGsk) * ?TMk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gsk * (Gsk\<^sup>T * Mk\<^sup>T) = Gsk * Gsk\<^sup>T * Mk\<^sup>T
[PROOF STEP]
by (rule assoc_mult_mat[symmetric, OF Gsk], insert Gsk Mk, auto)
[PROOF STATE]
proof (state)
this:
Gsk * (Gsk\<^sup>T * Mk\<^sup>T) = Gsk * Gsk\<^sup>T * Mk\<^sup>T

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gsk * (Gsk\<^sup>T * Mk\<^sup>T) = Gsk * Gsk\<^sup>T * Mk\<^sup>T

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "det \<dots> = det (Gsk * ?TGsk) * det ?TMk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gsk * Gsk\<^sup>T * Mk\<^sup>T) = det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T
[PROOF STEP]
by (rule det_mult, insert Gsk Mk, auto)
[PROOF STATE]
proof (state)
this:
det (Gsk * Gsk\<^sup>T * Mk\<^sup>T) = det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Gsk * Gsk\<^sup>T * Mk\<^sup>T) = det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "\<dots> = det (Gsk * ?TGsk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T = det (Gsk * Gsk\<^sup>T)
[PROOF STEP]
using detMk det_transpose[OF Mk]
[PROOF STATE]
proof (prove)
using this:
det Mk = (1::'a)
det Mk\<^sup>T = det Mk

goal (1 subgoal):
 1. det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T = det (Gsk * Gsk\<^sup>T)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T = det (Gsk * Gsk\<^sup>T)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Gsk * Gsk\<^sup>T) * det Mk\<^sup>T = det (Gsk * Gsk\<^sup>T)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "Gsk * ?TGsk = mat k k (\<lambda> (i,j). if i = j then sq_norm (gso j) else 0)" (is "_ = ?M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gsk * Gsk\<^sup>T = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
proof (rule eq_matI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
 2. dim_row (Gsk * Gsk\<^sup>T) = dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
 3. dim_col (Gsk * Gsk\<^sup>T) = dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
[PROOF STEP]
show "dim_row (Gsk * ?TGsk) = dim_row ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (Gsk * Gsk\<^sup>T) = dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
[PROOF STEP]
unfolding Gsk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat k n (\<lambda>(i, y). gso i $ y) * (mat k n (\<lambda>(i, y). gso i $ y))\<^sup>T) = dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row (Gsk * Gsk\<^sup>T) = dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
 2. dim_col (Gsk * Gsk\<^sup>T) = dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
[PROOF STEP]
show "dim_col (Gsk * ?TGsk) = dim_col ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (Gsk * Gsk\<^sup>T) = dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
[PROOF STEP]
unfolding Gsk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (mat k n (\<lambda>(i, y). gso i $ y) * (mat k n (\<lambda>(i, y). gso i $ y))\<^sup>T) = dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_col (Gsk * Gsk\<^sup>T) = dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
assume "i < dim_row ?M" "j < dim_col ?M"
[PROOF STATE]
proof (state)
this:
i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
hence ij: "i < k" "j < k" and ijn: "i < m" "j < m"
[PROOF STATE]
proof (prove)
using this:
i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))

goal (1 subgoal):
 1. (i < k &&& j < k) &&& i < length fs &&& j < length fs
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))
k \<le> length fs

goal (1 subgoal):
 1. (i < k &&& j < k) &&& i < length fs &&& j < length fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < k
j < k
i < length fs
j < length fs

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i < k
j < k
i < length fs
j < length fs

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
assume "i < k"
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
hence "i < m"
[PROOF STATE]
proof (prove)
using this:
i < k

goal (1 subgoal):
 1. i < length fs
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
i < k
k \<le> length fs

goal (1 subgoal):
 1. i < length fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length fs

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
hence Gs: "gso i \<in> ?Rn"
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. gso i \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gso i \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
have "row Gsk i = gso i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row Gsk i = gso i
[PROOF STEP]
unfolding row_def Gsk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (dim_col (mat k n (\<lambda>(i, y). gso i $ y))) (\<lambda>j. mat k n (\<lambda>(i, y). gso i $ y) $$ (i, j)) = gso i
[PROOF STEP]
by (rule eq_vecI, insert Gs \<open>i < k\<close>, auto)
[PROOF STATE]
proof (state)
this:
row Gsk i = gso i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?ia5 < k \<Longrightarrow> row Gsk ?ia5 = gso ?ia5

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
note row = this
[PROOF STATE]
proof (state)
this:
?ia5 < k \<Longrightarrow> row Gsk ?ia5 = gso ?ia5

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
have "(Gsk * ?TGsk) $$ (i,j) = row Gsk i \<bullet> row Gsk j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gsk * Gsk\<^sup>T) $$ (i, j) = row Gsk i \<bullet> row Gsk j
[PROOF STEP]
using ij Gsk
[PROOF STATE]
proof (prove)
using this:
i < k
j < k
Gsk \<in> carrier_mat k n

goal (1 subgoal):
 1. (Gsk * Gsk\<^sup>T) $$ (i, j) = row Gsk i \<bullet> row Gsk j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Gsk * Gsk\<^sup>T) $$ (i, j) = row Gsk i \<bullet> row Gsk j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Gsk * Gsk\<^sup>T) $$ (i, j) = row Gsk i \<bullet> row Gsk j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
have "\<dots> = gso i \<bullet> gso j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row Gsk i \<bullet> row Gsk j = gso i \<bullet> gso j
[PROOF STEP]
using row ij
[PROOF STATE]
proof (prove)
using this:
?ia5 < k \<Longrightarrow> row Gsk ?ia5 = gso ?ia5
i < k
j < k

goal (1 subgoal):
 1. row Gsk i \<bullet> row Gsk j = gso i \<bullet> gso j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
row Gsk i \<bullet> row Gsk j = gso i \<bullet> gso j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row Gsk i \<bullet> row Gsk j = gso i \<bullet> gso j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
have "\<dots> = (if i = j then sq_norm (gso j) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
 2. i \<noteq> j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
 2. i \<noteq> j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
from \<open>i \<noteq> j\<close> orthogonalD[OF orthogonal_gso] ijn assms
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> j
\<lbrakk>?i < length (map gso [0..<length fs]); ?j < length (map gso [0..<length fs])\<rbrakk> \<Longrightarrow> (map gso [0..<length fs] ! ?i \<bullet> map gso [0..<length fs] ! ?j = (0::'a)) = (?i \<noteq> ?j)
i < length fs
j < length fs
k \<le> length fs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
\<lbrakk>?i < length (map gso [0..<length fs]); ?j < length (map gso [0..<length fs])\<rbrakk> \<Longrightarrow> (map gso [0..<length fs] ! ?i \<bullet> map gso [0..<length fs] ! ?j = (0::'a)) = (?i \<noteq> ?j)
i < length fs
j < length fs
k \<le> length fs

goal (1 subgoal):
 1. gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso i \<bullet> gso j = (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
have "\<dots> = ?M $$ (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i < k
j < k

goal (1 subgoal):
 1. (if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))); j < dim_col (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))\<rbrakk> \<Longrightarrow> (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
show "(Gsk * ?TGsk) $$ (i,j) = ?M $$ (i,j)"
[PROOF STATE]
proof (prove)
using this:
(Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)

goal (1 subgoal):
 1. (Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(Gsk * Gsk\<^sup>T) $$ (i, j) = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gsk * Gsk\<^sup>T = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gsk * Gsk\<^sup>T = mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "det ?M = prod_list (diag_mat ?M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))) = prod_list (diag_mat (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))))
[PROOF STEP]
by (rule det_upper_triangular, auto)
[PROOF STATE]
proof (state)
this:
det (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))) = prod_list (diag_mat (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))) = prod_list (diag_mat (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))))

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "diag_mat ?M = map (\<lambda> j. sq_norm (gso j)) [0 ..< k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diag_mat (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))) = map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<k]
[PROOF STEP]
unfolding diag_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)) $$ (i, i)) [0..<dim_row (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a)))] = map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
diag_mat (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))) = map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<k]

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
diag_mat (mat k k (\<lambda>(i, j). if i = j then \<parallel>gso j\<parallel>\<^sup>2 else (0::'a))) = map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<k]

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "prod_list \<dots> = (\<Prod> j < k. sq_norm (gso j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j\<leftarrow>[0..<k]. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
[PROOF STEP]
by (subst prod.distinct_set_conv_list[symmetric], force, rule prod.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Prod>j\<leftarrow>[0..<k]. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)

goal (2 subgoals):
 1. Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
 2. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
[PROOF STEP]
show "Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)

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

goal (1 subgoal):
 1. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs k = (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)

goal (1 subgoal):
 1. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
have "\<dots> > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)
[PROOF STEP]
by (rule prod_pos, intro ballI sq_norm_pos, insert k assms, auto)
[PROOF STATE]
proof (state)
this:
(0::'a) < (\<Prod>j<k. \<parallel>gso j\<parallel>\<^sup>2)

goal (1 subgoal):
 1. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < Gramian_determinant fs k
[PROOF STEP]
show "0 < Gramian_determinant fs k"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < Gramian_determinant fs k

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gramian_determinant_div:
  assumes "l < m"
  shows "Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
note gram = Gramian_determinant(1)[symmetric]
[PROOF STATE]
proof (state)
this:
?k \<le> length fs \<Longrightarrow> (\<Prod>j<?k. \<parallel>gso j\<parallel>\<^sup>2) = Gramian_determinant fs ?k

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
l < length fs
[PROOF STEP]
have le: "Suc l \<le> m" "l \<le> m"
[PROOF STATE]
proof (prove)
using this:
l < length fs

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

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
have "(\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j \<in> {0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < length fs

goal (1 subgoal):
 1. (\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2)
[PROOF STEP]
by (intro prod.cong) (auto)
[PROOF STATE]
proof (state)
this:
(\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2)

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2)

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (\<Prod>j<l. \<parallel>gso j\<parallel>\<^sup>2) * \<parallel>gso l\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<l. \<parallel>gso j\<parallel>\<^sup>2) * \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < length fs

goal (1 subgoal):
 1. (\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<l. \<parallel>gso j\<parallel>\<^sup>2) * \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
by (subst prod_Un) (auto simp add: atLeast0LessThan)
[PROOF STATE]
proof (state)
this:
(\<Prod>j\<in>{0..<l} \<union> {l}. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<l. \<parallel>gso j\<parallel>\<^sup>2) * \<parallel>gso l\<parallel>\<^sup>2

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<l. \<parallel>gso j\<parallel>\<^sup>2) * \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j<Suc l. \<parallel>gso j\<parallel>\<^sup>2) = (\<Prod>j<l. \<parallel>gso j\<parallel>\<^sup>2) * \<parallel>gso l\<parallel>\<^sup>2

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
unfolding gram[OF le(1)] gram[OF le(2)]
[PROOF STATE]
proof (prove)
using this:
Gramian_determinant fs (Suc l) = Gramian_determinant fs l * \<parallel>gso l\<parallel>\<^sup>2

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
using Gramian_determinant(2)[OF le(2)] assms
[PROOF STATE]
proof (prove)
using this:
Gramian_determinant fs (Suc l) = Gramian_determinant fs l * \<parallel>gso l\<parallel>\<^sup>2
(0::'a) < Gramian_determinant fs l
l < length fs

goal (1 subgoal):
 1. Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs (Suc l) / Gramian_determinant fs l = \<parallel>gso l\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gram_schmidt_fs_Rn) Gramian_determinant_Ints:
  assumes "k \<le> m" "\<And>i j. i < n \<Longrightarrow> j < m \<Longrightarrow> fs ! j $ i \<in> \<int>"
  shows "Gramian_determinant fs k \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
let ?oi = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
k \<le> length fs
\<lbrakk>?i1 < n; ?j1 < length fs\<rbrakk> \<Longrightarrow> fs ! ?j1 $ ?i1 \<in> \<int>
[PROOF STEP]
have "\<And> i. i < n \<Longrightarrow> \<forall>j. \<exists> c. j < m \<longrightarrow> fs ! j $ i = ?oi c"
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs
\<lbrakk>?i1 < n; ?j1 < length fs\<rbrakk> \<Longrightarrow> fs ! ?j1 $ ?i1 \<in> \<int>

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<forall>j. \<exists>c. j < length fs \<longrightarrow> fs ! j $ i = of_int c
[PROOF STEP]
unfolding Ints_def
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs
\<lbrakk>?i1 < n; ?j1 < length fs\<rbrakk> \<Longrightarrow> fs ! ?j1 $ ?i1 \<in> range of_int

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<forall>j. \<exists>c. j < length fs \<longrightarrow> fs ! j $ i = of_int c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < n \<Longrightarrow> \<forall>j. \<exists>c. j < length fs \<longrightarrow> fs ! j $ ?i1 = of_int c

goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
?i2 < n \<Longrightarrow> \<exists>f. \<forall>x<length fs. fs ! x $ ?i2 = of_int (f x)
[PROOF STEP]
have "\<forall> i. \<exists> c. \<forall> j. i < n \<longrightarrow> j < m \<longrightarrow> fs ! j $ i = ?oi (c j)"
[PROOF STATE]
proof (prove)
using this:
?i2 < n \<Longrightarrow> \<exists>f. \<forall>x<length fs. fs ! x $ ?i2 = of_int (f x)

goal (1 subgoal):
 1. \<forall>i. \<exists>c. \<forall>j. i < n \<longrightarrow> j < length fs \<longrightarrow> fs ! j $ i = of_int (c j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>c. \<forall>j. i < n \<longrightarrow> j < length fs \<longrightarrow> fs ! j $ i = of_int (c j)

goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x j. x < n \<longrightarrow> j < length fs \<longrightarrow> fs ! j $ x = of_int (f x j)
[PROOF STEP]
obtain c where c: "\<And> i j. i < n \<Longrightarrow> j < m \<Longrightarrow> fs ! j $ i = ?oi (c i j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x j. x < n \<longrightarrow> j < length fs \<longrightarrow> fs ! j $ x = of_int (f x j)

goal (1 subgoal):
 1. (\<And>c. (\<And>i j. \<lbrakk>i < n; j < length fs\<rbrakk> \<Longrightarrow> fs ! j $ i = of_int (c i j)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 < n; ?j1 < length fs\<rbrakk> \<Longrightarrow> fs ! ?j1 $ ?i1 = of_int (c ?i1 ?j1)

goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
define d where "d = map (\<lambda> j. vec n (\<lambda> i. c i j)) [0..<m]"
[PROOF STATE]
proof (state)
this:
d = map (\<lambda>j. vec n (\<lambda>i. c i j)) [0..<length fs]

goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
have fs: "fs = map (map_vec ?oi) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs = map of_int_hom.vec_hom d
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs = map of_int_hom.vec_hom (map (\<lambda>j. vec n (\<lambda>i. c i j)) [0..<length fs])
[PROOF STEP]
by (rule nth_equalityI, auto intro!: eq_vecI c)
[PROOF STATE]
proof (state)
this:
fs = map of_int_hom.vec_hom d

goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
have id: "mat k n (\<lambda>(i, y). map (map_vec ?oi) d ! i $ y) = map_mat of_int (mat k n (\<lambda>(i, y). d ! i $ y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat k n (\<lambda>(i, y). map of_int_hom.vec_hom d ! i $ y) = of_int_hom.mat_hom (mat k n (\<lambda>(i, y). d ! i $ y))
[PROOF STEP]
by (rule eq_matI, insert \<open>k \<le> m\<close>, auto simp: d_def o_def)
[PROOF STATE]
proof (state)
this:
mat k n (\<lambda>(i, y). map of_int_hom.vec_hom d ! i $ y) = of_int_hom.mat_hom (mat k n (\<lambda>(i, y). d ! i $ y))

goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
unfolding fs Gramian_determinant_def Gramian_matrix_def Let_def id
    map_mat_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (of_int_hom.mat_hom (mat k n (\<lambda>(i, y). d ! i $ y)) * of_int_hom.mat_hom (mat k n (\<lambda>(i, y). d ! i $ y))\<^sup>T) \<in> \<int>
[PROOF STEP]
by (subst of_int_hom.mat_hom_mult[symmetric], auto)
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs k \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gramian_determinant_ge1:
  assumes "k \<le> m"
  shows "1 \<le> Gramian_determinant fs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> Gramian_determinant fs k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) \<le> Gramian_determinant fs k
[PROOF STEP]
have "0 < Gramian_determinant fs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < Gramian_determinant fs k
[PROOF STEP]
by (simp add: assms Gramian_determinant(2) less_or_eq_imp_le)
[PROOF STATE]
proof (state)
this:
(0::'a) < Gramian_determinant fs k

goal (1 subgoal):
 1. (1::'a) \<le> Gramian_determinant fs k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0::'a) < Gramian_determinant fs k

goal (1 subgoal):
 1. (1::'a) \<le> Gramian_determinant fs k
[PROOF STEP]
have "Gramian_determinant fs k \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
by (simp add: Gramian_determinant_Ints assms fs_int)
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs k \<in> \<int>

goal (1 subgoal):
 1. (1::'a) \<le> Gramian_determinant fs k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < Gramian_determinant fs k
Gramian_determinant fs k \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) < Gramian_determinant fs k
Gramian_determinant fs k \<in> \<int>

goal (1 subgoal):
 1. (1::'a) \<le> Gramian_determinant fs k
[PROOF STEP]
using Ints_nonzero_abs_ge1
[PROOF STATE]
proof (prove)
using this:
(0::'a) < Gramian_determinant fs k
Gramian_determinant fs k \<in> \<int>
\<lbrakk>?x \<in> \<int>; ?x \<noteq> (0::?'a)\<rbrakk> \<Longrightarrow> (1::?'a) \<le> \<bar>?x\<bar>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mu_bound_Gramian_determinant:
  assumes "l < k" "k < m"
  shows "(\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
have "(\<mu> k l)\<^sup>2  = (fs ! k \<bullet> gso l)\<^sup>2 / (\<parallel>gso l\<parallel>\<^sup>2)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 = (fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
k < length fs

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 = (fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2
[PROOF STEP]
by (simp add: power_divide \<mu>.simps)
[PROOF STATE]
proof (state)
this:
(\<mu> k l)\<^sup>2 = (fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<mu> k l)\<^sup>2 = (fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<le> (\<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2) / (\<parallel>gso l\<parallel>\<^sup>2)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 \<le> \<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
k < length fs

goal (1 subgoal):
 1. (fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 \<le> \<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2
[PROOF STEP]
by (auto intro!: scalar_prod_Cauchy divide_right_mono)
[PROOF STATE]
proof (state)
this:
(fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 \<le> \<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(fs ! k \<bullet> gso l)\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 \<le> \<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = \<parallel>fs ! k\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 = \<parallel>fs ! k\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2
[PROOF STEP]
by (auto simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 = \<parallel>fs ! k\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! k\<parallel>\<^sup>2 * \<parallel>gso l\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2\<^sup>2 = \<parallel>fs ! k\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> =  \<parallel>fs ! k\<parallel>\<^sup>2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>fs ! k\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2 = \<parallel>fs ! k\<parallel>\<^sup>2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
k < length fs

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

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! k\<parallel>\<^sup>2 / \<parallel>gso l\<parallel>\<^sup>2 = \<parallel>fs ! k\<parallel>\<^sup>2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l)

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> =  Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / Gramian_determinant fs (Suc l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>fs ! k\<parallel>\<^sup>2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l) = Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / Gramian_determinant fs (Suc l)
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! k\<parallel>\<^sup>2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l) = Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / Gramian_determinant fs (Suc l)

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! k\<parallel>\<^sup>2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l) = Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / Gramian_determinant fs (Suc l)

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / Gramian_determinant fs (Suc l) \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / (1::'a)
[PROOF STEP]
by (rule divide_left_mono, insert Gramian_determinant_ge1[of l] Gramian_determinant_ge1[of "Suc l"] assms,
    auto intro!: mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / Gramian_determinant fs (Suc l) \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / (1::'a)

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2 / (1::'a)

goal (1 subgoal):
 1. (\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<mu> k l)\<^sup>2 \<le> Gramian_determinant fs l * \<parallel>fs ! k\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_cong:
  fixes f1 f2 :: "'a vec list"
  assumes "\<And> i. i \<le> x \<Longrightarrow> f1 ! i = f2 ! i"
  shows "gram_schmidt_fs.gso n f1 x = gram_schmidt_fs.gso n f2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_fs.gso n f1 x = gram_schmidt_fs.gso n f2 x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i3 \<le> x \<Longrightarrow> f1 ! ?i3 = f2 ! ?i3

goal (1 subgoal):
 1. gram_schmidt_fs.gso n f1 x = gram_schmidt_fs.gso n f2 x
[PROOF STEP]
proof(induct x rule:nat_less_induct[rule_format])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>m. \<lbrakk>m < na; \<And>i. i \<le> m \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> gram_schmidt_fs.gso n f1 m = gram_schmidt_fs.gso n f2 m; \<And>i. i \<le> na \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> gram_schmidt_fs.gso n f1 na = gram_schmidt_fs.gso n f2 na
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m3 < x; \<And>i. i \<le> ?m3 \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> gram_schmidt_fs.gso n f1 ?m3 = gram_schmidt_fs.gso n f2 ?m3
?i3 \<le> x \<Longrightarrow> f1 ! ?i3 = f2 ! ?i3

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>m. \<lbrakk>m < na; \<And>i. i \<le> m \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> gram_schmidt_fs.gso n f1 m = gram_schmidt_fs.gso n f2 m; \<And>i. i \<le> na \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> gram_schmidt_fs.gso n f1 na = gram_schmidt_fs.gso n f2 na
[PROOF STEP]
interpret f1: gram_schmidt_fs n f1
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>m. \<lbrakk>m < na; \<And>i. i \<le> m \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso m = gram_schmidt_fs.gso n f2 m; \<And>i. i \<le> na \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso na = gram_schmidt_fs.gso n f2 na
[PROOF STEP]
interpret f2: gram_schmidt_fs n f2
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<And>m. \<lbrakk>m < n; \<And>i. i \<le> m \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso m = f2.gso m; \<And>i. i \<le> n \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso n = f2.gso n
[PROOF STEP]
have *: "map (\<lambda>j. - f1.\<mu> x j \<cdot>\<^sub>v f1.gso j) [0..<x] = map (\<lambda>j. - f2.\<mu> x j \<cdot>\<^sub>v f2.gso j) [0..<x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>j. - f1.\<mu> x j \<cdot>\<^sub>v f1.gso j) [0..<x] = map (\<lambda>j. - f2.\<mu> x j \<cdot>\<^sub>v f2.gso j) [0..<x]
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?m3 < x; \<And>i. i \<le> ?m3 \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso ?m3 = f2.gso ?m3
?i3 \<le> x \<Longrightarrow> f1 ! ?i3 = f2 ! ?i3

goal (1 subgoal):
 1. map (\<lambda>j. - f1.\<mu> x j \<cdot>\<^sub>v f1.gso j) [0..<x] = map (\<lambda>j. - f2.\<mu> x j \<cdot>\<^sub>v f2.gso j) [0..<x]
[PROOF STEP]
by (intro map_cong) (auto simp add: f1.\<mu>.simps f2.\<mu>.simps)
[PROOF STATE]
proof (state)
this:
map (\<lambda>j. - f1.\<mu> x j \<cdot>\<^sub>v f1.gso j) [0..<x] = map (\<lambda>j. - f2.\<mu> x j \<cdot>\<^sub>v f2.gso j) [0..<x]

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<And>m. \<lbrakk>m < n; \<And>i. i \<le> m \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso m = f2.gso m; \<And>i. i \<le> n \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso n = f2.gso n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1.gso x = f2.gso x
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?m3 < x; \<And>i. i \<le> ?m3 \<Longrightarrow> f1 ! i = f2 ! i\<rbrakk> \<Longrightarrow> f1.gso ?m3 = f2.gso ?m3
?i3 \<le> x \<Longrightarrow> f1 ! ?i3 = f2 ! ?i3

goal (1 subgoal):
 1. f1.gso x = f2.gso x
[PROOF STEP]
by (subst f1.gso.simps, subst f2.gso.simps, subst *) auto
[PROOF STATE]
proof (state)
this:
f1.gso x = f2.gso x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<mu>_cong:
  fixes f1 f2 :: "'a vec list"
  assumes "\<And> k. j < i \<Longrightarrow> k \<le> j \<Longrightarrow> f1 ! k = f2 ! k"
    and "j < i \<Longrightarrow> f1 ! i = f2 ! i"
  shows "gram_schmidt_fs.\<mu> n f1 i j = gram_schmidt_fs.\<mu> n f2 i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_fs.\<mu> n f1 i j = gram_schmidt_fs.\<mu> n f2 i j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gram_schmidt_fs.\<mu> n f1 i j = gram_schmidt_fs.\<mu> n f2 i j
[PROOF STEP]
interpret f1: gram_schmidt_fs n f1
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f1.\<mu> i j = gram_schmidt_fs.\<mu> n f2 i j
[PROOF STEP]
interpret f2: gram_schmidt_fs n f2
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f1.\<mu> i j = f2.\<mu> i j
[PROOF STEP]
from gso_cong[of j f1 f2] assms
[PROOF STATE]
proof (chain)
picking this:
(\<And>i. i \<le> j \<Longrightarrow> f1 ! i = f2 ! i) \<Longrightarrow> f1.gso j = f2.gso j
\<lbrakk>j < i; ?k3 \<le> j\<rbrakk> \<Longrightarrow> f1 ! ?k3 = f2 ! ?k3
j < i \<Longrightarrow> f1 ! i = f2 ! i
[PROOF STEP]
have id: "j < i \<Longrightarrow> f1.gso j = f2.gso j"
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<le> j \<Longrightarrow> f1 ! i = f2 ! i) \<Longrightarrow> f1.gso j = f2.gso j
\<lbrakk>j < i; ?k3 \<le> j\<rbrakk> \<Longrightarrow> f1 ! ?k3 = f2 ! ?k3
j < i \<Longrightarrow> f1 ! i = f2 ! i

goal (1 subgoal):
 1. j < i \<Longrightarrow> f1.gso j = f2.gso j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> f1.gso j = f2.gso j

goal (1 subgoal):
 1. f1.\<mu> i j = f2.\<mu> i j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1.\<mu> i j = f2.\<mu> i j
[PROOF STEP]
unfolding f1.\<mu>.simps f2.\<mu>.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if j < i then f1 ! i \<bullet> f1.gso j / \<parallel>f1.gso j\<parallel>\<^sup>2 else if i = j then 1::'a else (0::'a)) = (if j < i then f2 ! i \<bullet> f2.gso j / \<parallel>f2.gso j\<parallel>\<^sup>2 else if i = j then 1::'a else (0::'a))
[PROOF STEP]
using assms id
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>j < i; ?k3 \<le> j\<rbrakk> \<Longrightarrow> f1 ! ?k3 = f2 ! ?k3
j < i \<Longrightarrow> f1 ! i = f2 ! i
j < i \<Longrightarrow> f1.gso j = f2.gso j

goal (1 subgoal):
 1. (if j < i then f1 ! i \<bullet> f1.gso j / \<parallel>f1.gso j\<parallel>\<^sup>2 else if i = j then 1::'a else (0::'a)) = (if j < i then f2 ! i \<bullet> f2.gso j / \<parallel>f2.gso j\<parallel>\<^sup>2 else if i = j then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1.\<mu> i j = f2.\<mu> i j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_list_le_mono: fixes us :: "'a :: {linordered_nonzero_semiring,ordered_ring} list"
  assumes "length us = length vs"
  and "\<And> i. i < length vs \<Longrightarrow> 0 \<le> us ! i \<and> us ! i \<le> vs ! i"
shows "0 \<le> prod_list us \<and> prod_list us \<le> prod_list vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length us = length vs
?i < length vs \<Longrightarrow> (0::'a) \<le> us ! ?i \<and> us ! ?i \<le> vs ! ?i

goal (1 subgoal):
 1. (0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs
[PROOF STEP]
proof (induction us vs rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>i. i < length [] \<Longrightarrow> (0::'a) \<le> [] ! i \<and> [] ! i \<le> [] ! i) \<Longrightarrow> (0::'a) \<le> prod_list [] \<and> prod_list [] \<le> prod_list []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; (\<And>i. i < length ys \<Longrightarrow> (0::'a) \<le> xs ! i \<and> xs ! i \<le> ys ! i) \<Longrightarrow> (0::'a) \<le> prod_list xs \<and> prod_list xs \<le> prod_list ys; \<And>i. i < length (y # ys) \<Longrightarrow> (0::'a) \<le> (x # xs) ! i \<and> (x # xs) ! i \<le> (y # ys) ! i\<rbrakk> \<Longrightarrow> (0::'a) \<le> prod_list (x # xs) \<and> prod_list (x # xs) \<le> prod_list (y # ys)
[PROOF STEP]
case (Cons u us v vs)
[PROOF STATE]
proof (state)
this:
length us = length vs
(\<And>i. i < length vs \<Longrightarrow> (0::'a) \<le> us ! i \<and> us ! i \<le> vs ! i) \<Longrightarrow> (0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs
?i < length (v # vs) \<Longrightarrow> (0::'a) \<le> (u # us) ! ?i \<and> (u # us) ! ?i \<le> (v # vs) ! ?i

goal (2 subgoals):
 1. (\<And>i. i < length [] \<Longrightarrow> (0::'a) \<le> [] ! i \<and> [] ! i \<le> [] ! i) \<Longrightarrow> (0::'a) \<le> prod_list [] \<and> prod_list [] \<le> prod_list []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; (\<And>i. i < length ys \<Longrightarrow> (0::'a) \<le> xs ! i \<and> xs ! i \<le> ys ! i) \<Longrightarrow> (0::'a) \<le> prod_list xs \<and> prod_list xs \<le> prod_list ys; \<And>i. i < length (y # ys) \<Longrightarrow> (0::'a) \<le> (x # xs) ! i \<and> (x # xs) ! i \<le> (y # ys) ! i\<rbrakk> \<Longrightarrow> (0::'a) \<le> prod_list (x # xs) \<and> prod_list (x # xs) \<le> prod_list (y # ys)
[PROOF STEP]
have "0 \<le> prod_list us \<and> prod_list us \<le> prod_list vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs
[PROOF STEP]
by (rule Cons.IH, insert Cons.prems[of "Suc i" for i], auto)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs

goal (2 subgoals):
 1. (\<And>i. i < length [] \<Longrightarrow> (0::'a) \<le> [] ! i \<and> [] ! i \<le> [] ! i) \<Longrightarrow> (0::'a) \<le> prod_list [] \<and> prod_list [] \<le> prod_list []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; (\<And>i. i < length ys \<Longrightarrow> (0::'a) \<le> xs ! i \<and> xs ! i \<le> ys ! i) \<Longrightarrow> (0::'a) \<le> prod_list xs \<and> prod_list xs \<le> prod_list ys; \<And>i. i < length (y # ys) \<Longrightarrow> (0::'a) \<le> (x # xs) ! i \<and> (x # xs) ! i \<le> (y # ys) ! i\<rbrakk> \<Longrightarrow> (0::'a) \<le> prod_list (x # xs) \<and> prod_list (x # xs) \<le> prod_list (y # ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs

goal (2 subgoals):
 1. (\<And>i. i < length [] \<Longrightarrow> (0::'a) \<le> [] ! i \<and> [] ! i \<le> [] ! i) \<Longrightarrow> (0::'a) \<le> prod_list [] \<and> prod_list [] \<le> prod_list []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; (\<And>i. i < length ys \<Longrightarrow> (0::'a) \<le> xs ! i \<and> xs ! i \<le> ys ! i) \<Longrightarrow> (0::'a) \<le> prod_list xs \<and> prod_list xs \<le> prod_list ys; \<And>i. i < length (y # ys) \<Longrightarrow> (0::'a) \<le> (x # xs) ! i \<and> (x # xs) ! i \<le> (y # ys) ! i\<rbrakk> \<Longrightarrow> (0::'a) \<le> prod_list (x # xs) \<and> prod_list (x # xs) \<le> prod_list (y # ys)
[PROOF STEP]
have "0 \<le> u \<and> u \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> u \<and> u \<le> v
[PROOF STEP]
using Cons.prems[of 0]
[PROOF STATE]
proof (prove)
using this:
0 < length (v # vs) \<Longrightarrow> (0::'a) \<le> (u # us) ! 0 \<and> (u # us) ! 0 \<le> (v # vs) ! 0

goal (1 subgoal):
 1. (0::'a) \<le> u \<and> u \<le> v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> u \<and> u \<le> v

goal (2 subgoals):
 1. (\<And>i. i < length [] \<Longrightarrow> (0::'a) \<le> [] ! i \<and> [] ! i \<le> [] ! i) \<Longrightarrow> (0::'a) \<le> prod_list [] \<and> prod_list [] \<le> prod_list []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; (\<And>i. i < length ys \<Longrightarrow> (0::'a) \<le> xs ! i \<and> xs ! i \<le> ys ! i) \<Longrightarrow> (0::'a) \<le> prod_list xs \<and> prod_list xs \<le> prod_list ys; \<And>i. i < length (y # ys) \<Longrightarrow> (0::'a) \<le> (x # xs) ! i \<and> (x # xs) ! i \<le> (y # ys) ! i\<rbrakk> \<Longrightarrow> (0::'a) \<le> prod_list (x # xs) \<and> prod_list (x # xs) \<le> prod_list (y # ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs
(0::'a) \<le> u \<and> u \<le> v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> prod_list us \<and> prod_list us \<le> prod_list vs
(0::'a) \<le> u \<and> u \<le> v

goal (1 subgoal):
 1. (0::'a) \<le> prod_list (u # us) \<and> prod_list (u # us) \<le> prod_list (v # vs)
[PROOF STEP]
by (auto intro: mult_mono)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> prod_list (u # us) \<and> prod_list (u # us) \<le> prod_list (v # vs)

goal (1 subgoal):
 1. (\<And>i. i < length [] \<Longrightarrow> (0::'a) \<le> [] ! i \<and> [] ! i \<le> [] ! i) \<Longrightarrow> (0::'a) \<le> prod_list [] \<and> prod_list [] \<le> prod_list []
[PROOF STEP]
qed simp