Theory Smooth_Paths
section ‹Smooth paths›
theory Smooth_Paths
imports Retracts
begin
subsection ‹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
by (intro path_connected_complement_homeomorphic_convex_compact) (auto simp: assms)
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
then have "connected (- path_image γ)"
by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym assms connected_arc_complement not_less_eq_eq)
then
show ?thesis
by (simp add: assms bounded_arc_image inside_bounded_complement_connected_empty)
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:
assumes "continuous_on {0..1} (g1 +++ g2)"
shows "continuous_on {0..1} g1"
proof (rule continuous_on_eq)
have "continuous_on {0..1/2} (g1 +++ g2)"
using assms continuous_on_subset split_01 by auto
then show "continuous_on {0..1} (g1 +++ g2 ∘ (*) (inverse 2))"
by (intro continuous_intros) force
qed (auto simp: joinpaths_def)
lemma continuous_on_joinpaths_D2:
"⟦continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2⟧ ⟹ continuous_on {0..1} g2"
using path_def path_join by blast
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
unfolding joinpaths_def
by (intro 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))"
using coDhalf
apply (intro continuous_intros)
by (simp add: scaleR_conv_of_real image_set_diff image_image)
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
unfolding 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
by (meson C1_differentiable_on_eq con_g2 finite_imageI finite_insert g2D piecewise_C1_differentiable_on_def)
qed
subsection ‹Valid paths, and their start and finish›
definition 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_translation_eq: "valid_path ((+)d ∘ p) ⟷ valid_path p"
by (simp add: valid_path_def piecewise_C1_differentiable_on_translation_eq)
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
by (metis C1_differentiable_on_eq DiffD1 der g_diff imageI path_image_def that
vector_derivative_chain_at_general)
qed
ultimately have "f ∘ g C1_differentiable_on {0..1} - S"
using C1_differentiable_on_eq by blast
moreover have "path (f ∘ g)"
using der
by (simp add: path_continuous_image[OF valid_path_imp_path[OF ‹valid_path g›]] 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
unfolding valid_path_def continuous_on_joinpaths joinpaths_def
by (intro piecewise_C1_differentiable_cases) (auto simp: o_def)
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
unfolding valid_path_def shiftpath_alt_def
apply (intro piecewise_C1_differentiable_cases)
apply (simp_all add: add.commute)
apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one])
apply (force 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"
by (simp add: has_vector_derivative_linepath_within vector_derivative_at_within_ivl)
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)"
using C1_differentiable_on_eq piecewise_C1_differentiable_on_def valid_path_def by fastforce
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
let ?f = "λx. ((v-u) * x + u)"
have "(g ∘ ?f) piecewise_C1_differentiable_on {0..1}"
proof (rule piecewise_C1_differentiable_compose)
show "?f piecewise_C1_differentiable_on {0..1}"
by (simp add: C1_differentiable_imp_piecewise)
have "g piecewise_C1_differentiable_on (if u ≤ v then {u..v} else {v..u})"
using assms piecewise_C1_differentiable_on_subset valid_path_def by force
then show "g piecewise_C1_differentiable_on ?f ` {0..1}"
by (simp add: image_affinity_atLeastAtMost split: if_split_asm)
show "⋀x. finite ({0..1} ∩ ?f -` {x})"
using False
by (simp add: Int_commute [of "{0..1}"] inj_on_def crossproduct_eq finite_vimage_IntI)
qed
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)
lemma linear_image_valid_path:
fixes p :: "real ⇒ 'a :: euclidean_space"
assumes "valid_path p" "linear f"
shows "valid_path (f ∘ p)"
unfolding valid_path_def piecewise_C1_differentiable_on_def
proof (intro conjI)
from assms have "path p"
by (simp add: valid_path_imp_path)
thus "continuous_on {0..1} (f ∘ p)"
unfolding o_def path_def by (intro linear_continuous_on_compose[OF _ assms(2)])
from assms(1) obtain S where S: "finite S" "p C1_differentiable_on {0..1} - S"
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
from S(2) obtain p' :: "real ⇒ 'a"
where p': "⋀x. x ∈ {0..1} - S ⟹ (p has_vector_derivative p' x) (at x)"
"continuous_on ({0..1} - S) p'"
by (fastforce simp: C1_differentiable_on_def)
have "(f ∘ p has_vector_derivative f (p' x)) (at x)" if "x ∈ {0..1} - S" for x
by (rule vector_derivative_diff_chain_within [OF p'(1)[OF that]]
linear_imp_has_derivative assms)+
moreover have "continuous_on ({0..1} - S) (λx. f (p' x))"
by (rule linear_continuous_on_compose [OF p'(2) assms(2)])
ultimately have "f ∘ p C1_differentiable_on {0..1} - S"
unfolding C1_differentiable_on_def by (intro exI[of _ "λx. f (p' x)"]) fast
thus "∃S. finite S ∧ f ∘ p C1_differentiable_on {0..1} - S"
using ‹finite S› by blast
qed
lemma valid_path_times:
fixes γ::"real ⇒ 'a ::real_normed_field"
assumes "c≠0"
shows "valid_path ((*) c ∘ γ) = valid_path γ"
proof
assume "valid_path ((*) c ∘ γ)"
then have "valid_path ((*) (1/c) ∘ ((*) c ∘ γ))"
by (simp add: valid_path_compose)
then show "valid_path γ"
unfolding comp_def using ‹c≠0› by auto
next
assume "valid_path γ"
then show "valid_path ((*) c ∘ γ)"
by (simp add: valid_path_compose)
qed
lemma path_compose_cnj_iff [simp]: "path (cnj ∘ p) ⟷ path p"
proof -
have "path (cnj ∘ p)" if "path p" for p
by (intro path_continuous_image continuous_intros that)
from this[of p] and this[of "cnj ∘ p"] show ?thesis
by (auto simp: o_def)
qed
lemma valid_path_cnj:
fixes g::"real ⇒ complex"
shows "valid_path (cnj ∘ g) = valid_path g"
proof
show valid:"valid_path (cnj ∘ g)" if "valid_path g" for 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 g_diff':"g differentiable at t" when "t∈{0..1} - S" for t
by (meson C1_differentiable_on_eq ‹g C1_differentiable_on {0..1} - S› that)
then have "(cnj ∘ g) differentiable at t" when "t∈{0..1} - S" for t
using bounded_linear_cnj bounded_linear_imp_differentiable differentiable_chain_at that by blast
moreover have "continuous_on ({0..1} - S)
(λx. vector_derivative (cnj ∘ g) (at x))"
proof -
have "continuous_on ({0..1} - S)
(λx. vector_derivative (cnj ∘ g) (at x))
= continuous_on ({0..1} - S)
(λx. cnj (vector_derivative g (at x)))"
apply (rule continuous_on_cong[OF refl])
unfolding comp_def using g_diff'
using has_vector_derivative_cnj vector_derivative_at vector_derivative_works by blast
also have "…"
apply (intro continuous_intros)
using C1_differentiable_on_eq g_diff by blast
finally show ?thesis .
qed
ultimately have "cnj ∘ g C1_differentiable_on {0..1} - S"
using C1_differentiable_on_eq by blast
moreover have "path (cnj ∘ g)"
apply (rule path_continuous_image[OF valid_path_imp_path[OF ‹valid_path g›]])
by (intro continuous_intros)
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using ‹finite S› by auto
qed
from this[of "cnj o g"]
show "valid_path (cnj ∘ g) ⟹ valid_path g"
unfolding comp_def by simp
qed
end