[STATEMENT]
lemma denote_while_n_positive:
  assumes dim0: "M0 \<in> carrier_mat d d" and dim1: "M1 \<in> carrier_mat d d" and un: "adjoint M1 * M1 \<le>\<^sub>L   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"
  shows "partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>)
[PROOF STEP]
proof (induction n arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS 0 \<rho>)
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS 0 \<rho>)
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote_while_n M0 M1 DS 0 \<rho>)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint dim0
[PROOF STATE]
proof (prove)
using this:
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> positive (?M * ?A * adjoint ?M)
M0 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote_while_n M0 M1 DS 0 \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
(positive \<rho> \<and> trace \<rho> \<le> 1) \<and> \<rho> \<in> carrier_mat d d
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> positive (?M * ?A * adjoint ?M)
M0 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote_while_n M0 M1 DS 0 \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (denote_while_n M0 M1 DS 0 \<rho>)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have pdoM: "partial_density_operator (M1 * \<rho> * adjoint M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
using pdo_close_under_measurement Suc dim1 un
[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)
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have cM: "M1 * \<rho> * adjoint M1 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> carrier_mat d d
[PROOF STEP]
using Suc dim1 adjoint_dim index_mult_mat
[PROOF STATE]
proof (prove)
using this:
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
M1 \<in> carrier_mat d d
?A \<in> carrier_mat ?n ?n \<Longrightarrow> adjoint ?A \<in> carrier_mat ?n ?n
\<lbrakk>?i < dim_row ?A; ?j < dim_col ?B\<rbrakk> \<Longrightarrow> (?A * ?B) $$ (?i, ?j) = row ?A ?i \<bullet> col ?B ?j
dim_row (?A * ?B) = dim_row ?A
dim_col (?A * ?B) = dim_col ?B

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator (M1 * \<rho> * adjoint M1)
M1 * \<rho> * adjoint M1 \<in> carrier_mat d d
[PROOF STEP]
have DSM1: "positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (M1 * \<rho> * adjoint M1)
M1 * \<rho> * adjoint M1 \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d
[PROOF STEP]
using DS
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (M1 * \<rho> * adjoint M1)
M1 * \<rho> * adjoint M1 \<in> carrier_mat d 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

goal (1 subgoal):
 1. positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have "trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
[PROOF STEP]
using trace_decrease_mul_adj Suc dim1 un
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d; ?x \<in> carrier_mat d d; adjoint ?x * ?x \<le>\<^sub>L 1\<^sub>m d\<rbrakk> \<Longrightarrow> trace (?x * ?\<rho> * adjoint ?x) \<le> trace ?\<rho>
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d
trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
[PROOF STEP]
have "partial_density_operator (DS (M1 * \<rho> * adjoint M1))"
[PROOF STATE]
proof (prove)
using this:
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d
trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>

