# Theory Tensor_Unit_Vec

theory Tensor_Unit_Vec
imports Tensor_Product
```(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
section ‹Unit Vectors as Tensors›

theory Tensor_Unit_Vec
imports Tensor_Product
begin

definition unit_vec::"nat ⇒ nat ⇒ 'a::ring_1 tensor"
where "unit_vec n i = tensor_from_lookup [n] (λx. if x=[i] then 1 else 0)"

lemma dims_unit_vec: "dims (unit_vec n i) = [n]" unfolding unit_vec_def by (simp add: tensor_from_lookup_def)

lemma lookup_unit_vec:
assumes "j<n"
shows "lookup (unit_vec n i) [j] = (if i=j then 1 else 0)"
proof -
have "[j] ⊲ [n]" by (simp add: assms valid_index.Cons valid_index.Nil)
then have "lookup (unit_vec n i) [j] = (λx. if x=[i] then 1 else 0) [j]"
then show ?thesis by auto
qed

lemma subtensor_prod_with_unit_vec:
fixes A::"'a::ring_1 tensor"
assumes "j<n"
shows "subtensor (unit_vec n i ⊗ A) j = (if i=j then A else (tensor0 (dims A)))"
proof -
have 0:"lookup (unit_vec n i) [j] = (if i=j then 1 else 0)" unfolding unit_vec_def
by (simp add: assms lookup_tensor_from_lookup valid_index.Cons valid_index.Nil)
have 1:"order (unit_vec n i) = 1" unfolding unit_vec_def by (simp add: tensor_from_lookup_def)
from assms have 2:"j < hd (dims (tensor_from_lookup [n] (λx. if x = [i] then 1 else 0)))"
show ?thesis using unit_vec_def subtensor_prod_with_vec 1 2 0 smult_1 tensor_smult0
by (metis (no_types, lifting) tensor_from_lookup_eqI)
qed

lemma subtensor_decomposition:
assumes "dims A ≠ []"
shows "listsum (dims A) (map (λi. unit_vec (hd (dims A)) i ⊗ subtensor A i) [0..<hd (dims A)]) = A" (is "?LS = A")
proof -
let ?f = "λi. unit_vec (hd (dims A)) i ⊗ subtensor A i"
have correct_dims:"⋀B. B ∈ set (map ?f [0..<hd (dims A)]) ⟹ dims B = dims A"
proof-
fix B
assume "B ∈ set (map ?f [0..<hd (dims A)])"
then obtain i where B:"B = ?f i" and "i<hd (dims A)" by auto
then have "dims (subtensor A i) = tl (dims A)" using dims_subtensor using assms by blast
then show "dims B = dims A" unfolding B
by (metis append_Cons assms dims_tensor_prod dims_unit_vec list.exhaust_sel self_append_conv2)
qed
have "⋀j. j < hd (dims A) ⟹ subtensor ?LS j = subtensor A j"
proof -
fix j
assume "j < hd (dims A)"
have 1:"subtensor ?LS j = listsum (tl (dims A)) (map (λA. subtensor A j) (map ?f [0..<hd (dims A)]))"
using subtensor_listsum[of "(map (λi. ?f i) [0..<hd (dims A)])" "dims A" j, OF correct_dims assms ‹j < hd (dims A)›]
by linarith
also have "... = listsum (tl (dims A)) (map (λi. subtensor (?f i) j) [0..<hd (dims A)])"
proof -
have "map (λA. subtensor A j) (map ?f [0..<hd (dims A)]) = map (λi. subtensor (?f i) j) [0..<hd (dims A)]"
unfolding map_map[of "(λA. subtensor A j)" "?f" "[0..<hd (dims A)]"] by simp
with 1 show ?thesis by metis
qed
also have "... =  map (λi. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j"
unfolding subtensor_prod_with_unit_vec[OF ‹j < hd (dims A)›]
using listsum_all_0_but_one[of j "(map (λi. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)])" "tl (dims A)"]
by (simp add: ‹j < hd (dims A)› assms)
also have "... = subtensor A j" by (simp add: ‹j < hd (dims A)›)
finally show "subtensor ?LS j = subtensor A j" by auto
qed
moreover have "dims ?LS = dims A" using correct_dims listsum_dims by blast
ultimately show ?thesis using subtensor_eqI by (metis (no_types, lifting) assms)
qed

end
```