# Theory Fashoda_Theorem

theory Fashoda_Theorem
imports Cartesian_Euclidean_Space

section

theory Fashoda_Theorem
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
begin

subsection

definition interval_bij ::
where

lemma interval_bij_affine:

by (auto simp: sum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff

lemma continuous_interval_bij:
fixes a b ::
shows
by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)

lemma continuous_on_interval_bij:
apply(rule continuous_at_imp_continuous_on)
apply (rule, rule continuous_interval_bij)
done

lemma in_interval_interval_bij:
fixes a b u v x ::
assumes
and
shows
apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
apply safe
proof -
fix i :: 'a
assume i:
have
using assms by auto
with i have *:
using assms(2) by (auto simp add: box_eq_empty)
have x:
using assms(1)[unfolded mem_box] using i by auto
have
using * x by auto
then show
using * by auto
have
apply (rule mult_right_mono)
unfolding divide_le_eq_1
using * x
apply auto
done
then show
using * by auto
qed

lemma interval_bij_bij:

by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])

lemma interval_bij_bij_cart: fixes x:: assumes
shows
using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)

subsection

lemma infnorm_2:
fixes x ::
shows
unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto

lemma infnorm_eq_1_2:
fixes x ::
shows
unfolding infnorm_2 by auto

lemma infnorm_eq_1_imp:
fixes x ::
assumes
shows  and
using assms unfolding infnorm_eq_1_2 by auto

lemma fashoda_unit:
fixes f g ::
assumes
and
and
and
and
and
and
shows
proof (rule ccontr)
assume
note as = this[unfolded bex_simps,rule_format]
define sqprojection
where [abs_def]:  for z ::
define negatex ::
where  for x
have lem1:
unfolding negatex_def infnorm_2 vector_2 by auto
have lem2:
unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR]
let ?F =
have *:
proof
show  for i
by (auto simp: mem_box_cart)
show  for i
by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component)
qed
{
fix x
assume
then obtain w ::  where w:

unfolding image_iff ..
then have
using as[of  ]
unfolding mem_box_cart atLeastAtMost_iff
by auto
} note x0 = this
have 1:
unfolding interval_eq_empty_cart by auto
have
for i x y c
using exhaust_2 [of i] by (auto simp: negatex_def)
then have
then have 2:
apply (intro continuous_intros continuous_on_component)
unfolding * sqprojection_def
apply (intro assms continuous_intros)+
apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
done
have 3:
unfolding subset_eq
proof (rule, goal_cases)
case (1 x)
then obtain y ::  where y:

unfolding image_iff ..
have
by (rule x0) (use y in auto)
then have *:
unfolding y o_def
by - (rule lem2[rule_format])
have inf1:
unfolding *[symmetric] y o_def
by (rule lem1[rule_format])
show
unfolding mem_box_cart interval_cbox_cart infnorm_2
proof
fix i
show
using exhaust_2 [of i] inf1 by (auto simp: infnorm_2)
qed
qed
obtain x ::  where x:

apply (rule brouwer_weak[of  ])
apply (rule compact_cbox convex_box)+
unfolding interior_cbox
apply (rule 1 2 3)+
apply blast
done
have
by (rule x0) (use x in auto)
then have *:
unfolding o_def
by (rule lem2[rule_format])
have nx:
apply (subst x(2)[symmetric])
unfolding *[symmetric] o_def
apply (rule lem1[rule_format])
done
have iff:   if  for x i
proof -
have
then show
and
unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
unfolding zero_less_mult_iff mult_less_0_iff
qed
have x1:
using x(1) unfolding mem_box_cart by auto
then have nz:
using as by auto
consider  |  |  |
using nx unfolding infnorm_eq_1_2 by auto
then show False
proof cases
case 1
then have *:
using assms(5) by auto
have
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
by (auto simp: negatex_def 1)
moreover
from x1 have
using assms(2) by blast
ultimately show False
unfolding iff[OF nz] vector_component_simps * mem_box_cart
using not_le by auto
next
case 2
then have *:
using assms(6) by auto
have
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2
by (auto simp: negatex_def)
moreover have
using assms(2) x1 by blast
ultimately show False
unfolding iff[OF nz] vector_component_simps * mem_box_cart
using not_le by auto
next
case 3
then have *:
using assms(7) by auto
have
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def)
moreover
from x1 have
using assms(1) by blast
ultimately show False
unfolding iff[OF nz] vector_component_simps * mem_box_cart
by (erule_tac x=2 in allE) auto
next
case 4
then have *:
using assms(8) by auto
have
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def)
moreover
from x1 have
using assms(1) by blast
ultimately show False
unfolding iff[OF nz] vector_component_simps * mem_box_cart
by (erule_tac x=2 in allE) auto
qed
qed

