[STATEMENT]
lemma lowner_is_lub_matrix_sum:
  assumes dim0: "M0 \<in> carrier_mat d d" and dim1: "M1 \<in> carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d"
      and DS: "\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d"
      and pdo: "partial_density_operator \<rho>" and dimr: " \<rho> \<in> carrier_mat d d"
  shows  "matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
have sumdd: "\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
using  denote_while_n_sum_dim assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
have sumtr: "\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
using denote_while_n_sum_trace assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n) \<le> trace ?\<rho>
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
have sumpar: "\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
using denote_while_n_sum_partial_density assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n)
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
have sumle:"\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)
[PROOF STEP]
using denote_while_n_sum_lowner_le assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) (Suc ?n)
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
have seqd: "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
[PROOF STEP]
using matrix_seq_def sumdd sumpar sumle
[PROOF STATE]
proof (prove)
using this:
matrix_seq ?dim ?f \<equiv> (\<forall>n. ?f n \<in> carrier_mat ?dim ?dim) \<and> (\<forall>n. partial_density_operator (?f n)) \<and> (\<forall>n. ?f n \<le>\<^sub>L ?f (Suc n))
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
using matrix_seq.lowner_lub_prop[of d "(matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))"]
[PROOF STATE]
proof (prove)
using this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<Longrightarrow> matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_dim_positive:
  assumes dim0: "M0 \<in> carrier_mat d d" and dim1: "M1 \<in> carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d"
      and DS: "\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d"
      and pdo: "partial_density_operator \<rho>" and dimr: " \<rho> \<in> carrier_mat d d"
  shows
    "denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
have sumdd: "\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_sum_dim assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
have sumtr: "\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
using denote_while_n_sum_trace assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n) \<le> trace ?\<rho>
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
have sumpar: "\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
using denote_while_n_sum_partial_density assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n)
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
have sumle:"\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)
[PROOF STEP]
using denote_while_n_sum_lowner_le assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) (Suc ?n)
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
have seqd: "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
[PROOF STEP]
using matrix_seq_def sumdd sumpar sumle
[PROOF STATE]
proof (prove)
using this:
matrix_seq ?dim ?f \<equiv> (\<forall>n. ?f n \<in> carrier_mat ?dim ?dim) \<and> (\<forall>n. partial_density_operator (?f n)) \<and> (\<forall>n. ?f n \<le>\<^sub>L ?f (Suc n))
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
have "matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
using lowner_is_lub_matrix_sum assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>)))
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>) \<and> trace (DS ?\<rho>) \<le> trace ?\<rho> \<and> DS ?\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
[PROOF STEP]
have "matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d
            \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
            \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>
[PROOF STEP]
using matrix_seq.lowner_is_lub_dim seqd matrix_seq.lowner_lub_is_positive matrix_seq.lowner_lub_trace sumtr
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)))
\<lbrakk>matrix_seq ?dim ?f; matrix_seq.lowner_is_lub ?f ?M\<rbrakk> \<Longrightarrow> ?M \<in> carrier_mat ?dim ?dim
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))
matrix_seq ?dim ?f \<Longrightarrow> positive (matrix_seq.lowner_lub ?f)
\<lbrakk>matrix_seq ?dim ?f; \<forall>n. trace (?f n) \<le> ?x\<rbrakk> \<Longrightarrow> trace (matrix_seq.lowner_lub ?f) \<le> ?x
\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>

goal (1 subgoal):
 1. denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>
[PROOF STEP]
unfolding denote_while_def matrix_inf_sum_def
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>)) \<in> carrier_mat d d \<and> positive (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<and> trace (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>))) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while M0 M1 DS \<rho> \<in> carrier_mat d d \<and> positive (denote_while M0 M1 DS \<rho>) \<and> trace (denote_while M0 M1 DS \<rho>) \<le> trace \<rho>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_measure_dim:
  assumes "\<rho> \<in> carrier_mat d d"
    "measurement d n M"
    "\<And>\<rho>' k. \<rho>' \<in> carrier_mat d d \<Longrightarrow> k < n \<Longrightarrow> (DS!k) \<rho>' \<in> carrier_mat d d"
  shows
    "denote_measure n M DS \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_measure n M DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote_measure n M DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
