(* Material originally from HOL Light, ported by Larry Paulson, moved here by Manuel Eberl *) section✐‹tag unimportant› ‹Smooth paths› theory Smooth_Paths imports Retracts begin subsection✐‹tag unimportant› ‹Homeomorphisms of arc images› lemma path_connected_arc_complement: fixes γ :: "real ⇒ 'a::euclidean_space" assumes "arc γ" "2 ≤ DIM('a)" shows "path_connected(- path_image γ)" proof - have "path_image γ homeomorphic {0..1::real}" by (simp add: assms homeomorphic_arc_image_interval) then show ?thesis apply (rule path_connected_complement_homeomorphic_convex_compact) apply (auto simp: assms) done qed lemma connected_arc_complement: fixes γ :: "real ⇒ 'a::euclidean_space" assumes "arc γ" "2 ≤ DIM('a)" shows "connected(- path_image γ)" by (simp add: assms path_connected_arc_complement path_connected_imp_connected) lemma inside_arc_empty: fixes γ :: "real ⇒ 'a::euclidean_space" assumes "arc γ" shows "inside(path_image γ) = {}" proof (cases "DIM('a) = 1") case True then show ?thesis using assms connected_arc_image connected_convex_1_gen inside_convex by blast next case False show ?thesis proof (rule inside_bounded_complement_connected_empty) show "connected (- path_image γ)" apply (rule connected_arc_complement [OF assms]) using False by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym) show "bounded (path_image γ)" by (simp add: assms bounded_arc_image) qed qed lemma inside_simple_curve_imp_closed: fixes γ :: "real ⇒ 'a::euclidean_space" shows "⟦simple_path γ; x ∈ inside(path_image γ)⟧ ⟹ pathfinish γ = pathstart γ" using arc_simple_path inside_arc_empty by blast subsection ‹Piecewise differentiability of paths› lemma continuous_on_joinpaths_D1: "continuous_on {0..1} (g1 +++ g2) ⟹ continuous_on {0..1} g1" apply (rule continuous_on_eq [of _ "(g1 +++ g2) ∘ ((*)(inverse 2))"]) apply (rule continuous_intros | simp)+ apply (auto elim!: continuous_on_subset simp: joinpaths_def) done lemma continuous_on_joinpaths_D2: "⟦continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2⟧ ⟹ continuous_on {0..1} g2" apply (rule continuous_on_eq [of _ "(g1 +++ g2) ∘ (λx. inverse 2*x + 1/2)"]) apply (rule continuous_intros | simp)+ apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) done lemma piecewise_differentiable_D1: assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" shows "g1 piecewise_differentiable_on {0..1}" proof - obtain S where cont: "continuous_on {0..1} g1" and "finite S" and S: "⋀x. x ∈ {0..1} - S ⟹ g1 +++ g2 differentiable at x within {0..1}" using assms unfolding piecewise_differentiable_on_def by (blast dest!: continuous_on_joinpaths_D1) show ?thesis unfolding piecewise_differentiable_on_def proof (intro exI conjI ballI cont) show "finite (insert 1 (((*)2) ` S))" by (simp add: ‹finite S›) show "g1 differentiable at x within {0..1}" if "x ∈ {0..1} - insert 1 ((*) 2 ` S)" for x proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within) have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}" by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+ then show "g1 +++ g2 ∘ (*) (inverse 2) differentiable at x within {0..1}" using image_affinity_atLeastAtMost_div [of 2 0 "0::real" 1] by (auto intro: differentiable_chain_within) qed (use that in ‹auto simp: joinpaths_def›) qed qed lemma piecewise_differentiable_D2: assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2" shows "g2 piecewise_differentiable_on {0..1}" proof - have [simp]: "g1 1 = g2 0" using eq by (simp add: pathfinish_def pathstart_def) obtain S where cont: "continuous_on {0..1} g2" and "finite S" and S: "⋀x. x ∈ {0..1} - S ⟹ g1 +++ g2 differentiable at x within {0..1}" using assms unfolding piecewise_differentiable_on_def by (blast dest!: continuous_on_joinpaths_D2) show ?thesis unfolding piecewise_differentiable_on_def proof (intro exI conjI ballI cont) show "finite (insert 0 ((λx. 2*x-1)`S))" by (simp add: ‹finite S›) show "g2 differentiable at x within {0..1}" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1)`S)" for x proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within) have x2: "(x + 1) / 2 ∉ S" using that apply (clarsimp simp: image_iff) by (metis add.commute add_diff_cancel_left' mult_2 field_sum_of_halves) have "g1 +++ g2 ∘ (λx. (x+1) / 2) differentiable at x within {0..1}" by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+ then show "g1 +++ g2 ∘ (λx. (x+1) / 2) differentiable at x within {0..1}" by (auto intro: differentiable_chain_within) show "(g1 +++ g2 ∘ (λx. (x + 1) / 2)) x' = g2 x'" if "x' ∈ {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x' proof - have [simp]: "(2*x'+2)/2 = x'+1" by (simp add: field_split_simps) show ?thesis using that by (auto simp: joinpaths_def) qed qed (use that in ‹auto simp: joinpaths_def›) qed qed lemma piecewise_C1_differentiable_D1: fixes g1 :: "real ⇒ 'a::real_normed_field" assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" shows "g1 piecewise_C1_differentiable_on {0..1}" proof - obtain S where "finite S" and co12: "continuous_on ({0..1} - S) (λx. vector_derivative (g1 +++ g2) (at x))" and g12D: "∀x∈{0..1} - S. g1 +++ g2 differentiable at x" using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) have g1D: "g1 differentiable at x" if "x ∈ {0..1} - insert 1 ((*) 2 ` S)" for x proof (rule differentiable_transform_within) show "g1 +++ g2 ∘ (*) (inverse 2) differentiable at x" using that g12D apply (simp only: joinpaths_def) by (rule differentiable_chain_at derivative_intros | force)+ show "⋀x'. ⟦dist x' x < dist (x/2) (1/2)⟧ ⟹ (g1 +++ g2 ∘ (*) (inverse 2)) x' = g1 x'" using that by (auto simp: dist_real_def joinpaths_def) qed (use that in ‹auto simp: dist_real_def›) have [simp]: "vector_derivative (g1 ∘ (*) 2) (at (x/2)) = 2 *⇩_{R}vector_derivative g1 (at x)" if "x ∈ {0..1} - insert 1 ((*) 2 ` S)" for x apply (subst vector_derivative_chain_at) using that apply (rule derivative_eq_intros g1D | simp)+ done have "continuous_on ({0..1/2} - insert (1/2) S) (λx. vector_derivative (g1 +++ g2) (at x))" using co12 by (rule continuous_on_subset) force then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (λx. vector_derivative (g1 ∘ (*)2) (at x))" proof (rule continuous_on_eq [OF _ vector_derivative_at]) show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 ∘ (*) 2) (at x)) (at x)" if "x ∈ {0..1/2} - insert (1/2) S" for x proof (rule has_vector_derivative_transform_within) show "(g1 ∘ (*) 2 has_vector_derivative vector_derivative (g1 ∘ (*) 2) (at x)) (at x)" using that by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric]) show "⋀x'. ⟦dist x' x < dist x (1/2)⟧ ⟹ (g1 ∘ (*) 2) x' = (g1 +++ g2) x'" using that by (auto simp: dist_norm joinpaths_def) qed (use that in ‹auto simp: dist_norm›) qed have "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) ((λx. 1/2 * vector_derivative (g1 ∘ (*)2) (at x)) ∘ (*)(1/2))" apply (rule continuous_intros)+ using coDhalf apply (simp add: scaleR_conv_of_real image_set_diff image_image) done then have con_g1: "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) (λx. vector_derivative g1 (at x))" by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) have "continuous_on {0..1} g1" using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast with ‹finite S› show ?thesis apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) apply (rule_tac x="insert 1 (((*)2)`S)" in exI) apply (simp add: g1D con_g1) done qed lemma piecewise_C1_differentiable_D2: fixes g2 :: "real ⇒ 'a::real_normed_field" assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2" shows "g2 piecewise_C1_differentiable_on {0..1}" proof - obtain S where "finite S" and co12: "continuous_on ({0..1} - S) (λx. vector_derivative (g1 +++ g2) (at x))" and g12D: "∀x∈{0..1} - S. g1 +++ g2 differentiable at x" using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) have g2D: "g2 differentiable at x" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1) ` S)" for x proof (rule differentiable_transform_within) show "g1 +++ g2 ∘ (λx. (x + 1) / 2) differentiable at x" using g12D that apply (simp only: joinpaths_def) apply (drule_tac x= "(x+1) / 2" in bspec, force simp: field_split_simps) apply (rule differentiable_chain_at derivative_intros | force)+ done show "⋀x'. dist x' x < dist ((x + 1) / 2) (1/2) ⟹ (g1 +++ g2 ∘ (λx. (x + 1) / 2)) x' = g2 x'" using that by (auto simp: dist_real_def joinpaths_def field_simps) qed (use that in ‹auto simp: dist_norm›) have [simp]: "vector_derivative (g2 ∘ (λx. 2*x-1)) (at ((x+1)/2)) = 2 *⇩_{R}vector_derivative g2 (at x)" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1) ` S)" for x using that by (auto simp: vector_derivative_chain_at field_split_simps g2D) have "continuous_on ({1/2..1} - insert (1/2) S) (λx. vector_derivative (g1 +++ g2) (at x))" using co12 by (rule continuous_on_subset) force then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (λx. vector_derivative (g2 ∘ (λx. 2*x-1)) (at x))" proof (rule continuous_on_eq [OF _ vector_derivative_at]) show "(g1 +++ g2 has_vector_derivative vector_derivative (g2 ∘ (λx. 2 * x - 1)) (at x)) (at x)" if "x ∈ {1 / 2..1} - insert (1 / 2) S" for x proof (rule_tac f="g2 ∘ (λx. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within) show "(g2 ∘ (λx. 2 * x - 1) has_vector_derivative vector_derivative (g2 ∘ (λx. 2 * x - 1)) (at x)) (at x)" using that by (force intro: g2D differentiable_chain_at simp: vector_derivative_works [symmetric]) show "⋀x'. ⟦dist x' x < dist (3 / 4) ((x + 1) / 2)⟧ ⟹ (g2 ∘ (λx. 2 * x - 1)) x' = (g1 +++ g2) x'" using that by (auto simp: dist_norm joinpaths_def add_divide_distrib) qed (use that in ‹auto simp: dist_norm›) qed have [simp]: "((λx. (x+1) / 2) ` ({0..1} - insert 0 ((λx. 2 * x - 1) ` S))) = ({1/2..1} - insert (1/2) S)" apply (simp add: image_set_diff inj_on_def image_image) apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib) done have "continuous_on ({0..1} - insert 0 ((λx. 2*x-1) ` S)) ((λx. 1/2 * vector_derivative (g2 ∘ (λx. 2*x-1)) (at x)) ∘ (λx. (x+1)/2))" by (rule continuous_intros | simp add: coDhalf)+ then have con_g2: "continuous_on ({0..1} - insert 0 ((λx. 2*x-1) ` S)) (λx. vector_derivative g2 (at x))" by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) have "continuous_on {0..1} g2" using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast with ‹finite S› show ?thesis apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) apply (rule_tac x="insert 0 ((λx. 2 * x - 1) ` S)" in exI) apply (simp add: g2D con_g2) done qed subsection ‹Valid paths, and their start and finish› definition✐‹tag important› valid_path :: "(real ⇒ 'a :: real_normed_vector) ⇒ bool" where "valid_path f ≡ f piecewise_C1_differentiable_on {0..1::real}" definition closed_path :: "(real ⇒ 'a :: real_normed_vector) ⇒ bool" where "closed_path g ≡ g 0 = g 1" text‹In particular, all results for paths apply› lemma valid_path_imp_path: "valid_path g ⟹ path g" by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def) lemma connected_valid_path_image: "valid_path g ⟹ connected(path_image g)" by (metis connected_path_image valid_path_imp_path) lemma compact_valid_path_image: "valid_path g ⟹ compact(path_image g)" by (metis compact_path_image valid_path_imp_path) lemma bounded_valid_path_image: "valid_path g ⟹ bounded(path_image g)" by (metis bounded_path_image valid_path_imp_path) lemma closed_valid_path_image: "valid_path g ⟹ closed(path_image g)" by (metis closed_path_image valid_path_imp_path) lemma valid_path_compose: assumes "valid_path g" and der: "⋀x. x ∈ path_image g ⟹ f field_differentiable (at x)" and con: "continuous_on (path_image g) (deriv f)" shows "valid_path (f ∘ g)" proof - obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S" using ‹valid_path g› unfolding valid_path_def piecewise_C1_differentiable_on_def by auto have "f ∘ g differentiable at t" when "t∈{0..1} - S" for t proof (rule differentiable_chain_at) show "g differentiable at t" using ‹valid_path g› by (meson C1_differentiable_on_eq ‹g C1_differentiable_on {0..1} - S› that) next have "g t∈path_image g" using that DiffD1 image_eqI path_image_def by metis then show "f differentiable at (g t)" using der[THEN field_differentiable_imp_differentiable] by auto qed moreover have "continuous_on ({0..1} - S) (λx. vector_derivative (f ∘ g) (at x))" proof (rule continuous_on_eq [where f = "λx. vector_derivative g (at x) * deriv f (g x)"], rule continuous_intros) show "continuous_on ({0..1} - S) (λx. vector_derivative g (at x))" using g_diff C1_differentiable_on_eq by auto next have "continuous_on {0..1} (λx. deriv f (g x))" using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] ‹valid_path g› piecewise_C1_differentiable_on_def valid_path_def by blast then show "continuous_on ({0..1} - S) (λx. deriv f (g x))" using continuous_on_subset by blast next show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f ∘ g) (at t)" when "t ∈ {0..1} - S" for t proof (rule vector_derivative_chain_at_general[symmetric]) show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that) next have "g t∈path_image g" using that DiffD1 image_eqI path_image_def by metis then show "f field_differentiable at (g t)" using der by auto qed qed ultimately have "f ∘ g C1_differentiable_on {0..1} - S" using C1_differentiable_on_eq by blast moreover have "path (f ∘ g)" apply (rule path_continuous_image[OF valid_path_imp_path[OF ‹valid_path g›]]) using der by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at) ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def using ‹finite S› by auto qed lemma valid_path_uminus_comp[simp]: fixes g::"real ⇒ 'a ::real_normed_field" shows "valid_path (uminus ∘ g) ⟷ valid_path g" proof show "valid_path g ⟹ valid_path (uminus ∘ g)" for g::"real ⇒ 'a" by (auto intro!: valid_path_compose derivative_intros) then show "valid_path g" when "valid_path (uminus ∘ g)" by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that) qed lemma valid_path_offset[simp]: shows "valid_path (λt. g t - z) ⟷ valid_path g" proof show *: "valid_path (g::real⇒'a) ⟹ valid_path (λt. g t - z)" for g z unfolding valid_path_def by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff) show "valid_path (λt. g t - z) ⟹ valid_path g" using *[of "λt. g t - z" "-z",simplified] . qed lemma valid_path_imp_reverse: assumes "valid_path g" shows "valid_path(reversepath g)" proof - obtain S where "finite S" and S: "g C1_differentiable_on ({0..1} - S)" using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) then have "finite ((-) 1 ` S)" by auto moreover have "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` S))" unfolding reversepath_def apply (rule C1_differentiable_compose [of "λx::real. 1-x" _ g, unfolded o_def]) using S by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq elim!: continuous_on_subset)+ ultimately show ?thesis using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric]) qed lemma valid_path_reversepath [simp]: "valid_path(reversepath g) ⟷ valid_path g" using valid_path_imp_reverse by force lemma valid_path_join: assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2" shows "valid_path(g1 +++ g2)" proof - have "g1 1 = g2 0" using assms by (auto simp: pathfinish_def pathstart_def) moreover have "(g1 ∘ (λx. 2*x)) piecewise_C1_differentiable_on {0..1/2}" apply (rule piecewise_C1_differentiable_compose) using assms apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths) apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI) done moreover have "(g2 ∘ (λx. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}" apply (rule piecewise_C1_differentiable_compose) using assms unfolding valid_path_def piecewise_C1_differentiable_on_def by (auto intro!: continuous_intros finite_vimageI [where h = "(λx. 2*x - 1)"] inj_onI simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths) ultimately show ?thesis apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def) apply (rule piecewise_C1_differentiable_cases) apply (auto simp: o_def) done qed lemma valid_path_join_D1: fixes g1 :: "real ⇒ 'a::real_normed_field" shows "valid_path (g1 +++ g2) ⟹ valid_path g1" unfolding valid_path_def by (rule piecewise_C1_differentiable_D1) lemma valid_path_join_D2: fixes g2 :: "real ⇒ 'a::real_normed_field" shows "⟦valid_path (g1 +++ g2); pathfinish g1 = pathstart g2⟧ ⟹ valid_path g2" unfolding valid_path_def by (rule piecewise_C1_differentiable_D2) lemma valid_path_join_eq [simp]: fixes g2 :: "real ⇒ 'a::real_normed_field" shows "pathfinish g1 = pathstart g2 ⟹ (valid_path(g1 +++ g2) ⟷ valid_path g1 ∧ valid_path g2)" using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast lemma valid_path_shiftpath [intro]: assumes "valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}" shows "valid_path(shiftpath a g)" using assms apply (auto simp: valid_path_def shiftpath_alt_def) apply (rule piecewise_C1_differentiable_cases) apply (auto simp: algebra_simps) apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) apply (rule piecewise_C1_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps]) apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) done lemma vector_derivative_linepath_within: "x ∈ {0..1} ⟹ vector_derivative (linepath a b) (at x within {0..1}) = b - a" apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified]) apply (auto simp: has_vector_derivative_linepath_within) done lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b - a" by (simp add: has_vector_derivative_linepath_within vector_derivative_at) lemma valid_path_linepath [iff]: "valid_path (linepath a b)" apply (simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_on_linepath) apply (rule_tac x="{}" in exI) apply (simp add: differentiable_on_def differentiable_def) using has_vector_derivative_def has_vector_derivative_linepath_within apply (fastforce simp add: continuous_on_eq_continuous_within) done lemma valid_path_subpath: fixes g :: "real ⇒ 'a :: real_normed_vector" assumes "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}" shows "valid_path(subpath u v g)" proof (cases "v=u") case True then show ?thesis unfolding valid_path_def subpath_def by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise) next case False have "(g ∘ (λx. ((v-u) * x + u))) piecewise_C1_differentiable_on {0..1}" apply (rule piecewise_C1_differentiable_compose) apply (simp add: C1_differentiable_imp_piecewise) apply (simp add: image_affinity_atLeastAtMost) using assms False apply (auto simp: algebra_simps valid_path_def piecewise_C1_differentiable_on_subset) apply (subst Int_commute) apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI) done then show ?thesis by (auto simp: o_def valid_path_def subpath_def) qed lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)" by (simp add: Let_def rectpath_def) end