lemma fashoda_unit_path:
fixes f g ::
assumes
and
and
and
and
and
and
and
obtains z where  and
proof -
note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
define iscale where [abs_def]:  for z :: real
have isc:
unfolding iscale_def by auto
have
proof (rule fashoda_unit)
show
using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
have *:
unfolding iscale_def by (rule continuous_intros)+
show
apply -
apply (rule_tac[!] continuous_on_compose[OF *])
apply (rule_tac[!] continuous_on_subset[OF _ isc])
apply (rule assms)+
done
have *:
unfolding vec_eq_iff by auto
show
and
and
and
unfolding o_def iscale_def
using assms
qed
then obtain s t where st:

by auto
show thesis
apply (rule_tac z =  in that)
using st
unfolding o_def path_image_def image_iff
apply -
apply (rule_tac x= in bexI)
prefer 3
apply (rule_tac x= in bexI)
using isc[unfolded subset_eq, rule_format]
apply auto
done
qed

lemma fashoda:
fixes b ::
assumes
and
and
and
and
and
and
and
obtains z where  and
proof -
fix P Q S
presume   and  and
then show thesis
by auto
next
have
using assms(3) using path_image_nonempty[of f] by auto
then have
unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
then show
unfolding less_eq_vec_def forall_2 by auto
next
assume as:
have
apply (rule connected_ivt_component_cart)
apply (rule connected_path_image assms)+
apply (rule pathstart_in_path_image)
apply (rule pathfinish_in_path_image)
unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of ]
unfolding pathstart_def
apply (auto simp add: less_eq_vec_def mem_box_cart)
done
then obtain z ::  where z:   ..
have
using z(1) assms(4)
unfolding path_image_def
by blast
then have
unfolding vec_eq_iff forall_2
unfolding z(2) pathstart_def
using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of  1]
unfolding mem_box_cart
apply (erule_tac x=1 in allE)
using as
apply auto
done
then show thesis
apply -
apply (rule that[OF _ z(1)])
unfolding path_image_def
apply auto
done
next
assume as:
have
apply (rule connected_ivt_component_cart)
apply (rule connected_path_image assms)+
apply (rule pathstart_in_path_image)
apply (rule pathfinish_in_path_image)
unfolding assms
using assms(4)[unfolded path_image_def subset_eq,rule_format,of ]
unfolding pathstart_def
apply (auto simp add: less_eq_vec_def mem_box_cart)
done
then obtain z where z:   ..
have
using z(1) assms(3)
unfolding path_image_def
by blast
then have
unfolding vec_eq_iff forall_2
unfolding z(2) pathstart_def
using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of  2]
unfolding mem_box_cart
apply (erule_tac x=2 in allE)
using as
apply auto
done
then show thesis
apply -
apply (rule that[OF z(1)])
unfolding path_image_def
apply auto
done
next
assume as:
have int_nem:
unfolding interval_eq_empty_cart by auto
obtain z ::  where z:

apply (rule fashoda_unit_path[of  ])
unfolding path_def path_image_def pathstart_def pathfinish_def
apply (rule_tac[1-2] continuous_on_compose)
apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
unfolding subset_eq
apply(rule_tac[1-2] ballI)
proof -
fix x
assume
then obtain y where y:

unfolding image_iff ..
show
unfolding y o_def
apply (rule in_interval_interval_bij)
using y(1)
using assms(3)[unfolded path_image_def subset_eq] int_nem
apply auto
done
next
fix x
assume
then obtain y where y:

unfolding image_iff ..
show
unfolding y o_def
apply (rule in_interval_interval_bij)
using y(1)
using assms(4)[unfolded path_image_def subset_eq] int_nem
apply auto
done
next
show
and
and
and
using assms as
by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
qed
from z(1) obtain zf where zf:

unfolding image_iff ..
from z(2) obtain zg where zg:

unfolding image_iff ..
have *:
unfolding forall_2
using as
by auto
show thesis
proof (rule_tac z= in that)
show
using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def)
show
using zg by (simp add: interval_bij_bij_cart[OF *] path_image_def)
qed
qed

