[STATEMENT]
lemma left_null_space_orthogonal_complement_col_space:
  fixes A::"'a^'cols::{finite, wellorder}^'rows::{finite, wellorder}"
  shows "left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi> i j. cnj (A $ i $ j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
interpret m: matrix inner_rows inner_cols
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Generalizations2.matrix inner_rows inner_cols
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
using m.null_space_orthogonal_complement_row_space[of "transpose A"]
[PROOF STATE]
proof (prove)
using this:
null_space (Finite_Cartesian_Product.transpose A) = ROWS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (Finite_Cartesian_Product.transpose A $ i $ j)))

goal (1 subgoal):
 1. left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
unfolding left_null_space_eq_null_space_transpose
[PROOF STATE]
proof (prove)
using this:
null_space (Finite_Cartesian_Product.transpose A) = ROWS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (Finite_Cartesian_Product.transpose A $ i $ j)))

goal (1 subgoal):
 1. null_space (Finite_Cartesian_Product.transpose A) = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
unfolding col_space_eq_row_space_transpose
[PROOF STATE]
proof (prove)
using this:
null_space (Finite_Cartesian_Product.transpose A) = ROWS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (Finite_Cartesian_Product.transpose A $ i $ j)))

goal (1 subgoal):
 1. null_space (Finite_Cartesian_Product.transpose A) = ROWS.v.orthogonal_complement (row_space (Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
left_null_space A = ROWS.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma null_space_orthogonal_complement_row_space_complex:
  fixes A::"complex^'cols::{finite,wellorder}^'rows::{finite,wellorder}"
  shows "null_space A = complex_matrix.orthogonal_complement (row_space (\<chi> i j. cnj (A $ i $ j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null_space A = complex_matrix.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
using complex_matrix.null_space_orthogonal_complement_row_space
[PROOF STATE]
proof (prove)
using this:
null_space ?A = complex_matrix.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (?A $ i $ j)))

goal (1 subgoal):
 1. null_space A = complex_matrix.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
.


[STATEMENT]
lemma left_null_space_orthogonal_complement_col_space_complex:
  fixes A::"complex^'cols::{finite, wellorder}^'rows::{finite, wellorder}"
  shows "left_null_space A = complex_matrix.orthogonal_complement (col_space (\<chi> i j. cnj (A $ i $ j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_null_space A = complex_matrix.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
using complex_matrix.left_null_space_orthogonal_complement_col_space
[PROOF STATE]
proof (prove)
using this:
left_null_space ?A = complex_matrix.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (?A $ i $ j)))

goal (1 subgoal):
 1. left_null_space A = complex_matrix.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
.


[STATEMENT]
lemma null_space_orthogonal_complement_row_space_reals:
  fixes A::"real^'cols::{finite,wellorder}^'rows::{finite,wellorder}"
  shows "null_space A = real_matrix.orthogonal_complement (row_space A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null_space A = real_matrix.v.orthogonal_complement (row_space A)
[PROOF STEP]
using real_matrix.null_space_orthogonal_complement_row_space[of A]
[PROOF STATE]
proof (prove)
using this:
null_space A = real_matrix.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))

goal (1 subgoal):
 1. null_space A = real_matrix.v.orthogonal_complement (row_space A)
[PROOF STEP]
unfolding cnj_real_def
[PROOF STATE]
proof (prove)
using this:
null_space A = real_matrix.v.orthogonal_complement (row_space (\<chi>i j. id (A $ i $ j)))

goal (1 subgoal):
 1. null_space A = real_matrix.v.orthogonal_complement (row_space A)
[PROOF STEP]
by (simp add: vec_lambda_eta)


[STATEMENT]
lemma left_null_space_orthogonal_complement_col_space_real:
  fixes A::"real^'cols::{finite, wellorder}^'rows::{finite, wellorder}"
  shows "left_null_space A = real_matrix.orthogonal_complement (col_space A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_null_space A = real_matrix.v.orthogonal_complement (col_space A)