goal (1 subgoal):
 1. partial_density_operator (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d
trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. partial_density_operator (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d
trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
(positive ?\<rho> \<and> trace ?\<rho> \<le> 1) \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
(positive \<rho> \<and> trace \<rho> \<le> 1) \<and> \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
have "positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) * adjoint M0)"
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) * adjoint M0)
[PROOF STEP]
using Suc DSM1
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (DS (M1 * \<rho> * adjoint M1))
partial_density_operator ?\<rho> \<and> ?\<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n ?\<rho>)
partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d
positive (DS (M1 * \<rho> * adjoint M1)) \<and> trace (DS (M1 * \<rho> * adjoint M1)) \<le> trace (M1 * \<rho> * adjoint M1) \<and> DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) * adjoint M0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) * adjoint M0)

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) * adjoint M0)
[PROOF STEP]
have "positive (denote_while_n M0 M1 DS (Suc n) \<rho>)"
[PROOF STATE]
proof (prove)
using this:
positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) * adjoint M0)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d \<Longrightarrow> positive (denote_while_n M0 M1 DS n \<rho>); partial_density_operator \<rho> \<and> \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (denote_while_n M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n M0 M1 DS (Suc n) \<rho>)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
positive (denote_while_n M0 M1 DS (Suc n) \<rho>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_sum_positive:
  assumes dim0: "M0 \<in> carrier_mat d d" and dim1: "M1 \<in> carrier_mat d d" and un: "adjoint M1 * M1 \<le>\<^sub>L   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 r: " \<rho> \<in> carrier_mat d d"
    shows "positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
have "\<And>k. k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS k \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS k \<rho>)
[PROOF STEP]
using assms denote_while_n_positive
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M1 * M1 \<le>\<^sub>L 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
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M1.0 * ?M1.0 \<le>\<^sub>L 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> \<and> ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho>)

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS k \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS ?k \<rho>)

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS ?k \<rho>)

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
have "\<And>k. k < n \<Longrightarrow> denote_while_n M0 M1 DS k \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> denote_while_n M0 M1 DS k \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_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> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M1 * M1 \<le>\<^sub>L 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. \<And>k. k < n \<Longrightarrow> denote_while_n M0 M1 DS k \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> denote_while_n M0 M1 DS ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS ?k \<rho>)
?k < n \<Longrightarrow> denote_while_n M0 M1 DS ?k \<rho> \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS ?k \<rho>)
?k < n \<Longrightarrow> denote_while_n M0 M1 DS ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
using matrix_sum_positive
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (denote_while_n M0 M1 DS ?k \<rho>)
?k < n \<Longrightarrow> denote_while_n M0 M1 DS ?k \<rho> \<in> carrier_mat d d
\<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. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trace_measure2_id:
  assumes dM0: "M0 \<in> carrier_mat n n" and dM1: "M1 \<in> carrier_mat n n"
    and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m n"
    and dA: "A \<in> carrier_mat n n"
  shows "trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
have "trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace ((adjoint M0 * M0 + adjoint M1 * M1) * A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace ((adjoint M0 * M0 + adjoint M1 * M1) * A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat n n
M1 \<in> carrier_mat n n
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m n
A \<in> carrier_mat n n

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace ((adjoint M0 * M0 + adjoint M1 * M1) * A)
[PROOF STEP]
by (mat_assoc n)
[PROOF STATE]
proof (state)
this:
trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace ((adjoint M0 * M0 + adjoint M1 * M1) * A)

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace ((adjoint M0 * M0 + adjoint M1 * M1) * A)

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
have "\<dots> = trace (1\<^sub>m n * A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace ((adjoint M0 * M0 + adjoint M1 * M1) * A) = trace (1\<^sub>m n * A)
[PROOF STEP]
using id
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m n