subsection

lemma segment_vertical:
fixes a ::
assumes
shows
(is )
proof -
let ?L =
{
presume  and
then show ?thesis
unfolding closed_segment_def mem_Collect_eq
unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
by blast
}
{
assume ?L
then obtain u where u:

by blast
{ fix b a
assume
then have
then have
apply (drule_tac mult_left_less_imp_less)
using u
apply auto
done
then have
apply -
apply (rule mult_left_mono[OF _ u(3)])
using u(3-4)
done
} note * = this
{
fix a b
assume
then have
apply -
apply (rule mult_left_mono)
apply (drule mult_left_less_imp_less)
using u
apply auto
done
then have
} note ** = this
then show ?R
unfolding u assms
using u
by (auto simp add:field_simps not_le intro: * **)
}
{
assume ?R
then show ?L
proof (cases )
case True
then show ?L
apply (rule_tac x= in exI)
unfolding assms True using  apply (auto simp add: field_simps)
done
next
case False
then show ?L
apply (rule_tac x= in exI)
unfolding assms using  apply (auto simp add: field_simps)
done
qed
}
qed

lemma segment_horizontal:
fixes a ::
assumes
shows
(is )
proof -
let ?L =
{
presume  and
then show ?thesis
unfolding closed_segment_def mem_Collect_eq
unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
by blast
}
{
assume ?L
then obtain u where u:

by blast
{
fix b a
assume
then have
then have
apply (drule_tac mult_left_less_imp_less)
using u
apply auto
done
then have
apply -
apply (rule mult_left_mono[OF _ u(3)])
using u(3-4)
done
} note * = this
{
fix a b
assume
then have
apply -
apply (rule mult_left_mono)
apply (drule mult_left_less_imp_less)
using u
apply auto
done
then have
} note ** = this
then show ?R
unfolding u assms
using u
by (auto simp add: field_simps not_le intro: * **)
}
{
assume ?R
then show ?L
proof (cases )
case True
then show ?L
apply (rule_tac x= in exI)
unfolding assms True
using
done
next
case False
then show ?L
apply (rule_tac x= in exI)
unfolding assms
using
done
qed
}
qed

subsection

lemma fashoda_interlace:
fixes a ::
assumes
and
and paf:
and pag:
and
and
and
and
and
and
and
obtains z where  and
proof -
have
using path_image_nonempty[of f] using assms(3) by auto
note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
have
and
and
and
using pathstart_in_path_image pathfinish_in_path_image
using assms(3-4)
by auto
note startfin = this[unfolded mem_box_cart forall_2]
let ?P1 =
let ?P2 =
let ?a =
let ?b =
have P1P2:
using assms(1-2)
have abab:
unfolding interval_cbox_cart[symmetric]
by (auto simp add:less_eq_vec_def forall_2 vector_2)
obtain z where

apply (rule fashoda[of ?P1 ?P2 ?a ?b])
unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
proof -
show  and
using assms by auto
show
unfolding P1P2 path_image_linepath using startfin paf pag
by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2)
show
and
and
and
qed
note z=this[unfolded P1P2 path_image_linepath]
show thesis
proof (rule that[of z])
have
proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
case prems: 1
have
using assms(3) pathfinish_in_path_image[of f] by auto
then have
unfolding mem_box_cart forall_2 by auto
then have
using prems(2)
using assms ab
moreover have
using assms(3) pathstart_in_path_image[of f]
by auto
then have
unfolding mem_box_cart forall_2
by auto
then have
using prems(2) using assms ab
ultimately have *:
using prems(1) by auto
have
using prems(2) assms ab
by (auto simp add: field_simps *)
moreover have
using assms(4) pathstart_in_path_image[of g]
by auto
note this[unfolded mem_box_cart forall_2]
then have
using prems(1) assms ab
by (auto simp add: field_simps *)
ultimately have
using prems(2)  unfolding * assms by (auto simp add: field_simps)
then show False
unfolding * using ab by auto
qed
then have
using z unfolding Un_iff by blast
then have z':
using assms(3-4) by auto
have
unfolding vec_eq_iff forall_2 assms
by auto
with z' show
using z(1)
unfolding Un_iff mem_box_cart forall_2
by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
have
unfolding vec_eq_iff forall_2 assms
by auto
with z' show
using z(2)
unfolding Un_iff mem_box_cart forall_2
by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
qed
qed

end