have dMk: "k < n \<Longrightarrow> M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> M k \<in> carrier_mat d d
[PROOF STEP]
using assms measurement_def
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
measurement d n M
\<lbrakk>?\<rho>' \<in> carrier_mat d d; ?k < n\<rbrakk> \<Longrightarrow> (DS ! ?k) ?\<rho>' \<in> carrier_mat d d
measurement ?d ?n ?M = ((\<forall>j<?n. ?M j \<in> carrier_mat ?d ?d) \<and> matrix_sum ?d (\<lambda>j. adjoint (?M j) * ?M j) ?n = 1\<^sub>m ?d)

goal (1 subgoal):
 1. k < n \<Longrightarrow> M k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_measure n M DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
have d: "k < n \<Longrightarrow> (M k) * \<rho> * adjoint (M k) \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> M k * \<rho> * adjoint (M k) \<in> carrier_mat d d
[PROOF STEP]
using mult_carrier_mat[OF mult_carrier_mat[OF dMk assms(1)] adjoint_dim[OF dMk]]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k4 < n; ?k2 < n\<rbrakk> \<Longrightarrow> M ?k4 * \<rho> * adjoint (M ?k2) \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> M k * \<rho> * adjoint (M k) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> M ?k * \<rho> * adjoint (M ?k) \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_measure n M DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> M ?k * \<rho> * adjoint (M ?k) \<in> carrier_mat d d
[PROOF STEP]
have "k < n \<Longrightarrow> (DS!k) ((M k) * \<rho> * adjoint (M k)) \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k * \<rho> * adjoint (M ?k) \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> (DS ! k) (M k * \<rho> * adjoint (M k)) \<in> carrier_mat d d
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k * \<rho> * adjoint (M ?k) \<in> carrier_mat d d
\<lbrakk>?\<rho>' \<in> carrier_mat d d; ?k < n\<rbrakk> \<Longrightarrow> (DS ! ?k) ?\<rho>' \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> (DS ! k) (M k * \<rho> * adjoint (M k)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> (DS ! ?k) (M ?k * \<rho> * adjoint (M ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_measure n M DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> (DS ! ?k) (M ?k * \<rho> * adjoint (M ?k)) \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> (DS ! ?k) (M ?k * \<rho> * adjoint (M ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_measure n M DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
unfolding denote_measure_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> (DS ! ?k) (M ?k * \<rho> * adjoint (M ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (DS ! k) (M k * \<rho> * adjoint (M k))) n \<in> carrier_mat d d
[PROOF STEP]
using matrix_sum_dim[of n "\<lambda>k. (DS!k) ((M k) * \<rho> * adjoint (M k))"]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> (DS ! ?k) (M ?k * \<rho> * adjoint (M ?k)) \<in> carrier_mat d d
(\<And>k. k < n \<Longrightarrow> (DS ! k) (M k * \<rho> * adjoint (M k)) \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d (\<lambda>k. (DS ! k) (M k * \<rho> * adjoint (M k))) n \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (DS ! k) (M k * \<rho> * adjoint (M k))) n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_measure n M DS \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measure_well_com:
  assumes "well_com (Measure n M S)"
  shows "\<And>k. k < n \<Longrightarrow> well_com (S ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> well_com (S ! k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
well_com (Measure n M S)

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> well_com (S ! k)
[PROOF STEP]
unfolding well_com.simps
[PROOF STATE]
proof (prove)
using this:
measurement d n M \<and> length S = n \<and> list_all well_com S

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> well_com (S ! k)
[PROOF STEP]
using list_all_length
[PROOF STATE]
proof (prove)
using this:
measurement d n M \<and> length S = n \<and> list_all well_com S
list_all ?P ?xs = (\<forall>n<length ?xs. ?P (?xs ! n))

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> well_com (S ! k)
[PROOF STEP]
by auto


[STATEMENT]
lemma denote_measure_expand:
  assumes m: "m \<le> n" and wc: "well_com (Measure n M S)"
  shows "denote (Measure m M S) \<rho> = matrix_sum d (\<lambda>k. denote (S!k) ((M k) * \<rho> * adjoint (M k))) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (Measure m M S) \<rho> = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
unfolding denote.simps denote_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
have "k < m \<Longrightarrow> map denote S ! k = denote (S!k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < m \<Longrightarrow> map denote S ! k = denote (S ! k)
[PROOF STEP]
using wc m
[PROOF STATE]
proof (prove)
using this:
well_com (Measure n M S)
m \<le> n

goal (1 subgoal):
 1. k < m \<Longrightarrow> map denote S ! k = denote (S ! k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> map denote S ! ?k = denote (S ! ?k)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < m \<Longrightarrow> map denote S ! ?k = denote (S ! ?k)
[PROOF STEP]
have "k < m \<Longrightarrow> (map denote S ! k) (M k * \<rho> * adjoint (M k)) = denote (S!k) ((M k) * \<rho> * adjoint (M k))" for k
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> map denote S ! ?k = denote (S ! ?k)

goal (1 subgoal):
 1. k < m \<Longrightarrow> (map denote S ! k) (M k * \<rho> * adjoint (M k)) = denote (S ! k) (M k * \<rho> * adjoint (M k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> (map denote S ! ?k) (M ?k * \<rho> * adjoint (M ?k)) = denote (S ! ?k) (M ?k * \<rho> * adjoint (M ?k))

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < m \<Longrightarrow> (map denote S ! ?k) (M ?k * \<rho> * adjoint (M ?k)) = denote (S ! ?k) (M ?k * \<rho> * adjoint (M ?k))
[PROOF STEP]
show "matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m
    = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m"
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> (map denote S ! ?k) (M ?k * \<rho> * adjoint (M ?k)) = denote (S ! ?k) (M ?k * \<rho> * adjoint (M ?k))

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
using matrix_sum_cong[of m "\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))" "\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))"]
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> (map denote S ! ?k) (M ?k * \<rho> * adjoint (M ?k)) = denote (S ! ?k) (M ?k * \<rho> * adjoint (M ?k))
(\<And>k. k < m \<Longrightarrow> (map denote S ! k) (M k * \<rho> * adjoint (M k)) = denote (S ! k) (M k * \<rho> * adjoint (M k))) \<Longrightarrow> matrix_sum ?d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum ?d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. (map denote S ! k) (M k * \<rho> * adjoint (M k))) m = matrix_sum d (\<lambda>k. denote (S ! k) (M k * \<rho> * adjoint (M k))) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_sum_trace_le:
  fixes f :: "nat \<Rightarrow> complex mat" and g :: "nat \<Rightarrow> complex mat"
  assumes "(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d)"
    "(\<And>k. k < n \<Longrightarrow> g k \<in> carrier_mat d d)"
    "(\<And>k. k < n \<Longrightarrow> trace (f k) \<le> trace (g k))"
  shows "trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)
[PROOF STEP]
have "sum (\<lambda>k. trace (f k)) {0..<n} \<le>  sum (\<lambda>k. trace (g k)) {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..<n. trace (f k)) \<le> (\<Sum>k = 0..<n. trace (g k))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> f ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> g ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> trace (f ?k) \<le> trace (g ?k)

goal (1 subgoal):
 1. (\<Sum>k = 0..<n. trace (f k)) \<le> (\<Sum>k = 0..<n. trace (g k))
[PROOF STEP]
by (meson atLeastLessThan_iff sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<n. trace (f k)) \<le> (\<Sum>k = 0..<n. trace (g k))

goal (1 subgoal):
 1. trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>k = 0..<n. trace (f k)) \<le> (\<Sum>k = 0..<n. trace (g k))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k = 0..<n. trace (f k)) \<le> (\<Sum>k = 0..<n. trace (g k))

goal (1 subgoal):
 1. trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)
[PROOF STEP]
using trace_matrix_sum_linear assms
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k = 0..<n. trace (f k)) \<le> (\<Sum>k = 0..<n. trace (g k))
(\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d) \<Longrightarrow> trace (matrix_sum ?d ?f ?n) = (\<Sum>k = 0..<?n. trace (?f k))
?k < n \<Longrightarrow> f ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> g ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> trace (f ?k) \<le> trace (g ?k)

goal (1 subgoal):
 1. trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d f n) \<le> trace (matrix_sum d g n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_denote_positive_trace_dim:
  assumes "well_com (Measure x1 x2a x3a)"
    "x4 \<in> carrier_mat d d"
    "partial_density_operator x4"
    "\<And>x3aa \<rho>. x3aa \<in> set x3a \<Longrightarrow> well_com x3aa \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
      \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d"
  shows "\<forall>k < x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))
               \<and> ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<in> carrier_mat d d
               \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have x2ak: "\<forall> k < x1. x2a k \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. x2a k \<in> carrier_mat d d
[PROOF STEP]
using assms(1) measurement_dim
[PROOF STATE]
proof (prove)
using this:
well_com (Measure x1 x2a x3a)
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. x2a k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>k<x1. x2a k \<in> carrier_mat d d
[PROOF STEP]
have x2aa:"\<forall> k < x1. (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. x2a k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. x2a k \<in> carrier_mat d d
x4 \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have posct: "positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))
               \<and> ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<in> carrier_mat d d
               \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))"
    if k: "k < x1" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have lea: "adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_le_one_mat assms(1) k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>measurement ?d ?n ?f; ?j < ?n\<rbrakk> \<Longrightarrow> adjoint (?f ?j) * ?f ?j \<le>\<^sub>L 1\<^sub>m ?d
well_com (Measure x1 x2a x3a)
k < x1

goal (1 subgoal):
 1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have "(x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
using k x2aa assms(2)
[PROOF STATE]
proof (prove)
using this:
k < x1
\<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
x4 \<in> carrier_mat d d

goal (1 subgoal):
 1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have "(x3a ! k) \<in> set x3a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x3a ! k \<in> set x3a
[PROOF STEP]
using k assms(1)
[PROOF STATE]
proof (prove)
using this:
k < x1
well_com (Measure x1 x2a x3a)

goal (1 subgoal):
 1. x3a ! k \<in> set x3a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x3a ! k \<in> set x3a

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x3a ! k \<in> set x3a

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have "well_com (x3a ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_com (x3a ! k)
[PROOF STEP]
using k assms(1)
[PROOF STATE]
proof (prove)
using this:
k < x1
well_com (Measure x1 x2a x3a)

goal (1 subgoal):
 1. well_com (x3a ! k)
[PROOF STEP]
using measure_well_com
[PROOF STATE]
proof (prove)
using this:
k < x1
well_com (Measure x1 x2a x3a)
\<lbrakk>well_com (Measure ?n ?M ?S); ?k < ?n\<rbrakk> \<Longrightarrow> well_com (?S ! ?k)

goal (1 subgoal):
 1. well_com (x3a ! k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
well_com (x3a ! k)

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
well_com (x3a ! k)

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have "partial_density_operator (x2a k * x4 * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
using pdo_close_under_measurement x2ak assms(2,3) lea  k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?\<rho> \<in> carrier_mat ?n ?n; partial_density_operator ?\<rho>; adjoint ?M * ?M \<le>\<^sub>L 1\<^sub>m ?n\<rbrakk> \<Longrightarrow> partial_density_operator (?M * ?\<rho> * adjoint ?M)
\<forall>k<x1. x2a k \<in> carrier_mat d d
x4 \<in> carrier_mat d d
partial_density_operator x4
adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
k < x1

goal (1 subgoal):
 1. partial_density_operator (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
partial_density_operator (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
x3a ! k \<in> set x3a
well_com (x3a ! k)
partial_density_operator (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have "positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)))
         \<and> (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<in> carrier_mat d d
         \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
using this:
x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
x3a ! k \<in> set x3a
well_com (x3a ! k)
partial_density_operator (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
x3a ! k \<in> set x3a
well_com (x3a ! k)
partial_density_operator (x2a k * x4 * adjoint (x2a k))
\<lbrakk>?x3aa \<in> set x3a; well_com ?x3aa; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?x3aa ?\<rho>) \<and> trace (denote ?x3aa ?\<rho>) \<le> trace ?\<rho> \<and> denote ?x3aa ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
using assms(1) k
[PROOF STATE]
proof (prove)
using this:
positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
well_com (Measure x1 x2a x3a)
k < x1

goal (1 subgoal):
 1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> positive ((map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k))) \<and> (map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k))) \<le> trace (x2a ?k * x4 * adjoint (x2a ?k))

goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < x1 \<Longrightarrow> positive ((map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k))) \<and> (map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k))) \<le> trace (x2a ?k * x4 * adjoint (x2a ?k))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> positive ((map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k))) \<and> (map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! ?k) (x2a ?k * x4 * adjoint (x2a ?k))) \<le> trace (x2a ?k * x4 * adjoint (x2a ?k))

goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_measure_positive_trace_dim:
  assumes "well_com (Measure x1 x2a x3a)"
    "x4 \<in> carrier_mat d d"
    "partial_density_operator x4"
    "\<And>x3aa \<rho>. x3aa \<in> set x3a \<Longrightarrow> well_com x3aa \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
      \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d"
  shows "positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4
        \<and> (denote (Measure x1 x2a x3a) x4) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
have x2ak: "\<forall> k < x1. x2a k \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. x2a k \<in> carrier_mat d d
[PROOF STEP]
using assms(1) measurement_dim
[PROOF STATE]
proof (prove)
using this:
well_com (Measure x1 x2a x3a)
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. x2a k \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>k<x1. x2a k \<in> carrier_mat d d
[PROOF STEP]
have x2aa:"\<forall> k < x1. (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. x2a k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. x2a k \<in> carrier_mat d d
x4 \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
have posct:"\<forall> k < x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))
               \<and> ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<in> carrier_mat d d
               \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
using map_denote_positive_trace_dim assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com (Measure ?x1.0 ?x2a ?x3a); ?x4.0 \<in> carrier_mat d d; partial_density_operator ?x4.0; \<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set ?x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> \<forall>k<?x1.0. positive ((map denote ?x3a ! k) (?x2a k * ?x4.0 * adjoint (?x2a k))) \<and> (map denote ?x3a ! k) (?x2a k * ?x4.0 * adjoint (?x2a k)) \<in> carrier_mat d d \<and> trace ((map denote ?x3a ! k) (?x2a k * ?x4.0 * adjoint (?x2a k))) \<le> trace (?x2a k * ?x4.0 * adjoint (?x2a k))
well_com (Measure x1 x2a x3a)
x4 \<in> carrier_mat d d
partial_density_operator x4
\<lbrakk>?x3aa \<in> set x3a; well_com ?x3aa; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?x3aa ?\<rho>) \<and> trace (denote ?x3aa ?\<rho>) \<le> trace ?\<rho> \<and> denote ?x3aa ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1)
       \<le> trace (matrix_sum d (\<lambda>k. (x2a k * x4 * adjoint (x2a k))) x1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1)