[PROOF STEP]
using real_matrix.left_null_space_orthogonal_complement_col_space[of A]
[PROOF STATE]
proof (prove)
using this:
left_null_space A = real_matrix.v.orthogonal_complement (col_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))

goal (1 subgoal):
 1. left_null_space A = real_matrix.v.orthogonal_complement (col_space A)
[PROOF STEP]
by (simp add: cnj_real_def vec_lambda_eta)


[STATEMENT]
lemma inj_Left [simp]: "inj_on Left X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on vertex.Left X
[PROOF STEP]
by(simp add: inj_on_def)


[STATEMENT]
lemma inj_Right [simp]: "inj_on Right X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on vertex.Right X
[PROOF STEP]
by(simp add: inj_on_def)


[STATEMENT]
lemma \<Delta>_sel [simp]:
  "edge \<Delta> = edge'"
  "capacity \<Delta> = cap"
  "source \<Delta> = Source"
  "sink \<Delta> = Sink"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (edge \<Delta> = edge' &&& capacity \<Delta> = cap) &&& source \<Delta> = Source &&& sink \<Delta> = Sink
[PROOF STEP]
by(simp_all add: \<Delta>_def)


[STATEMENT]
lemma IN_Left [simp]: "\<^bold>I\<^bold>N\<^bsub>\<Delta>\<^esub> (Left x) = (if x \<in> set_pmf p then {Source} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>I\<^bold>N\<^bsub>\<Delta>\<^esub> (vertex.Left x) = (if x \<in> set_pmf p then {Source} else {})
[PROOF STEP]
by(auto simp add: incoming_def)


[STATEMENT]
lemma OUT_Right [simp]: "\<^bold>O\<^bold>U\<^bold>T\<^bsub>\<Delta>\<^esub> (Right y) = (if y \<in> set_pmf q then {Sink} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>O\<^bold>U\<^bold>T\<^bsub>\<Delta>\<^esub> (vertex.Right y) = (if y \<in> set_pmf q then {Sink} else {})
[PROOF STEP]
by(auto simp add: outgoing_def)


[STATEMENT]
lemma OUT_cap_Source: "d_OUT cap Source = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
have "d_OUT cap Source = (\<Sum>\<^sup>+ y\<in>range Left. cap (Source, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT cap Source = (\<Sum>\<^sup>+ y\<in>range vertex.Left. cap (Source, y))
[PROOF STEP]
by(auto 4 4 simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.capacity_outside[simplified] split: split_indicator)
[PROOF STATE]
proof (state)
this:
d_OUT cap Source = (\<Sum>\<^sup>+ y\<in>range vertex.Left. cap (Source, y))

goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_OUT cap Source = (\<Sum>\<^sup>+ y\<in>range vertex.Left. cap (Source, y))

goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. pmf p y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>range vertex.Left. cap (Source, y)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Left. cap (Source, y)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))

goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Left. cap (Source, y)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))

goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf p x)) = 1
[PROOF STEP]
by(simp add: nn_integral_pmf)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf p x)) = 1

goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d_OUT cap Source = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d_OUT cap Source = 1

goal (1 subgoal):
 1. d_OUT cap Source = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
d_OUT cap Source = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma IN_cap_Left: "d_IN cap (Left x) = pmf p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN cap (vertex.Left x) = ennreal (pmf p x)
[PROOF STEP]
by(subst d_IN_alt_def[of _ \<Delta>])(simp_all add: pmf_eq_0_set_pmf nn_integral_count_space_indicator max_def)


[STATEMENT]
lemma OUT_cap_Right: "d_OUT cap (Right y) = pmf q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT cap (vertex.Right y) = ennreal (pmf q y)
[PROOF STEP]
by(subst d_OUT_alt_def[of _ \<Delta>])(simp_all add: pmf_eq_0_set_pmf nn_integral_count_space_indicator max_def)