goal (1 subgoal):
 1. trace ((adjoint M0 * M0 + adjoint M1 * M1) * A) = trace (1\<^sub>m n * A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace ((adjoint M0 * M0 + adjoint M1 * M1) * A) = trace (1\<^sub>m n * A)

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace ((adjoint M0 * M0 + adjoint M1 * M1) * A) = trace (1\<^sub>m n * A)

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
have "\<dots> = trace A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (1\<^sub>m n * A) = trace A
[PROOF STEP]
using dA
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. trace (1\<^sub>m n * A) = trace A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (1\<^sub>m n * A) = trace A

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A

goal (1 subgoal):
 1. trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measurement_lowner_le_one1:
  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"
  shows "adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have paM0: "positive (adjoint M0 * M0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (adjoint M0 * M0)
[PROOF STEP]
apply (subgoal_tac "adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0 \<Longrightarrow> positive (adjoint M0 * M0)
 2. adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0 \<Longrightarrow> positive (adjoint M0 * M0)
[PROOF STEP]
using positive_if_decomp[of "adjoint M0 * M0"] dim0 adjoint_dim[OF dim0]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>adjoint M0 * M0 \<in> carrier_mat ?n ?n; \<exists>M. M * adjoint M = adjoint M0 * M0\<rbrakk> \<Longrightarrow> positive (adjoint M0 * M0)
M0 \<in> carrier_mat d d
adjoint M0 \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0 \<Longrightarrow> positive (adjoint M0 * M0)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0
[PROOF STEP]
using adjoint_adjoint[of M0]
[PROOF STATE]
proof (prove)
using this:
adjoint (adjoint M0) = M0

goal (1 subgoal):
 1. adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (adjoint M0 * M0)

goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have le1: "adjoint M0 * M0 + adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * M0 + adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using id lowner_le_refl[of "1\<^sub>m d"]
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
1\<^sub>m d \<in> carrier_mat ?n ?n \<Longrightarrow> 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. adjoint M0 * M0 + adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
adjoint M0 * M0 + adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show "adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using add_positive_le_reduce2[OF _ _ _ paM0 le1] dim0 dim1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>adjoint M1 * M1 \<in> carrier_mat ?n ?n; adjoint M0 * M0 \<in> carrier_mat ?n ?n; 1\<^sub>m d \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_sum_trace:
  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 r: " \<rho> \<in> carrier_mat d d"
      and pdor: "partial_density_operator \<rho>"
    shows "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. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have un: "adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_lowner_le_one1
[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\<rbrakk> \<Longrightarrow> adjoint ?M1.0 * ?M1.0 \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using dim0 dim1 id
[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\<rbrakk> \<Longrightarrow> adjoint ?M1.0 * ?M1.0 \<le>\<^sub>L 1\<^sub>m d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d

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

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have DS': "(DS \<rho> \<in> carrier_mat d d) \<and> partial_density_operator (DS \<rho>)" if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
have res: "positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
using DS that
[PROOF STATE]
proof (prove)
using this:
\<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>

goal (1 subgoal):
 1. positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
have "trace \<rho> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace \<rho> \<le> 1
[PROOF STEP]
using that partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
partial_density_operator ?A = (positive ?A \<and> trace ?A \<le> 1)

goal (1 subgoal):
 1. trace \<rho> \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace \<rho> \<le> 1

goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
trace \<rho> \<le> 1
[PROOF STEP]
have "trace (DS \<rho>) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
trace \<rho> \<le> 1

goal (1 subgoal):
 1. trace (DS \<rho>) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (DS \<rho>) \<le> 1

goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
trace (DS \<rho>) \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
trace (DS \<rho>) \<le> 1

goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> trace \<rho> \<and> DS \<rho> \<in> carrier_mat d d
trace (DS \<rho>) \<le> 1

goal (1 subgoal):
 1. DS \<rho> \<in> carrier_mat d d \<and> positive (DS \<rho>) \<and> trace (DS \<rho>) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS \<rho>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have dWk: "denote_while_n_iter M0 M1 DS k \<rho> \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS k \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_iter_dim[OF r pdor dim1 un] DS' dim0 dim1
[PROOF STATE]
proof (prove)
using this:
(\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> ?DS \<rho> \<in> carrier_mat d d \<and> partial_density_operator (?DS \<rho>)) \<Longrightarrow> denote_while_n_iter ?M0.0 M1 ?DS ?n \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote_while_n_iter ?M0.0 M1 ?DS ?n \<rho>)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS ?\<rho>)
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS k \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n_iter M0 M1 DS ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have pdoWk: "partial_density_operator (denote_while_n_iter M0 M1 DS k \<rho>)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote_while_n_iter M0 M1 DS k \<rho>)
[PROOF STEP]
using pdo_denote_while_n_iter[OF r pdor dim1 un] DS' dim0 dim1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<rho>. \<rho> \<in> carrier_mat d d \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (?DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat d d \<and> partial_density_operator \<rho> \<Longrightarrow> ?DS \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter ?M0.0 M1 ?DS ?n \<rho>)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat d d \<and> partial_density_operator (DS ?\<rho>)
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d

goal (1 subgoal):
 1. partial_density_operator (denote_while_n_iter M0 M1 DS k \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (denote_while_n_iter M0 M1 DS ?k \<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have dW0k: "denote_while_n M0 M1 DS k \<rho> \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS k \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_dim r dim0 dim1 pdor
[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> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
partial_density_operator \<rho>

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

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote_while_n M0 M1 DS ?k \<rho> \<in> carrier_mat d d
[PROOF STEP]
have dsW0k: "matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS ?k \<rho> \<in> carrier_mat d d

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

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

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have "(denote_while_n_comp M0 M1 DS n \<rho>) \<in> carrier_mat d d" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n_comp M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
unfolding denote_while_n_comp.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1 \<in> carrier_mat d d
[PROOF STEP]
using dim1 dWk
[PROOF STATE]
proof (prove)
using this:
M1 \<in> carrier_mat d d
denote_while_n_iter M0 M1 DS ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n_comp M0 M1 DS ?n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
denote_while_n_comp M0 M1 DS ?n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have
    pdoW1k: "partial_density_operator (denote_while_n_comp M0 M1 DS n \<rho>)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
unfolding denote_while_n_comp.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)
[PROOF STEP]
using pdo_close_under_measurement[OF dim1 dWk pdoWk un]
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (M1 * denote_while_n_iter M0 M1 DS ?k1 \<rho> * adjoint M1)

goal (1 subgoal):
 1. partial_density_operator (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
denote_while_n_comp M0 M1 DS ?n \<rho> \<in> carrier_mat d d
partial_density_operator (denote_while_n_comp M0 M1 DS ?n \<rho>)
[PROOF STEP]
have "trace (DS (denote_while_n_comp M0 M1 DS n \<rho>)) \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)" for n
[PROOF STATE]
proof (prove)
using this:
denote_while_n_comp M0 M1 DS ?n \<rho> \<in> carrier_mat d d
partial_density_operator (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. trace (DS (denote_while_n_comp M0 M1 DS n \<rho>)) \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
using DS
[PROOF STATE]
proof (prove)
using this:
denote_while_n_comp M0 M1 DS ?n \<rho> \<in> carrier_mat d d
partial_density_operator (denote_while_n_comp M0 M1 DS ?n \<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

goal (1 subgoal):
 1. trace (DS (denote_while_n_comp M0 M1 DS n \<rho>)) \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (DS (denote_while_n_comp M0 M1 DS ?n \<rho>)) \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)

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

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have "trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) = trace (DS (denote_while_n_comp M0 M1 DS n \<rho>))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) = trace (DS (denote_while_n_comp M0 M1 DS n \<rho>))
[PROOF STEP]
using denote_while_n_iter_assoc[folded denote_while_n_comp.simps]
[PROOF STATE]
proof (prove)
using this:
denote_while_n_iter ?M0.0 ?M1.0 ?DS (Suc ?n) ?\<rho> = ?DS (denote_while_n_comp ?M0.0 ?M1.0 ?DS ?n ?\<rho>)

goal (1 subgoal):
 1. trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) = trace (DS (denote_while_n_comp M0 M1 DS n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (denote_while_n_iter M0 M1 DS (Suc ?n) \<rho>) = trace (DS (denote_while_n_comp M0 M1 DS ?n \<rho>))

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (DS (denote_while_n_comp M0 M1 DS ?n \<rho>)) \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)
trace (denote_while_n_iter M0 M1 DS (Suc ?n) \<rho>) = trace (DS (denote_while_n_comp M0 M1 DS ?n \<rho>))
[PROOF STEP]
have leq3: "trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)" for n
[PROOF STATE]
proof (prove)
using this:
trace (DS (denote_while_n_comp M0 M1 DS ?n \<rho>)) \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)
trace (denote_while_n_iter M0 M1 DS (Suc ?n) \<rho>) = trace (DS (denote_while_n_comp M0 M1 DS ?n \<rho>))

goal (1 subgoal):
 1. trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (denote_while_n_iter M0 M1 DS (Suc ?n) \<rho>) \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have mainleq: "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho>" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho>
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc 0)) + trace (denote_while_n_comp M0 M1 DS 0 \<rho>) \<le> trace \<rho>
 2. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc 0)) + trace (denote_while_n_comp M0 M1 DS 0 \<rho>) \<le> trace \<rho>
 2. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc 0)) + trace (denote_while_n_comp M0 M1 DS 0 \<rho>) \<le> trace \<rho>
