Theory MFMC_Bounded
section ‹The max-flow min-cut theorem in bounded networks›
subsection ‹Linkages in unhindered bipartite webs›
theory MFMC_Bounded imports
Matrix_For_Marginals
MFMC_Reduction
begin
context countable_bipartite_web begin
lemma countable_A [simp]: "countable (A Γ)"
using A_vertex countable_V by(blast intro: countable_subset)
lemma unhindered_criterion [rule_format]:
assumes "¬ hindered Γ"
shows "∀X ⊆ A Γ. finite X ⟶ (∑⇧+ x∈X. weight Γ x) ≤ (∑⇧+ y∈❙E `` X. weight Γ y)"
using assms
proof(rule contrapos_np)
assume "¬ ?thesis"
then obtain X where "X ∈ {X. X ⊆ A Γ ∧ finite X ∧ (∑⇧+ y∈❙E `` X. weight Γ y) < (∑⇧+ x∈X. weight Γ x)}" (is "_ ∈ Collect ?P")
by(auto simp add: not_le)
from wf_eq_minimal[THEN iffD1, OF wf_finite_psubset, rule_format, OF this, simplified]
obtain X where X_A: "X ⊆ A Γ" and fin_X [simp]: "finite X"
and less: "(∑⇧+ y∈❙E `` X. weight Γ y) < (∑⇧+ x∈X. weight Γ x)"
and minimal: "⋀X'. X' ⊂ X ⟹ (∑⇧+ x∈X'. weight Γ x) ≤ (∑⇧+ y∈❙E `` X'. weight Γ y)"
by(clarsimp simp add: not_less)(meson finite_subset order_trans psubset_imp_subset)
have nonempty: "X ≠ {}" using less by auto
then obtain xx where xx: "xx ∈ X" by auto
define f where
"f x = (if x = xx then (∑⇧+ y∈❙E `` X. weight Γ y) - (∑⇧+ x∈X - {xx}. weight Γ x) else if x ∈ X then weight Γ x else 0)" for x
define g where
"g y = (if y ∈ ❙E `` X then weight Γ y else 0)" for y
define E' where "E' ≡ ❙E ∩ X × UNIV"
have Xxx: "X - {xx} ⊂ X" using xx by blast
have E [simp]: "E' `` X' = ❙E `` X'" if "X' ⊆ X" for X' using that by(auto simp add: E'_def)
have in_E': "(x, y) ∈ E' ⟷ x ∈ X ∧ (x, y) ∈ ❙E" for x y by(auto simp add: E'_def)
have "(∑⇧+ x∈X. f x) = (∑⇧+ x∈X - {xx}. f x) + (∑⇧+ x∈{xx}. f x)" using xx
by(auto simp add: nn_integral_count_space_indicator nn_integral_add[symmetric] simp del: nn_integral_indicator_singleton intro!: nn_integral_cong split: split_indicator)
also have "… = (∑⇧+ x∈X - {xx}. weight Γ x) + ((∑⇧+ y∈❙E `` X. weight Γ y) - (∑⇧+ x∈X - {xx}. weight Γ x))"
by(rule arg_cong2[where f="(+)"])(auto simp add: f_def xx nn_integral_count_space_indicator intro!: nn_integral_cong)
also have "… = (∑⇧+ y∈❙E `` X. g y)" using minimal[OF Xxx] xx
by(subst add_diff_eq_iff_ennreal[THEN iffD2])(fastforce simp add: g_def[abs_def] nn_integral_count_space_indicator intro!: nn_integral_cong intro: nn_integral_mono elim: order_trans split: split_indicator)+
finally have sum_eq: "(∑⇧+ x∈X. f x) = (∑⇧+ y∈❙E `` X. g y)" .
have "(∑⇧+ y∈❙E `` X. weight Γ y) = (∑⇧+ y∈❙E `` X. g y)"
by(auto simp add: nn_integral_count_space_indicator g_def intro!: nn_integral_cong)
then have fin: "… ≠ ⊤" using less by auto
have fin2: "(∑⇧+ x∈X'. weight Γ x) ≠ ⊤" if "X' ⊂ X" for X'
proof -
have "(∑⇧+ x∈❙E `` X'. weight Γ x) ≤ (∑⇧+ x∈❙E `` X. weight Γ x)" using that
by(auto 4 3 simp add: nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator split_indicator_asm)
then show ?thesis using minimal[OF that] less by(auto simp add: top_unique)
qed
have "f xx = (∑⇧+ y∈❙E `` X. weight Γ y) - (∑⇧+ x∈X - {xx}. weight Γ x)" by (simp add: f_def)
also have "… < (∑⇧+ x∈X. weight Γ x) - (∑⇧+ x∈X - {xx}. weight Γ x)" using less fin2[OF Xxx] minimal[OF Xxx]
by(subst minus_less_iff_ennreal)(fastforce simp add: less_top[symmetric] nn_integral_count_space_indicator diff_add_self_ennreal intro: nn_integral_mono elim: order_trans split: split_indicator)+
also have "… = (∑⇧+ x∈{xx}. weight Γ x)" using fin2[OF Xxx] xx
apply(simp add: nn_integral_count_space_indicator del: nn_integral_indicator_singleton)
apply(subst nn_integral_diff[symmetric])
apply(auto simp add: AE_count_space split: split_indicator simp del: nn_integral_indicator_singleton intro!: nn_integral_cong)
done
also have "… = weight Γ xx" by(simp add: nn_integral_count_space_indicator)
finally have fxx: "f xx < weight Γ xx" .
have le: "(∑⇧+ x∈X'. f x) ≤ (∑⇧+ y∈❙E `` X'. g y)" if "X' ⊆ X" for X'
proof(cases "X' = X")
case True
then show ?thesis using sum_eq by simp
next
case False
hence X': "X' ⊂ X" using that by blast
have "(∑⇧+ x∈X'. f x) = (∑⇧+ x∈X' - {xx}. f x) + (∑⇧+ x∈{xx}. f x * indicator X' xx)"
by(auto simp add: nn_integral_count_space_indicator nn_integral_add[symmetric] simp del: nn_integral_indicator_singleton intro!: nn_integral_cong split: split_indicator)
also have "… ≤ (∑⇧+ x∈X' - {xx}. f x) + (∑⇧+ x∈{xx}. weight Γ x * indicator X' xx)" using fxx
by(intro add_mono)(auto split: split_indicator simp add: nn_integral_count_space_indicator)
also have "… = (∑⇧+ x∈X'. weight Γ x)" using xx that
by(auto simp add: nn_integral_count_space_indicator nn_integral_add[symmetric] f_def simp del: nn_integral_indicator_singleton intro!: nn_integral_cong split: split_indicator)
also have "… ≤ (∑⇧+ y∈❙E `` X'. weight Γ y)" by(rule minimal[OF X'])
also have "… = (∑⇧+ y∈❙E `` X'. g y)" using that
by(auto 4 3 intro!: nn_integral_cong simp add: g_def Image_iff)
finally show ?thesis .
qed
have "countable X" using X_A A_vertex countable_V by(blast intro: countable_subset)
moreover have "❙E `` X ⊆ ❙V" by(auto simp add: vertex_def)
with countable_V have "countable (❙E `` X)" by(blast intro: countable_subset)
moreover have "E' ⊆ X × ❙E `` X" by(auto simp add: E'_def)
ultimately obtain h' where h'_dom: "⋀x y. 0 < h' x y ⟹ (x, y) ∈ E'"
and h'_fin: "⋀x y. h' x y ≠ ⊤"
and h'_f: "⋀x. x ∈ X ⟹ (∑⇧+ y∈E' `` X. h' x y) = f x"
and h'_g: "⋀y. y ∈ E' `` X ⟹ (∑⇧+ x∈X. h' x y) = g y"
using bounded_matrix_for_marginals_ennreal[where f=f and g=g and A=X and B="E' `` X" and R=E' and thesis=thesis] sum_eq fin le
by(auto)
have h'_outside: "(x, y) ∉ E' ⟹ h' x y = 0" for x y using h'_dom[of x y] not_gr_zero by(fastforce)
define h where "h = (λ(x, y). if x ∈ X ∧ edge Γ x y then h' x y else 0)"
have h_OUT: "d_OUT h x = (if x ∈ X then f x else 0)" for x
by(auto 4 3 simp add: h_def d_OUT_def h'_f[symmetric] E'_def nn_integral_count_space_indicator intro!: nn_integral_cong intro: h'_outside split: split_indicator)
have h_IN: "d_IN h y = (if y ∈ ❙E `` X then weight Γ y else 0)" for y using h'_g[of y, symmetric]
by(auto 4 3 simp add: h_def d_IN_def g_def nn_integral_count_space_indicator nn_integral_0_iff_AE in_E' intro!: nn_integral_cong intro: h'_outside split: split_indicator split_indicator_asm)
have h: "current Γ h"
proof
show "d_OUT h x ≤ weight Γ x" for x using fxx by(auto simp add: h_OUT f_def)
show "d_IN h y ≤ weight Γ y" for y by(simp add: h_IN)
show "h e = 0" if "e ∉ ❙E" for e using that by(cases e)(auto simp add: h_def)
qed
have "separating Γ (TER h)"
proof
fix x y p
assume x: "x ∈ A Γ" and y: "y ∈ B Γ" and p: "path Γ x p y"
then obtain [simp]: "p = [y]" and xy: "(x, y) ∈ ❙E" using disjoint
by -(erule rtrancl_path.cases; auto dest: bipartite_E)+
show "(∃z∈set p. z ∈ TER h) ∨ x ∈ TER h"
proof(rule disjCI)
assume "x ∉ TER h"
hence "x ∈ X" using x by(auto simp add: SAT.simps SINK.simps h_OUT split: if_split_asm)
hence "y ∈ TER h" using xy currentD_OUT[OF h y] by(auto simp add: SAT.simps h_IN SINK.simps)
thus "∃z∈set p. z ∈ TER h" by simp
qed
qed
then have w: "wave Γ h" using h ..
have "xx ∈ A Γ" using xx X_A by blast
moreover have "xx ∉ ℰ (TER h)"
proof
assume "xx ∈ ℰ (TER h)"
then obtain p y where y: "y ∈ B Γ" and p: "path Γ xx p y"
and bypass: "⋀z. ⟦ xx ≠ y; z ∈ set p ⟧ ⟹ z = xx ∨ z ∉ TER h"
by(rule ℰ_E) auto
from p obtain [simp]: "p = [y]" and xy: "edge Γ xx y" and neq: "xx ≠ y" using disjoint X_A xx y
by -(erule rtrancl_path.cases; auto dest: bipartite_E)+
from neq bypass[of y] have "y ∉ TER h" by simp
moreover from xy xx currentD_OUT[OF h y] have "y ∈ TER h"
by(auto simp add: SAT.simps h_IN SINK.simps)
ultimately show False by contradiction
qed
moreover have "d_OUT h xx < weight Γ xx" using fxx xx by(simp add: h_OUT)
ultimately have "hindrance Γ h" ..
then show "hindered Γ" using h w ..
qed
end
lemma nn_integral_count_space_top_approx:
fixes f :: "nat => ennreal" and b :: ennreal
assumes "nn_integral (count_space UNIV) f = top"
and "b < top"
obtains n where "b < sum f {..<n}"
using assms unfolding nn_integral_count_space_nat suminf_eq_SUP SUP_eq_top_iff by(auto)
lemma One_le_of_nat_ennreal: "(1 :: ennreal) ≤ of_nat x ⟷ 1 ≤ x"
by (metis of_nat_le_iff of_nat_1)
locale bounded_countable_bipartite_web = countable_bipartite_web Γ
for Γ :: "('v, 'more) web_scheme" (structure)
+
assumes bounded_B: "x ∈ A Γ ⟹ (∑⇧+ y ∈ ❙E `` {x}. weight Γ y) < ⊤"
begin
theorem unhindered_linkable_bounded:
assumes "¬ hindered Γ"
shows "linkable Γ"
proof(cases "A Γ = {}")
case True
hence "linkage Γ (λ_. 0)" by(auto simp add: linkage.simps)
moreover have "web_flow Γ (λ_. 0)" by(auto simp add: web_flow.simps)
ultimately show ?thesis by blast
next
case nonempty: False
define A_n :: "nat ⇒ 'v set" where "A_n n = from_nat_into (A Γ) ` {..n}" for n
have fin_A_n [simp]: "finite (A_n n)" for n by(simp add: A_n_def)
have A_n_A: "A_n n ⊆ A Γ" for n by(auto simp add: A_n_def from_nat_into[OF nonempty])
have countable2: "countable (❙E `` A_n n)" for n using countable_V
by(rule countable_subset[rotated])(auto simp add: vertex_def)
have "∃Y2. ∀n. ∀X ⊆ A_n n. Y2 n X ⊆ ❙E `` X ∧ (∑⇧+ x∈X. weight Γ x) ≤ (∑⇧+ y∈Y2 n X. weight Γ y) ∧ (∑⇧+ y∈Y2 n X. weight Γ y) ≠ ⊤"
proof(rule choice strip ex_simps(6)[THEN iffD2])+
fix n X
assume X: "X ⊆ A_n n"
then have [simp]: "finite X" by(rule finite_subset) simp
have X_count: "countable (❙E `` X)" using countable2
by(rule countable_subset[rotated])(rule Image_mono[OF order_refl X])
show "∃Y. Y ⊆ ❙E `` X ∧ (∑⇧+ x∈X. weight Γ x) ≤ (∑⇧+ y∈Y. weight Γ y) ∧ (∑⇧+ y∈Y. weight Γ y) ≠ ⊤" (is "Ex ?P")
proof(cases "(∑⇧+ y∈❙E `` X. weight Γ y) = ⊤")
case True
define Y' where "Y' = to_nat_on (❙E `` X) ` (❙E `` X)"
have inf: "infinite (❙E `` X)" using True
by(intro notI)(auto simp add: nn_integral_count_space_finite)
then have Y': "Y' = UNIV" using X_count by(auto simp add: Y'_def intro!: image_to_nat_on)
have "(∑⇧+ y∈❙E `` X. weight Γ y) = (∑⇧+ y∈from_nat_into (❙E `` X) ` Y'. weight Γ y * indicator (❙E `` X) y)"
using X_count
by(auto simp add: nn_integral_count_space_indicator Y'_def image_image intro!: nn_integral_cong from_nat_into_to_nat_on[symmetric] rev_image_eqI split: split_indicator)
also have "… = (∑⇧+ y. weight Γ (from_nat_into (❙E `` X) y) * indicator (❙E `` X) (from_nat_into (❙E `` X) y))"
using X_count inf by(subst nn_integral_count_space_reindex)(auto simp add: inj_on_def Y')
finally have "… = ⊤" using True by simp
from nn_integral_count_space_top_approx[OF this, of "sum (weight Γ) X"]
obtain yy where yy: "sum (weight Γ) X < (∑ y<yy. weight Γ (from_nat_into (❙E `` X) y) * indicator (❙E `` X) (from_nat_into (❙E `` X) y))"
by(auto simp add: less_top[symmetric])
define Y where "Y = from_nat_into (❙E `` X) ` {..<yy} ∩ ❙E `` X"
have [simp]: "finite Y" by(simp add: Y_def)
have "(∑⇧+ x∈X. weight Γ x) = sum (weight Γ) X" by(simp add: nn_integral_count_space_finite)
also have "… ≤ (∑ y<yy. weight Γ (from_nat_into (❙E `` X) y) * indicator (❙E `` X) (from_nat_into (❙E `` X) y))"
using yy by simp
also have "… = (∑ y ∈ from_nat_into (❙E `` X) ` {..<yy}. weight Γ y * indicator (❙E `` X) y)"
using X_count inf by(subst sum.reindex)(auto simp add: inj_on_def)
also have "… = (∑ y ∈ Y. weight Γ y)" by(auto intro!: sum.cong simp add: Y_def)
also have "… = (∑⇧+ y∈Y. weight Γ y)" by(simp add: nn_integral_count_space_finite)
also have "Y ⊆ ❙E `` X" by(simp add: Y_def)
moreover have "(∑⇧+ y∈Y. weight Γ y) ≠ ⊤" by(simp add: nn_integral_count_space_finite)
ultimately show ?thesis by blast
next
case False
with unhindered_criterion[OF assms, of X] X A_n_A[of n] have "?P (❙E `` X)" by auto
then show ?thesis ..
qed
qed
then obtain Y2
where Y2_A: "Y2 n X ⊆ ❙E `` X"
and le: "(∑⇧+ x∈X. weight Γ x) ≤ (∑⇧+ y∈Y2 n X. weight Γ y)"
and finY2: "(∑⇧+ y∈Y2 n X. weight Γ y) ≠ ⊤" if "X ⊆ A_n n" for n X by iprover
define Y where "Y n = (⋃ X ∈ Pow (A_n n). Y2 n X)" for n
define s where "s n = (∑⇧+ y∈Y n. weight Γ y)" for n
have Y_vertex: "Y n ⊆ ❙V" for n by(auto 4 3 simp add: Y_def vertex_def dest!: Y2_A[of _ n])
have Y_B: "Y n ⊆ B Γ" for n unfolding Y_def by(auto dest!: Y2_A[of _ n] dest: bipartite_E)
have s_top [simp]: "s n ≠ ⊤" for n
proof -
have "⟦x ∈ Y2 n X; X ⊆ A_n n⟧ ⟹ Suc 0 ≤ card {X. X ⊆ A_n n ∧ x ∈ Y2 n X}" for x X
by(subst card_le_Suc_iff)(auto intro!: exI[where x=X] exI[where x="{X. X ⊆ A_n n ∧ x ∈ Y2 n X} - {X}"])
then have "(∑⇧+ y∈Y n. weight Γ y) ≤ (∑⇧+ y∈Y n. ∑ X∈Pow (A_n n). weight Γ y * indicator (Y2 n X) y)"
by(intro nn_integral_mono)(auto simp add: Y_def One_le_of_nat_ennreal intro!: mult_right_mono[of "1 :: ennreal", simplified])
also have "… = (∑ X∈Pow (A_n n). ∑⇧+ y∈Y n. weight Γ y * indicator (Y2 n X) y)"
by(subst nn_integral_sum) auto
also have "… = (∑ X∈Pow (A_n n). ∑⇧+ y∈Y2 n X. weight Γ y)"
by(auto intro!: sum.cong nn_integral_cong simp add: nn_integral_count_space_indicator Y_def split: split_indicator)
also have "… < ⊤" by(simp add: less_top[symmetric] finY2)
finally show ?thesis by(simp add: less_top s_def)
qed
define f :: "nat ⇒ 'v option ⇒ real"
where "f n xo = (case xo of Some x ⇒ if x ∈ A_n n then enn2real (weight Γ x) else 0
| None ⇒ enn2real (s n - sum (weight Γ) (A_n n)))" for n xo
define g :: "nat ⇒ 'v ⇒ real"
where "g n y = enn2real (weight Γ y * indicator (Y n) y)" for n y
define R :: "nat ⇒ ('v option × 'v) set"
where "R n = map_prod Some id ` (❙E ∩ A_n n × Y n) ∪ {None} × Y n" for n
define A_n' where "A_n' n = Some ` A_n n ∪ {None}" for n
have f_simps:
"f n (Some x) = (if x ∈ A_n n then enn2real (weight Γ x) else 0)"
"f n None = enn2real (s n - sum (weight Γ) (A_n n))"
for n x by(simp_all add: f_def)
have g_s: "(∑⇧+ y∈Y n. g n y) = s n" for n
by(auto simp add: s_def g_def ennreal_enn2real_if intro!: nn_integral_cong)
have "(∑⇧+ x∈A_n' n. f n x) = (∑⇧+ x∈Some`A_n n. weight Γ (the x)) + (∑⇧+ x∈{None}. f n x)" for n
by(auto simp add: nn_integral_count_space_indicator nn_integral_add[symmetric] f_simps A_n'_def ennreal_enn2real_if simp del: nn_integral_indicator_singleton intro!: nn_integral_cong split: split_indicator)
also have "… n = sum (weight Γ) (A_n n) + (s n - sum (weight Γ) (A_n n))" for n
by(subst nn_integral_count_space_reindex)(auto simp add: nn_integral_count_space_finite f_simps ennreal_enn2real_if)
also have "… n = s n" for n using le[OF order_refl, of n]
by(simp add: s_def nn_integral_count_space_finite)(auto elim!: order_trans simp add: nn_integral_count_space_indicator Y_def intro!: nn_integral_mono split: split_indicator)
finally have sum_eq: "(∑⇧+ x∈A_n' n. f n x) = (∑⇧+ y∈Y n. g n y)" for n using g_s by simp
have "∃h'. ∀n. (∀x y. (x, y) ∉ R n ⟶ h' n x y = 0) ∧ (∀x y. h' n x y ≠ ⊤) ∧ (∀x∈A_n' n. (∑⇧+ y∈Y n. h' n x y) = f n x) ∧ (∀y∈Y n. (∑⇧+ x∈A_n' n. h' n x y) = g n y)"
(is "Ex (λh'. ∀n. ?Q n (h' n))")
proof(rule choice allI)+
fix n
note sum_eq
moreover have "(∑⇧+ y∈Y n. g n y) ≠ ⊤" using g_s by simp
moreover have le_fg: "(∑⇧+ x∈X. f n x) ≤ (∑⇧+ y∈R n `` X. g n y)" if "X ⊆ A_n' n" for X
proof(cases "None ∈ X")
case True
have "(∑⇧+ x∈X. f n x) ≤ (∑⇧+ x∈A_n' n. f n x)" using that
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
also have "… = (∑⇧+ y∈Y n. g n y)" by(simp add: sum_eq)
also have "R n `` X = Y n" using True by(auto simp add: R_def)
ultimately show ?thesis by simp
next
case False
then have *: "Some ` (the ` X) = X"
by(auto simp add: image_image)(metis (no_types, lifting) image_iff notin_range_Some option.sel option.collapse)+
from False that have X: "the ` X ⊆ A_n n" by(auto simp add: A_n'_def)
from * have "(∑⇧+ x∈X. f n x) = (∑⇧+ x∈Some ` (the ` X). f n x)" by simp
also have "… = (∑⇧+ x∈the ` X. f n (Some x))" by(rule nn_integral_count_space_reindex) simp
also have "… = (∑⇧+ x∈the ` X. weight Γ x)" using that False
by(auto 4 3intro!: nn_integral_cong simp add: f_simps A_n'_def ennreal_enn2real_if)
also have "… ≤ (∑⇧+ y∈Y2 n (the ` X). weight Γ y)" using False that
by(intro le)(auto simp add: A_n'_def)
also have "… ≤ (∑⇧+ y∈R n `` X. weight Γ y)" using False Y2_A[of "the ` X" n] X
by(auto simp add: A_n'_def nn_integral_count_space_indicator R_def Image_iff Y_def intro: rev_image_eqI intro!: nn_integral_mono split: split_indicator)
(drule (1) subsetD; clarify; drule (1) bspec; auto 4 3 intro: rev_image_eqI)
also have "… = (∑⇧+ y∈R n `` X. g n y)"
by(auto intro!: nn_integral_cong simp add: R_def g_def ennreal_enn2real_if)
finally show ?thesis .
qed
moreover have "countable (A_n' n)" by(simp add: A_n'_def countable_finite)
moreover have "countable (Y2 n X)" if "X ⊆ A_n n" for X using Y2_A[OF that]
by(rule countable_subset)(rule countable_subset[OF _ countable_V]; auto simp add: vertex_def)
then have "countable (Y n)" unfolding Y_def
by(intro countable_UN)(simp_all add: countable_finite)
moreover have "R n ⊆ A_n' n × Y n" by(auto simp add: R_def A_n'_def)
ultimately obtain h' where "⋀x y. 0 < h' x y ⟹ (x, y) ∈ R n" "⋀x y. h' x y ≠ ⊤"
"⋀x. x ∈ A_n' n ⟹ (∑⇧+ y∈Y n. h' x y) = (f n x)" "⋀y. y ∈ Y n ⟹ (∑⇧+ x∈A_n' n. h' x y) = g n y"
by(rule bounded_matrix_for_marginals_ennreal) blast+
hence "?Q n h'" by(auto)(use not_gr_zero in blast)
thus "Ex (?Q n)" by blast
qed
then obtain h' where dom_h': "⋀x y. (x, y) ∉ R n ⟹ h' n x y = 0"
and fin_h' [simp]: "⋀x y. h' n x y ≠ ⊤"
and h'_f: "⋀x. x ∈ A_n' n ⟹ (∑⇧+ y∈Y n. h' n x y) = f n x"
and h'_g: "⋀y. y ∈ Y n ⟹ (∑⇧+ x∈A_n' n. h' n x y) = g n y"
for n by blast
define h :: "nat ⇒ 'v × 'v ⇒ real"
where "h n = (λ(x, y). if x ∈ A_n n ∧ y ∈ Y n then enn2real (h' n (Some x) y) else 0)" for n
have h_nonneg: "0 ≤ h n xy" for n xy by(simp add: h_def split_def)
have h_notB: "h n (x, y) = 0" if "y ∉ B Γ" for n x y using Y_B[of n] that by(auto simp add: h_def)
have h_le_weight2: "h n (x, y) ≤ weight Γ y" for n x y
proof(cases "x ∈ A_n n ∧ y ∈ Y n")
case True
have "h' n (Some x) y ≤ (∑⇧+ x∈A_n' n. h' n x y)"
by(rule nn_integral_ge_point)(auto simp add: A_n'_def True)
also have "… ≤ weight Γ y" using h'_g[of y n] True by(simp add: g_def ennreal_enn2real_if)
finally show ?thesis using True by(simp add: h_def ennreal_enn2real_if)
qed(auto simp add: h_def)
have h_OUT: "d_OUT (h n) x = (if x ∈ A_n n then weight Γ x else 0)" for n x
using h'_f[of "Some x" n, symmetric]
by(auto simp add: h_def d_OUT_def A_n'_def f_simps ennreal_enn2real_if nn_integral_count_space_indicator intro!: nn_integral_cong)
have h_IN: "d_IN (h n) y = (if y ∈ Y n then enn2real (weight Γ y - h' n None y) else 0)" for n y
proof(cases "y ∈ Y n")
case True
have "d_IN (h n) y = (∑⇧+ x∈Some ` A_n n. h' n x y)"
by(subst nn_integral_count_space_reindex)
(auto simp add: d_IN_def h_def nn_integral_count_space_indicator ennreal_enn2real_if R_def intro!: nn_integral_cong dom_h' split: split_indicator)
also have "… = (∑⇧+ x∈A_n' n. h' n x y) - (∑⇧+ x∈{None}. h' n x y)"
apply(simp add: nn_integral_count_space_indicator del: nn_integral_indicator_singleton)
apply(subst nn_integral_diff[symmetric])
apply(auto simp add: AE_count_space A_n'_def nn_integral_count_space_indicator split: split_indicator intro!: nn_integral_cong)
done
also have "… = g n y - h' n None y" using h'_g[OF True] by(simp add: nn_integral_count_space_indicator)
finally show ?thesis using True by(simp add: g_def ennreal_enn2real_if)
qed(auto simp add: d_IN_def ennreal_enn2real_if nn_integral_0_iff_AE AE_count_space h_def g_def)
let ?Q = "❙V × ❙V"
have "bounded (range (λn. h n xy))" if "xy ∈ ?Q" for xy unfolding bounded_def dist_real_def
proof(rule exI strip|erule imageE|hypsubst)+
fix n
obtain x y where [simp]: "xy = (x, y)" by(cases xy)
have "h n (x, y) ≤ d_OUT (h n) x" unfolding d_OUT_def by(rule nn_integral_ge_point) simp
also have "… ≤ weight Γ x" by(simp add: h_OUT)
finally show "¦0 - h n xy¦ ≤ enn2real (weight Γ (fst xy))"
by(simp add: h_nonneg)(metis enn2real_ennreal ennreal_cases ennreal_le_iff weight_finite)
qed
moreover have "countable ?Q" using countable_V by(simp)
ultimately obtain k where k: "strict_mono k"
and conv: "⋀xy. xy ∈ ?Q ⟹ convergent (λn. h (k n) xy)"
by(rule convergent_bounded_family) blast+
have h_outside: "h n xy = 0" if "xy ∉ ?Q" for xy n using that A_n_A[of n] A_vertex Y_vertex
by(auto simp add: h_def split: prod.split)
have h_outside_AB: "h n (x, y) = 0" if "x ∉ A Γ ∨ y ∉ B Γ" for n x y
using that A_n_A[of n] Y_B[of n] by(auto simp add: h_def)
have h_outside_E: "h n (x, y) = 0" if "(x, y) ∉ ❙E" for n x y using that unfolding h_def
by(clarsimp)(subst dom_h', auto simp add: R_def)
define H where "H xy = lim (λn. h (k n) xy)" for xy
have H: "(λn. h (k n) xy) ⇢ H xy" for xy
using conv[of xy] unfolding H_def by(cases "xy ∈ ?Q")(auto simp add: convergent_LIMSEQ_iff h_outside)
have H_outside: "H (x, y) = 0" if "x ∉ A Γ ∨ y ∉ B Γ" for x y
using that by(simp add: H_def convergent_LIMSEQ_iff h_outside_AB)
have H': "(λn. ennreal (h (k n) xy)) ⇢ H xy" for xy
using H by(rule tendsto_ennrealI)
have H_def': "H xy = lim (λn. ennreal (h (k n) xy))" for xy by (metis H' limI)
have H_OUT: "d_OUT H x = weight Γ x" if x: "x ∈ A Γ" for x
proof -
let ?w = "λy. if (x, y) ∈ ❙E then weight Γ y else 0"
have sum_w: "(∑⇧+ y. if edge Γ x y then weight Γ y else 0) = (∑⇧+ y ∈ ❙E `` {x}. weight Γ y)"
by(simp add: nn_integral_count_space_indicator indicator_def of_bool_def if_distrib cong: if_cong)
have "(λn. d_OUT (h (k n)) x) ⇢ d_OUT H x" unfolding d_OUT_def
by(rule nn_integral_dominated_convergence[where w="?w"])(use bounded_B x in ‹simp_all add: AE_count_space H h_outside_E h_le_weight2 sum_w›)
moreover define n_x where "n_x = to_nat_on (A Γ) x"
have x': "x ∈ A_n (k n)" if "n ≥ n_x" for n
using that seq_suble[OF k, of n] x unfolding A_n_def
by(intro rev_image_eqI[where x=n_x])(simp_all add: A_n_def n_x_def)
have "(λn. d_OUT (h (k n)) x) ⇢ weight Γ x"
by(intro tendsto_eventually eventually_sequentiallyI[where c="n_x"])(simp add: h_OUT x')
ultimately show ?thesis by(rule LIMSEQ_unique)
qed
then have "linkage Γ H" ..
moreover
have "web_flow Γ H" unfolding web_flow_iff
proof
show "d_OUT H x ≤ weight Γ x" for x
by(cases "x ∈ A Γ")(simp_all add: H_OUT[unfolded d_OUT_def] H_outside d_OUT_def)
show "d_IN H y ≤ weight Γ y" for y
proof -
have "d_IN H y = (∑⇧+ x. liminf (λn. ennreal (h (k n) (x, y))))" unfolding d_IN_def H_def'
by(rule nn_integral_cong convergent_liminf_cl[symmetric] convergentI H')+
also have "… ≤ liminf (λn. d_IN (h (k n)) y)"
unfolding d_IN_def by(rule nn_integral_liminf) simp
also have "… ≤ liminf (λn. weight Γ y)" unfolding h_IN
by(rule Liminf_mono)(auto simp add: ennreal_enn2real_if)
also have "… = weight Γ y" by(simp add: Liminf_const)
finally show "?thesis" .
qed
show "ennreal (H e) = 0" if "e ∉ ❙E" for e
proof(rule LIMSEQ_unique[OF H'])
obtain x y where [simp]: "e = (x, y)" by(cases e)
have "ennreal (h (k n) (x, y)) = 0" for n
using dom_h'[of "Some x" y "k n"] that by(auto simp add: h_def R_def enn2real_eq_0_iff elim: meta_mp)
then show "(λn. ennreal (h (k n) e)) ⇢ 0" using that
by(intro tendsto_eventually eventually_sequentiallyI) simp
qed
qed
ultimately show ?thesis by blast
qed
end
subsection ‹Glueing the reductions together›
locale bounded_countable_web = countable_web Γ
for Γ :: "('v, 'more) web_scheme" (structure)
+
assumes bounded_out: "x ∈ ❙V - B Γ ⟹ (∑⇧+ y ∈ ❙E `` {x}. weight Γ y) < ⊤"
begin
lemma bounded_countable_bipartite_web_of: "bounded_countable_bipartite_web (bipartite_web_of Γ)"
(is "bounded_countable_bipartite_web ?Γ")
proof -
interpret bi: countable_bipartite_web ?Γ by(rule countable_bipartite_web_of)
show ?thesis
proof
fix x
assume "x ∈ A ?Γ"
then obtain x' where x: "x = Inl x'" and x': "vertex Γ x'" "x' ∉ B Γ" by auto
have "❙E⇘?Γ⇙ `` {x} ⊆ Inr ` ({x'} ∪ (❙E `` {x'}))" using x
by(auto simp add: bipartite_web_of_def vertex_def split: sum.split_asm)
hence "(∑⇧+ y ∈ ❙E⇘?Γ⇙ `` {x}. weight ?Γ y) ≤ (∑⇧+ y ∈ …. weight ?Γ y)"
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
also have "… = (∑⇧+ y∈{x'} ∪ (❙E `` {x'}). weight (bipartite_web_of Γ) (Inr y))"
by(rule nn_integral_count_space_reindex)(auto)
also have "… ≤ weight Γ x' + (∑⇧+ y ∈ ❙E `` {x'}. weight Γ y)"
apply(subst (1 2) nn_integral_count_space_indicator, simp, simp)
apply(cases "¬ edge Γ x' x'")
apply(subst nn_integral_disjoint_pair)
apply(auto intro!: nn_integral_mono add_increasing split: split_indicator)
done
also have "… < ⊤" using bounded_out[of x'] x' using weight_finite[of x'] by(simp del: weight_finite add: less_top)
finally show "(∑⇧+ y ∈ ❙E⇘?Γ⇙ `` {x}. weight ?Γ y) < ⊤" .
qed
qed
theorem loose_linkable_bounded:
assumes "loose Γ"
shows "linkable Γ"
proof -
interpret bi: bounded_countable_bipartite_web "bipartite_web_of Γ" by(rule bounded_countable_bipartite_web_of)
have "¬ hindered (bipartite_web_of Γ)" using assms by(rule unhindered_bipartite_web_of)
then have "linkable (bipartite_web_of Γ)"
by(rule bi.unhindered_linkable_bounded)
then show ?thesis by(rule linkable_bipartite_web_ofD) simp
qed
lemma bounded_countable_web_quotient_web: "bounded_countable_web (quotient_web Γ f)" (is "bounded_countable_web ?Γ")
proof -
interpret r: countable_web ?Γ by(rule countable_web_quotient_web)
show ?thesis
proof
fix x
assume "x ∈ ❙V⇘quotient_web Γ f⇙ - B (quotient_web Γ f)"
then have x: "x ∈ ❙V - B Γ" by(auto dest: vertex_quotient_webD)
have "(∑⇧+ y ∈ ❙E⇘?Γ⇙ `` {x}. weight ?Γ y) ≤ (∑⇧+ y ∈ ❙E `` {x}. weight Γ y)"
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
also have "… < ⊤" using x by(rule bounded_out)
finally show "(∑⇧+ y ∈ ❙E⇘?Γ⇙ `` {x}. weight ?Γ y) < ⊤" .
qed
qed
lemma ex_orthogonal_current:
"∃f S. web_flow Γ f ∧ separating Γ S ∧ orthogonal_current Γ f S"
proof -
from ex_maximal_wave[OF countable]
obtain f where f: "current Γ f"
and w: "wave Γ f"
and maximal: "⋀w. ⟦ current Γ w; wave Γ w; f ≤ w ⟧ ⟹ f = w" by blast
from ex_trimming[OF f w countable weight_finite] obtain h where h: "trimming Γ f h" ..
let ?Γ = "quotient_web Γ f"
interpret Γ: bounded_countable_web "?Γ" by(rule bounded_countable_web_quotient_web)
have "loose ?Γ" using f w maximal by(rule loose_quotient_web[OF weight_finite])
then have "linkable ?Γ" by(rule Γ.loose_linkable_bounded)
then obtain g where wg: "web_flow ?Γ g" and link: "linkage ?Γ g" by blast
let ?k = "plus_current h g"
have "web_flow Γ ?k" "orthogonal_current Γ ?k (ℰ (TER f))"
by(rule linkage_quotient_webD[OF f w wg link h])+
moreover have "separating Γ (ℰ (TER f))"
using waveD_separating[OF w] by(rule separating_essential)
ultimately show ?thesis by blast
qed
end
locale bounded_countable_network = countable_network Δ
for Δ :: "('v, 'more) network_scheme" (structure) +
assumes out: "⟦ x ∈ ❙V; x ≠ source Δ; x ≠ sink Δ ⟧ ⟹ d_OUT (capacity Δ) x < ⊤"
context antiparallel_edges begin
lemma Δ''_bounded_countable_network: "bounded_countable_network Δ''"
if "⋀x. ⟦ x ∈ ❙V; x ≠ source Δ; x ≠ sink Δ ⟧ ⟹ d_OUT (capacity Δ) x < ⊤"
proof -
interpret ae: countable_network Δ'' by(rule Δ''_countable_network)
show ?thesis
proof
fix x
assume x: "x ∈ ❙V⇘Δ''⇙" and not_source: "x ≠ source Δ''" and not_sink: "x ≠ sink Δ''"
from x consider (Vertex) x' where "x = Vertex x'" "x' ∈ ❙V" | (Edge) y z where "x = Edge y z" "edge Δ y z"
unfolding "❙V_Δ''" by auto
then show "d_OUT (capacity Δ'') x < ⊤"
proof cases
case Vertex
then show ?thesis using x not_source not_sink that[of x'] by auto
next
case Edge
then show ?thesis using capacity_finite[of "(y, z)"] by(simp del: capacity_finite add: less_top)
qed
qed
qed
end
context bounded_countable_network begin
lemma bounded_countable_web_web_of_network:
assumes source_in: "⋀x. ¬ edge Δ x (source Δ)"
and sink_out: "⋀y. ¬ edge Δ (sink Δ) y"
and undead: "⋀x y. edge Δ x y ⟹ (∃z. edge Δ y z) ∨ (∃z. edge Δ z x)"
and source_sink: "¬ edge Δ (source Δ) (sink Δ)"
and no_loop: "⋀x. ¬ edge Δ x x"
shows "bounded_countable_web (web_of_network Δ)" (is "bounded_countable_web ?Γ")
proof -
interpret web: countable_web ?Γ by(rule countable_web_web_of_network) fact+
show ?thesis
proof
fix e
assume "e ∈ ❙V⇘?Γ⇙ - B ?Γ"
then obtain x y where e: "e = (x, y)" and xy: "edge Δ x y" by(cases e) simp
from xy have y: "y ≠ source Δ" using source_in[of x] by auto
have out_sink: "d_OUT (capacity Δ) (sink Δ) = 0" unfolding d_OUT_def
by(auto simp add: nn_integral_0_iff_AE AE_count_space sink_out intro!: capacity_outside)
have "❙E⇘?Γ⇙ `` {e} ⊆ ❙E ∩ {y} × UNIV" using e by auto
hence "(∑⇧+ e' ∈ ❙E⇘?Γ⇙ `` {e}. weight ?Γ e') ≤ (∑⇧+ e ∈ ❙E ∩ {y} × UNIV. capacity Δ e)" using e
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
also have "… ≤ (∑⇧+ e ∈ Pair y ` UNIV. capacity Δ e)"
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
also have "… = d_OUT (capacity Δ) y" unfolding d_OUT_def
by(rule nn_integral_count_space_reindex) simp
also have "… < ⊤" using out[of y] xy y out_sink by(cases "y = sink Δ")(auto simp add: vertex_def)
finally show "(∑⇧+ e' ∈ ❙E⇘?Γ⇙ `` {e}. weight ?Γ e') < ⊤" .
qed
qed
context begin
qualified lemma max_flow_min_cut'_bounded:
assumes source_in: "⋀x. ¬ edge Δ x (source Δ)"
and sink_out: "⋀y. ¬ edge Δ (sink Δ) y"
and undead: "⋀x y. edge Δ x y ⟹ (∃z. edge Δ y z) ∨ (∃z. edge Δ z x)"
and source_sink: "¬ edge Δ (source Δ) (sink Δ)"
and no_loop: "⋀x. ¬ edge Δ x x"
and capacity_pos: "⋀e. e ∈ ❙E ⟹ capacity Δ e > 0"
shows "∃f S. flow Δ f ∧ cut Δ S ∧ orthogonal Δ f S"
by(rule max_flow_min_cut')(rule bounded_countable_web.ex_orthogonal_current[OF bounded_countable_web_web_of_network], fact+)
qualified lemma max_flow_min_cut''_bounded:
assumes sink_out: "⋀y. ¬ edge Δ (sink Δ) y"
and source_in: "⋀x. ¬ edge Δ x (source Δ)"
and no_loop: "⋀x. ¬ edge Δ x x"
and capacity_pos: "⋀e. e ∈ ❙E ⟹ capacity Δ e > 0"
shows "∃f S. flow Δ f ∧ cut Δ S ∧ orthogonal Δ f S"
proof -
interpret antiparallel_edges Δ ..
interpret Δ'': bounded_countable_network Δ'' by(rule Δ''_bounded_countable_network)(rule out)
have "∃f S. flow Δ'' f ∧ cut Δ'' S ∧ orthogonal Δ'' f S"
by(rule Δ''.max_flow_min_cut'_bounded)(auto simp add: sink_out source_in no_loop capacity_pos elim: edg.cases)
then obtain f S where f: "flow Δ'' f" and cut: "cut Δ'' S" and ortho: "orthogonal Δ'' f S" by blast
have "flow Δ (collect f)" using f by(rule flow_collect)
moreover have "cut Δ (cut' S)" using cut by(rule cut_cut')
moreover have "orthogonal Δ (collect f) (cut' S)" using ortho f by(rule orthogonal_cut')
ultimately show ?thesis by blast
qed
qualified lemma max_flow_min_cut'''_bounded:
assumes sink_out: "⋀y. ¬ edge Δ (sink Δ) y"
and source_in: "⋀x. ¬ edge Δ x (source Δ)"
and capacity_pos: "⋀e. e ∈ ❙E ⟹ capacity Δ e > 0"
shows "∃f S. flow Δ f ∧ cut Δ S ∧ orthogonal Δ f S"
proof -
interpret antiparallel_edges Δ ..
interpret Δ'': bounded_countable_network Δ'' by(rule Δ''_bounded_countable_network)(rule out)
have "∃f S. flow Δ'' f ∧ cut Δ'' S ∧ orthogonal Δ'' f S"
by(rule Δ''.max_flow_min_cut''_bounded)(auto simp add: sink_out source_in capacity_pos elim: edg.cases)
then obtain f S where f: "flow Δ'' f" and cut: "cut Δ'' S" and ortho: "orthogonal Δ'' f S" by blast
have "flow Δ (collect f)" using f by(rule flow_collect)
moreover have "cut Δ (cut' S)" using cut by(rule cut_cut')
moreover have "orthogonal Δ (collect f) (cut' S)" using ortho f by(rule orthogonal_cut')
ultimately show ?thesis by blast
qed
lemma Δ'''_bounded_countable_network: "bounded_countable_network Δ'''"
proof -
interpret Δ''': countable_network Δ''' by(rule Δ'''_countable_network)
show ?thesis
proof
fix x
assume x: "x ∈ ❙V⇘Δ'''⇙" and not_source: "x ≠ source Δ'''" and not_sink: "x ≠ sink Δ'''"
from x have x': "x ∈ ❙V" by(auto simp add: vertex_def)
have "d_OUT (capacity Δ''') x ≤ d_OUT (capacity Δ) x" by(rule d_OUT_mono) simp
also have "… < ⊤" using x' not_source not_sink by(simp add: out)
finally show "d_OUT (capacity Δ''') x < ⊤" .
qed
qed
theorem max_flow_min_cut_bounded:
"∃f S. flow Δ f ∧ cut Δ S ∧ orthogonal Δ f S"
proof -
interpret Δ': bounded_countable_network Δ''' by(rule Δ'''_bounded_countable_network)
have "∃f S. flow Δ''' f ∧ cut Δ''' S ∧ orthogonal Δ''' f S" by(rule Δ'.max_flow_min_cut'''_bounded) auto
then obtain f S where f: "flow Δ''' f" and cut: "cut Δ''' S" and ortho: "orthogonal Δ''' f S" by blast
from flow_Δ'''[OF this] show ?thesis by blast
qed
end
end
end