[PROOF STEP]
using posct matrix_sum_trace_le[of x1 "(\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))" "(\<lambda>k. x2a k * x4 * adjoint (x2a k)) "]
         x2aa
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
\<lbrakk>\<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d; \<And>k. k < x1 \<Longrightarrow> x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d; \<And>k. k < x1 \<Longrightarrow> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1)
\<forall>k<x1. x2a k * x4 * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1)

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1)

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
have "\<dots> = trace x4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1) = trace x4
[PROOF STEP]
using trace_measurement[of d "x1" "x2a" x4] assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>measurement d x1 x2a; x4 \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1) = trace x4
well_com (Measure x1 x2a x3a)
x4 \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1) = trace x4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>k. x2a k * x4 * adjoint (x2a k)) x1) = trace x4

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4
[PROOF STEP]
have " trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4"
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4
[PROOF STEP]
have "trace (denote_measure x1 x2a (map denote x3a) x4) \<le> trace x4"
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4

goal (1 subgoal):
 1. trace (denote_measure x1 x2a (map denote x3a) x4) \<le> trace x4
[PROOF STEP]
unfolding denote_measure_def
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1) \<le> trace x4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (denote_measure x1 x2a (map denote x3a) x4) \<le> trace x4

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (denote_measure x1 x2a (map denote x3a) x4) \<le> trace x4
[PROOF STEP]
have "trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4"
[PROOF STATE]
proof (prove)
using this:
trace (denote_measure x1 x2a (map denote x3a) x4) \<le> trace x4