[PROOF STEP]
unfolding matrix_sum.simps denote_while_n.simps denote_while_n_comp.simps denote_while_n_iter.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M0 * \<rho> * adjoint M0 + 0\<^sub>m d d) + trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
[PROOF STEP]
apply (subgoal_tac "M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0 \<Longrightarrow> trace (M0 * \<rho> * adjoint M0 + 0\<^sub>m d d) + trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
 2. M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0
[PROOF STEP]
using trace_measure2_id[OF dim0 dim1 id r] dim0
[PROOF STATE]
proof (prove)
using this:
trace (M0 * \<rho> * adjoint M0) + trace (M1 * \<rho> * adjoint M1) = trace \<rho>
M0 \<in> carrier_mat d d

goal (2 subgoals):
 1. M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0 \<Longrightarrow> trace (M0 * \<rho> * adjoint M0 + 0\<^sub>m d d) + trace (M1 * \<rho> * adjoint M1) \<le> trace \<rho>
 2. M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0
[PROOF STEP]
using dim0
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d

goal (1 subgoal):
 1. M0 * \<rho> * adjoint M0 + 0\<^sub>m d d = M0 * \<rho> * adjoint M0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc 0)) + trace (denote_while_n_comp M0 M1 DS 0 \<rho>) \<le> trace \<rho>

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho>

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
have eq1: "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n)))
      = trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) = trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n))
[PROOF STEP]
unfolding matrix_sum.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote_while_n M0 M1 DS (Suc n) \<rho> + (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)) = trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
using trace_add_linear dW0k[of "Suc n"] dsW0k[of "Suc n"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?A + ?B) = trace ?A + trace ?B
denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d

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

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
have eq2: "trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>)
      = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
unfolding denote_while_n.simps denote_while_n_comp.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M0 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M0) + trace (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1) = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
using trace_measure2_id[OF dim0 dim1 id dWk[of "Suc n"]]
[PROOF STATE]
proof (prove)
using this:
trace (M0 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M0) + trace (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1) = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)

goal (1 subgoal):
 1. trace (M0 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M0) + trace (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1) = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>)
    = trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) = trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n))

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

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>)

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
have "\<dots> = trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
using eq2
[PROOF STATE]
proof (prove)
using this:
trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)

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

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n M0 M1 DS (Suc n) \<rho>) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) = trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
have "\<dots> \<le> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) \<le> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
using leq3
[PROOF STATE]
proof (prove)
using this:
trace (denote_while_n_iter M0 M1 DS (Suc ?n) \<rho>) \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)

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

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_iter M0 M1 DS (Suc n) \<rho>) \<le> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>)

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
have "\<dots> \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho>
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho>

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

goal (1 subgoal):
 1. \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> trace \<rho> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) \<rho>) \<le> trace \<rho>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc ?n)) + trace (denote_while_n_comp M0 M1 DS ?n \<rho>) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have reduce_le_complex: "(b::complex) \<ge> 0 \<Longrightarrow> a + b \<le> c \<Longrightarrow> a \<le> c" for a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> b; a + b \<le> c\<rbrakk> \<Longrightarrow> a \<le> c
[PROOF STEP]
by (simp add: less_eq_complex_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?b; ?a + ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have "positive (denote_while_n_comp M0 M1 DS n \<rho>)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
using pdoW1k
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. positive (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n_comp M0 M1 DS ?n \<rho>) \<and> trace (denote_while_n_comp M0 M1 DS ?n \<rho>) \<le> 1

goal (1 subgoal):
 1. positive (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (denote_while_n_comp M0 M1 DS ?n \<rho>)
[PROOF STEP]
have "trace (denote_while_n_comp M0 M1 DS n \<rho>) \<ge> 0" for n
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. 0 \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
using positive_trace
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n_comp M0 M1 DS ?n \<rho>)
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> 0 \<le> trace ?A

goal (1 subgoal):
 1. 0 \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
using \<open>\<And>n. denote_while_n_comp M0 M1 DS n \<rho> \<in> carrier_mat d d\<close>
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n_comp M0 M1 DS ?n \<rho>)
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> 0 \<le> trace ?A
denote_while_n_comp M0 M1 DS ?n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. 0 \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) \<le> trace \<rho>" for n
[PROOF STATE]
proof (prove)
using this:
0 \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) \<le> trace \<rho>
[PROOF STEP]
using mainleq reduce_le_complex[of "trace (denote_while_n_comp M0 M1 DS n \<rho>)"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> trace (denote_while_n_comp M0 M1 DS ?n \<rho>)
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc ?n)) + trace (denote_while_n_comp M0 M1 DS ?n \<rho>) \<le> trace \<rho>
\<lbrakk>0 \<le> trace (denote_while_n_comp M0 M1 DS n \<rho>); ?a + trace (denote_while_n_comp M0 M1 DS n \<rho>) \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

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

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

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>
[PROOF STEP]
unfolding matrix_sum.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (0\<^sub>m d d) \<le> trace \<rho>
[PROOF STEP]
using trace_zero positive_trace pdor
[PROOF STATE]
proof (prove)
using this:
trace (0\<^sub>m ?n ?n) = (0::?'a)
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> 0 \<le> trace ?A
partial_density_operator \<rho>

goal (1 subgoal):
 1. trace (0\<^sub>m d d) \<le> trace \<rho>
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
trace (0\<^sub>m ?n ?n) = (0::?'a)
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> 0 \<le> trace ?A
positive \<rho> \<and> trace \<rho> \<le> 1

goal (1 subgoal):
 1. trace (0\<^sub>m d d) \<le> trace \<rho>
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
trace (0\<^sub>m ?n ?n) = (0::?'a)
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> 0 \<le> trace ?A
positive \<rho> \<and> trace \<rho> \<le> 1
\<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc ?n)) \<le> trace \<rho>
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>
[PROOF STEP]
show "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>" for n
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc ?n)) \<le> trace \<rho>
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) \<le> trace \<rho>; trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>
 2. \<And>n. \<lbrakk>\<lbrakk>\<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) \<le> trace \<rho>; trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>; \<And>n. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) \<le> trace \<rho>; trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0) \<le> trace \<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n)) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) ?n) \<le> trace \<rho>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_sum_partial_density:
  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 r: " \<rho> \<in> carrier_mat d d"
  shows "(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. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
have "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. 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. 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:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> 1
[PROOF STEP]
using pdo
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> trace \<rho>
partial_density_operator \<rho>

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

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

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

goal (1 subgoal):
 1. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
have "positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
using assms DS denote_while_n_sum_positive measurement_lowner_le_one1[OF dim0 dim1 id]
[PROOF STATE]
proof (prove)
using this:
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
\<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
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M1.0 * ?M1.0 \<le>\<^sub>L 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> positive (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n)
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d

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

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

goal (1 subgoal):
 1. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<le> 1
positive (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_sum_lowner_le:
  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_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. 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]
proof auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
have whilenc: "denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_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> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<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. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
have sumc: "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. 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. 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:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
have "denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n
         = denote_while_n M0 M1 DS n \<rho>  + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + (- matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n
[PROOF STEP]
using  minus_add_uminus_mat[of "matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n" d d "matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d; matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
have "\<dots> = denote_while_n M0 M1 DS n \<rho>  + 0\<^sub>m d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho> + 0\<^sub>m d d
[PROOF STEP]
by (smt assoc_add_mat minus_add_uminus_mat minus_r_inv_mat sumc uminus_carrier_mat whilenc)
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho> + 0\<^sub>m d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n + - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho> + 0\<^sub>m d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
have "\<dots> = denote_while_n M0 M1 DS n \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> + 0\<^sub>m d d = denote_while_n M0 M1 DS n \<rho>
[PROOF STEP]
using whilenc
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> + 0\<^sub>m d d = denote_while_n M0 M1 DS n \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n \<rho> + 0\<^sub>m d d = denote_while_n M0 M1 DS n \<rho>

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho>
[PROOF STEP]
have simp: "denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n -  matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n =
                denote_while_n M0 M1 DS n \<rho> "
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho>

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
have "positive (denote_while_n M0 M1 DS n \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote_while_n M0 M1 DS n \<rho>)
[PROOF STEP]
using denote_while_n_positive assms measurement_lowner_le_one1[OF dim0 dim1 id]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M1.0 * ?M1.0 \<le>\<^sub>L 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> \<and> ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> positive (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
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (denote_while_n M0 M1 DS n \<rho>)
[PROOF STEP]
have "matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)"
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n M0 M1 DS n \<rho>)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n M0 M1 DS n \<rho>)

goal (1 subgoal):
 1. dim_row (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) = dim_row (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<and> dim_col (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) = dim_col (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<and> positive (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
using simp
[PROOF STATE]
proof (prove)
using this:
positive (denote_while_n M0 M1 DS n \<rho>)
denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n = denote_while_n M0 M1 DS n \<rho>

goal (1 subgoal):
 1. dim_row (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) = dim_row (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<and> dim_col (matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) = dim_col (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n) \<and> positive (denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n - matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n
[PROOF STEP]
show "matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n \<le>\<^sub>L
             (M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0 + matrix_sum d (\<lambda>n. M0 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M0) n)"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<le>\<^sub>L denote_while_n M0 M1 DS n \<rho> + matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n

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

goal:
No subgoals!
[PROOF STEP]
qed