1061 subsection \<open>Shift Path to Start at Some Given Point\<close> |
1061 subsection \<open>Shift Path to Start at Some Given Point\<close> |
1062 |
1062 |
1063 definition\<^marker>\<open>tag important\<close> shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a" |
1063 definition\<^marker>\<open>tag important\<close> shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a" |
1064 where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))" |
1064 where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))" |
1065 |
1065 |
|
1066 lemma shiftpath_alt_def: "shiftpath a f = (\<lambda>x. if x \<le> 1-a then f (a + x) else f (a + x - 1))" |
|
1067 by (auto simp: shiftpath_def) |
|
1068 |
1066 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a" |
1069 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a" |
1067 unfolding pathstart_def shiftpath_def by auto |
1070 unfolding pathstart_def shiftpath_def by auto |
1068 |
1071 |
1069 lemma pathfinish_shiftpath: |
1072 lemma pathfinish_shiftpath: |
1070 assumes "0 \<le> a" |
1073 assumes "0 \<le> a" |
1270 qed |
1273 qed |
1271 |
1274 |
1272 lemma linepath_le_1: |
1275 lemma linepath_le_1: |
1273 fixes a::"'a::linordered_idom" shows "\<lbrakk>a \<le> 1; b \<le> 1; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> (1 - u) * a + u * b \<le> 1" |
1276 fixes a::"'a::linordered_idom" shows "\<lbrakk>a \<le> 1; b \<le> 1; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> (1 - u) * a + u * b \<le> 1" |
1274 using mult_left_le [of a "1-u"] mult_left_le [of b u] by auto |
1277 using mult_left_le [of a "1-u"] mult_left_le [of b u] by auto |
|
1278 |
|
1279 lemma linepath_in_path: |
|
1280 shows "x \<in> {0..1} \<Longrightarrow> linepath a b x \<in> closed_segment a b" |
|
1281 by (auto simp: segment linepath_def) |
|
1282 |
|
1283 lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b" |
|
1284 by (auto simp: segment linepath_def) |
|
1285 |
|
1286 lemma linepath_in_convex_hull: |
|
1287 fixes x::real |
|
1288 assumes a: "a \<in> convex hull s" |
|
1289 and b: "b \<in> convex hull s" |
|
1290 and x: "0\<le>x" "x\<le>1" |
|
1291 shows "linepath a b x \<in> convex hull s" |
|
1292 apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD]) |
|
1293 using x |
|
1294 apply (auto simp: linepath_image_01 [symmetric]) |
|
1295 done |
|
1296 |
|
1297 lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b" |
|
1298 by (simp add: linepath_def) |
|
1299 |
|
1300 lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0" |
|
1301 by (simp add: linepath_def) |
|
1302 |
|
1303 lemma bounded_linear_linepath: |
|
1304 assumes "bounded_linear f" |
|
1305 shows "f (linepath a b x) = linepath (f a) (f b) x" |
|
1306 proof - |
|
1307 interpret f: bounded_linear f by fact |
|
1308 show ?thesis by (simp add: linepath_def f.add f.scale) |
|
1309 qed |
|
1310 |
|
1311 lemma bounded_linear_linepath': |
|
1312 assumes "bounded_linear f" |
|
1313 shows "f \<circ> linepath a b = linepath (f a) (f b)" |
|
1314 using bounded_linear_linepath[OF assms] by (simp add: fun_eq_iff) |
|
1315 |
|
1316 lemma linepath_cnj': "cnj \<circ> linepath a b = linepath (cnj a) (cnj b)" |
|
1317 by (simp add: linepath_def fun_eq_iff) |
|
1318 |
|
1319 lemma differentiable_linepath [intro]: "linepath a b differentiable at x within A" |
|
1320 by (auto simp: linepath_def) |
|
1321 |
|
1322 lemma has_vector_derivative_linepath_within: |
|
1323 "(linepath a b has_vector_derivative (b - a)) (at x within s)" |
|
1324 apply (simp add: linepath_def has_vector_derivative_def algebra_simps) |
|
1325 apply (rule derivative_eq_intros | simp)+ |
|
1326 done |
1275 |
1327 |
1276 |
1328 |
1277 subsection\<^marker>\<open>tag unimportant\<close>\<open>Segments via convex hulls\<close> |
1329 subsection\<^marker>\<open>tag unimportant\<close>\<open>Segments via convex hulls\<close> |
1278 |
1330 |
1279 lemma segments_subset_convex_hull: |
1331 lemma segments_subset_convex_hull: |
4001 fixes f :: "'a::topological_space \<Rightarrow> real" |
4053 fixes f :: "'a::topological_space \<Rightarrow> real" |
4002 assumes "path_connected S" "continuous_on S f" "f ` S = T" "inj_on f S" |
4054 assumes "path_connected S" "continuous_on S f" "f ` S = T" "inj_on f S" |
4003 shows "\<exists>g. homeomorphism S T f g" |
4055 shows "\<exists>g. homeomorphism S T f g" |
4004 using assms injective_into_1d_eq_homeomorphism by blast |
4056 using assms injective_into_1d_eq_homeomorphism by blast |
4005 |
4057 |
|
4058 |
|
4059 subsection\<^marker>\<open>tag unimportant\<close> \<open>Rectangular paths\<close> |
|
4060 |
|
4061 definition\<^marker>\<open>tag unimportant\<close> rectpath where |
|
4062 "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3) |
|
4063 in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)" |
|
4064 |
|
4065 lemma path_rectpath [simp, intro]: "path (rectpath a b)" |
|
4066 by (simp add: Let_def rectpath_def) |
|
4067 |
|
4068 lemma pathstart_rectpath [simp]: "pathstart (rectpath a1 a3) = a1" |
|
4069 by (simp add: rectpath_def Let_def) |
|
4070 |
|
4071 lemma pathfinish_rectpath [simp]: "pathfinish (rectpath a1 a3) = a1" |
|
4072 by (simp add: rectpath_def Let_def) |
|
4073 |
|
4074 lemma simple_path_rectpath [simp, intro]: |
|
4075 assumes "Re a1 \<noteq> Re a3" "Im a1 \<noteq> Im a3" |
|
4076 shows "simple_path (rectpath a1 a3)" |
|
4077 unfolding rectpath_def Let_def using assms |
|
4078 by (intro simple_path_join_loop arc_join arc_linepath) |
|
4079 (auto simp: complex_eq_iff path_image_join closed_segment_same_Re closed_segment_same_Im) |
|
4080 |
|
4081 lemma path_image_rectpath: |
|
4082 assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3" |
|
4083 shows "path_image (rectpath a1 a3) = |
|
4084 {z. Re z \<in> {Re a1, Re a3} \<and> Im z \<in> {Im a1..Im a3}} \<union> |
|
4085 {z. Im z \<in> {Im a1, Im a3} \<and> Re z \<in> {Re a1..Re a3}}" (is "?lhs = ?rhs") |
|
4086 proof - |
|
4087 define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)" |
|
4088 have "?lhs = closed_segment a1 a2 \<union> closed_segment a2 a3 \<union> |
|
4089 closed_segment a4 a3 \<union> closed_segment a1 a4" |
|
4090 by (simp_all add: rectpath_def Let_def path_image_join closed_segment_commute |
|
4091 a2_def a4_def Un_assoc) |
|
4092 also have "\<dots> = ?rhs" using assms |
|
4093 by (auto simp: rectpath_def Let_def path_image_join a2_def a4_def |
|
4094 closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl) |
|
4095 finally show ?thesis . |
|
4096 qed |
|
4097 |
|
4098 lemma path_image_rectpath_subset_cbox: |
|
4099 assumes "Re a \<le> Re b" "Im a \<le> Im b" |
|
4100 shows "path_image (rectpath a b) \<subseteq> cbox a b" |
|
4101 using assms by (auto simp: path_image_rectpath in_cbox_complex_iff) |
|
4102 |
|
4103 lemma path_image_rectpath_inter_box: |
|
4104 assumes "Re a \<le> Re b" "Im a \<le> Im b" |
|
4105 shows "path_image (rectpath a b) \<inter> box a b = {}" |
|
4106 using assms by (auto simp: path_image_rectpath in_box_complex_iff) |
|
4107 |
|
4108 lemma path_image_rectpath_cbox_minus_box: |
|
4109 assumes "Re a \<le> Re b" "Im a \<le> Im b" |
|
4110 shows "path_image (rectpath a b) = cbox a b - box a b" |
|
4111 using assms by (auto simp: path_image_rectpath in_cbox_complex_iff |
|
4112 in_box_complex_iff) |
|
4113 |
4006 end |
4114 end |