goal (1 subgoal):
 1. trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
from posct
[PROOF STATE]
proof (chain)
picking this:
\<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))
[PROOF STEP]
have "positive (denote (Measure x1 x2a x3a) x4)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k)) \<Longrightarrow> positive (denote_measure x1 x2a (map denote x3a) x4)
[PROOF STEP]
unfolding denote_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k)) \<Longrightarrow> positive (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1)
[PROOF STEP]
using matrix_sum_positive
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d; \<And>k. k < ?n \<Longrightarrow> positive (?f k)\<rbrakk> \<Longrightarrow> positive (matrix_sum ?d ?f ?n)

goal (1 subgoal):
 1. \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k)) \<Longrightarrow> positive (matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (denote (Measure x1 x2a x3a) x4)

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (denote (Measure x1 x2a x3a) x4)

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
have "(denote (Measure x1 x2a x3a) x4) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_measure x1 x2a (map denote x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
unfolding denote_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1 \<in> carrier_mat d d
[PROOF STEP]
using matrix_sum_dim posct
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d ?f ?n \<in> carrier_mat ?d ?d
\<forall>k<x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) \<le> trace (x2a k * x4 * adjoint (x2a k))

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1 \<in> carrier_mat d d
[PROOF STEP]
by (simp add: matrix_sum_dim)
[PROOF STATE]
proof (state)
this:
denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4
positive (denote (Measure x1 x2a x3a) x4)
denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4
positive (denote (Measure x1 x2a x3a) x4)
denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (denote (Measure x1 x2a x3a) x4) \<and> trace (denote (Measure x1 x2a x3a) x4) \<le> trace x4 \<and> denote (Measure x1 x2a x3a) x4 \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed