theory Derivs imports General_Utils begin lemma field_simp_has_vector_derivative [derivative_intros]: "(f has_field_derivative y) F ⟹ (f has_vector_derivative y) F" by (simp add: has_real_derivative_iff_has_vector_derivative) lemma continuous_on_cases_empty [continuous_intros]: "⟦closed S; continuous_on S f; ⋀x. ⟦x ∈ S; ¬ P x⟧ ⟹ f x = g x⟧ ⟹ continuous_on S (λx. if P x then f x else g x)" using continuous_on_cases [of _ "{}"] by force lemma inj_on_cases: assumes "inj_on f (Collect P ∩ S)" "inj_on g (Collect (Not ∘ P) ∩ S)" "f ` (Collect P ∩ S) ∩ g ` (Collect (Not ∘ P) ∩ S) = {}" shows "inj_on (λx. if P x then f x else g x) S" using assms by (force simp: inj_on_def) lemma inj_on_arccos: "S ⊆ {-1..1} ⟹ inj_on arccos S" by (metis atLeastAtMost_iff cos_arccos inj_onI subsetCE) lemma has_vector_derivative_componentwise_within: "(f has_vector_derivative f') (at a within S) ⟷ (∀i ∈ Basis. ((λx. f x ∙ i) has_vector_derivative (f' ∙ i)) (at a within S))" apply (simp add: has_vector_derivative_def) apply (subst has_derivative_componentwise_within) apply simp done lemma has_vector_derivative_pair_within: fixes f :: "real ⇒ 'a::euclidean_space" and g :: "real ⇒ 'b::euclidean_space" assumes "⋀u. u ∈ Basis ⟹ ((λx. f x ∙ u) has_vector_derivative f' ∙ u) (at x within S)" "⋀u. u ∈ Basis ⟹ ((λx. g x ∙ u) has_vector_derivative g' ∙ u) (at x within S)" shows "((λx. (f x, g x)) has_vector_derivative (f',g')) (at x within S)" apply (subst has_vector_derivative_componentwise_within) apply (auto simp: assms Basis_prod_def) done lemma piecewise_C1_differentiable_const: shows "(λx. c) piecewise_C1_differentiable_on s" using continuous_on_const by (auto simp add: piecewise_C1_differentiable_on_def) declare piecewise_C1_differentiable_const [simp, derivative_intros] declare piecewise_C1_differentiable_neg [simp, derivative_intros] declare piecewise_C1_differentiable_add [simp, derivative_intros] declare piecewise_C1_differentiable_diff [simp, derivative_intros] (*move to Derivative*) lemma piecewise_C1_differentiable_on_ident [simp, derivative_intros]: fixes f :: "real ⇒ 'a::real_normed_vector" shows "(λx. x) piecewise_C1_differentiable_on S" unfolding piecewise_C1_differentiable_on_def using C1_differentiable_on_ident by (blast intro: continuous_on_id C1_differentiable_on_ident) lemma piecewise_C1_differentiable_on_mult [simp, derivative_intros]: fixes f :: "real ⇒ 'a::real_normed_algebra" assumes "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on S" shows "(λx. f x * g x) piecewise_C1_differentiable_on S" using assms unfolding piecewise_C1_differentiable_on_def apply safe apply (blast intro: continuous_intros) apply (rename_tac A B) apply (rule_tac x="A ∪ B" in exI) apply (auto intro: C1_differentiable_on_mult C1_differentiable_on_subset) done lemma C1_differentiable_on_cdiv [simp, derivative_intros]: fixes f :: "real ⇒ 'a :: real_normed_field" shows "f C1_differentiable_on S ⟹ (λx. f x / c) C1_differentiable_on S" by (simp add: divide_inverse) lemma piecewise_C1_differentiable_on_cdiv [simp, derivative_intros]: fixes f :: "real ⇒ 'a::real_normed_field" assumes "f piecewise_C1_differentiable_on S" shows "(λx. f x / c) piecewise_C1_differentiable_on S" by (simp add: divide_inverse piecewise_C1_differentiable_const piecewise_C1_differentiable_on_mult assms) lemma sqrt_C1_differentiable [simp, derivative_intros]: assumes f: "f C1_differentiable_on S" and fim: "f ` S ⊆ {0<..}" shows "(λx. sqrt (f x)) C1_differentiable_on S" proof - have contf: "continuous_on S f" by (simp add: C1_differentiable_imp_continuous_on f) show ?thesis using assms unfolding C1_differentiable_on_def has_real_derivative_iff_has_vector_derivative [symmetric] by (fastforce intro!: contf continuous_intros derivative_intros) qed lemma sqrt_piecewise_C1_differentiable [simp, derivative_intros]: assumes f: "f piecewise_C1_differentiable_on S" and fim: "f ` S ⊆ {0<..}" shows "(λx. sqrt (f x)) piecewise_C1_differentiable_on S" using assms unfolding piecewise_C1_differentiable_on_def by (fastforce intro!: continuous_intros derivative_intros) lemma fixes f :: "real ⇒ 'a::{banach,real_normed_field}" assumes f: "f C1_differentiable_on S" shows sin_C1_differentiable [simp, derivative_intros]: "(λx. sin (f x)) C1_differentiable_on S" and cos_C1_differentiable [simp, derivative_intros]: "(λx. cos (f x)) C1_differentiable_on S" proof - have contf: "continuous_on S f" by (simp add: C1_differentiable_imp_continuous_on f) note df_sin = field_vector_diff_chain_at [where g=sin, unfolded o_def] note df_cos = field_vector_diff_chain_at [where g=cos, unfolded o_def] show "(λx. sin (f x)) C1_differentiable_on S" "(λx. cos (f x)) C1_differentiable_on S" using assms unfolding C1_differentiable_on_def has_real_derivative_iff_has_vector_derivative [symmetric] apply auto by (rule contf continuous_intros df_sin df_cos derivative_intros exI conjI ballI | force)+ qed lemma has_derivative_abs: fixes a::real assumes "a ≠ 0" shows "(abs has_derivative ((*) (sgn a))) (at a)" proof - have [simp]: "norm = abs" using real_norm_def by force show ?thesis using has_derivative_norm [where 'a=real, simplified] assms by (simp add: mult_commute_abs) qed lemma abs_C1_differentiable [simp, derivative_intros]: fixes f :: "real ⇒ real" assumes f: "f C1_differentiable_on S" and "0 ∉ f ` S" shows "(λx. abs (f x)) C1_differentiable_on S" proof - have contf: "continuous_on S f" by (simp add: C1_differentiable_imp_continuous_on f) note df = DERIV_chain [where f=abs and g=f, unfolded o_def] show ?thesis using assms unfolding C1_differentiable_on_def has_real_derivative_iff_has_vector_derivative [symmetric] apply clarify apply (rule df exI conjI ballI)+ apply (force simp: has_field_derivative_def intro: has_derivative_abs continuous_intros contf)+ done qed lemma C1_differentiable_on_pair [simp, derivative_intros]: fixes f :: "real ⇒ 'a::euclidean_space" and g :: "real ⇒ 'b::euclidean_space" assumes "f C1_differentiable_on S" "g C1_differentiable_on S" shows "(λx. (f x, g x)) C1_differentiable_on S" using assms unfolding C1_differentiable_on_def apply safe apply (rename_tac A B) apply (intro exI ballI conjI) apply (rule_tac f'="A x" and g'="B x" in has_vector_derivative_pair_within) using has_vector_derivative_componentwise_within by (blast intro: continuous_on_Pair)+ lemma piecewise_C1_differentiable_on_pair [simp, derivative_intros]: fixes f :: "real ⇒ 'a::euclidean_space" and g :: "real ⇒ 'b::euclidean_space" assumes "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on S" shows "(λx. (f x, g x)) piecewise_C1_differentiable_on S" using assms unfolding piecewise_C1_differentiable_on_def by (blast intro!: continuous_intros C1_differentiable_on_pair del: continuous_on_discrete intro: C1_differentiable_on_subset) lemma test2: assumes s: "⋀x. x ∈ {0..1} - s ⟹ g differentiable at x" and fs: "finite s" and uv: "u ∈ {0..1}" "v ∈ {0..1}" "u ≤ v" and "x ∈ {0..1}" "x ∉ (λt. (v-u) *⇩_{R}t + u) -` s" shows "vector_derivative (λx. g ((v-u) * x + u)) (at x within {0..1}) = (v-u) *⇩_{R}vector_derivative g (at ((v-u) * x + u) within{0..1})" proof - have i:"(g has_vector_derivative vector_derivative g (at ((v - u) * x + u))) (at ((v-u) * x + u))" using assms s [of "(v - u) * x + u"] uv mult_left_le [of x "v-u"] by (auto simp: vector_derivative_works) have ii:"((λx. g ((v - u) * x + u)) has_vector_derivative (v - u) *⇩_{R}vector_derivative g (at ((v - u) * x + u))) (at x)" by (intro vector_diff_chain_at [simplified o_def] derivative_eq_intros | simp add: i)+ have 0: "0 ≤ (v - u) * x + u" using assms uv by auto have 1: "(v - u) * x + u ≤ 1" using assms uv by simp (metis add.commute atLeastAtMost_iff atLeastatMost_empty_iff diff_ge_0_iff_ge empty_iff le_diff_eq mult_left_le) have iii: "vector_derivative g (at ((v - u) * x + u) within {0..1}) = vector_derivative g (at ((v - u) * x + u))" using Derivative.vector_derivative_at_within_ivl[OF i, of "0" "1", OF 0 1] by auto have iv: "vector_derivative (λx. g ((v - u) * x + u)) (at x within {0..1}) = (v - u) *⇩_{R}vector_derivative g (at ((v - u) * x + u))" using Derivative.vector_derivative_at_within_ivl[OF ii, of "0" "1"] assms by auto show ?thesis using iii iv by auto qed lemma C1_differentiable_on_components: assumes "⋀i. i ∈ Basis ⟹ (λx. f x ∙ i) C1_differentiable_on s" shows "f C1_differentiable_on s" proof (clarsimp simp add: C1_differentiable_on_def has_vector_derivative_def) have *:"∀f i x. x *⇩_{R}(f ∙ i) = (x *⇩_{R}f) ∙ i" by auto have "∃f'. ∀i∈Basis. ∀x∈s. ((λx. f x ∙ i) has_derivative (λz. z *⇩_{R}f' x ∙ i)) (at x) ∧ continuous_on s f'" using assms lambda_skolem_euclidean[of "λi D. (∀x∈s. ((λx. f x ∙ i) has_derivative (λz. z *⇩_{R}D x)) (at x)) ∧ continuous_on s D"] apply (simp only: C1_differentiable_on_def has_vector_derivative_def *) using continuous_on_componentwise[of "s"] by metis then obtain f' where f': "∀i∈Basis. ∀x∈s. ((λx. f x ∙ i) has_derivative (λz. z *⇩_{R}f' x ∙ i)) (at x) ∧ continuous_on s f'" by auto then have 0: "(∀x∈s. (f has_derivative (λz. z *⇩_{R}f' x)) (at x)) ∧ continuous_on s f'" using f' has_derivative_componentwise_within[of "f", where S= UNIV] by auto then show "∃D. (∀x∈s. (f has_derivative (λz. z *⇩_{R}D x)) (at x)) ∧ continuous_on s D" by metis qed lemma piecewise_C1_differentiable_on_components: assumes "finite t" "⋀i. i ∈ Basis ⟹ (λx. f x ∙ i) C1_differentiable_on s - t" "⋀i. i ∈ Basis ⟹ continuous_on s (λx. f x ∙ i)" shows "f piecewise_C1_differentiable_on s" using C1_differentiable_on_components assms continuous_on_componentwise piecewise_C1_differentiable_on_def by blast lemma all_components_smooth_one_pw_smooth_is_pw_smooth: assumes "⋀i. i ∈ Basis - {j} ⟹ (λx. f x ∙ i) C1_differentiable_on s" assumes "(λx. f x ∙ j) piecewise_C1_differentiable_on s" shows "f piecewise_C1_differentiable_on s" proof - have is_cont: "∀i∈Basis. continuous_on s (λx. f x ∙ i)" using assms C1_differentiable_imp_continuous_on piecewise_C1_differentiable_on_def by fastforce obtain t where t:"(finite t ∧ (λx. f x ∙ j) C1_differentiable_on s - t)" using assms(2) piecewise_C1_differentiable_on_def by auto show ?thesis using piecewise_C1_differentiable_on_components[where ?f = "f"] using assms(2) piecewise_C1_differentiable_on_def C1_differentiable_on_subset[OF assms(1) Diff_subset, where ?B1 ="t"] t is_cont by fastforce qed lemma derivative_component_fun_component: fixes i::"'a::euclidean_space" assumes "f differentiable (at x)" shows "((vector_derivative f (at x)) ∙ i) = ((vector_derivative (λx. (f x) ∙ i) (at x)) )" proof - have "((λx. f x ∙ i) has_vector_derivative vector_derivative f (at x) ∙ i) (at x)" using assms and bounded_linear.has_vector_derivative[of "(λx. x ∙ i)" "f" "(vector_derivative f (at x))" "(at x)"] and bounded_linear_inner_left[of "i"] and vector_derivative_works[of "f" "(at x)"] by blast then show "((vector_derivative f (at x)) ∙ i) = ((vector_derivative (λx. (f x) ∙ i) (at x)) )" using vector_derivative_works[of "(λx. (f x) ∙ i)" "(at x)"] and differentiableI_vector[of "(λx. (f x) ∙ i)" "(vector_derivative f (at x) ∙ i)" "(at x)"] and Derivative.vector_derivative_at by force qed lemma gamma_deriv_at_within: assumes a_leq_b: "a < b" and x_within_bounds: "x ∈ {a..b}" and gamma_differentiable: "∀x ∈ {a .. b}. γ differentiable at x" shows "vector_derivative γ (at x within {a..b}) = vector_derivative γ (at x)" using Derivative.vector_derivative_at_within_ivl[of "γ" "vector_derivative γ (at x)" "x" "a" "b"] gamma_differentiable x_within_bounds a_leq_b by (auto simp add: vector_derivative_works) lemma islimpt_diff_finite: assumes "finite (t::'a::t1_space set)" shows "x islimpt s - t = x islimpt s" proof- have iii: "s - t = s - (t ∩ s)" by auto have "(t ∩ s) ⊆ s" by auto have ii:"finite (t ∩ s)" using assms(1) by auto have i: "(t ∩ s) ∪ (s - (t ∩ s)) = ( s)" using assms by auto then have "x islimpt s - (t ∩ s) = x islimpt s" by (metis ii islimpt_Un_finite) then show ?thesis using iii by auto qed lemma ivl_limpt_diff: assumes "finite s" "a < b" "(x::real) ∈ {a..b} - s" shows "x islimpt {a..b} - s" proof- have "x islimpt {a..b}" proof (cases "x ∈{a,b}") have i: "finite {a,b}" and ii: "{a, b} ∪ {a<..<b} = {a..b}" using assms by auto assume "x ∈{a,b}" then show ?thesis by (meson DiffE assms(2) assms(3) islimpt_Icc) next assume "x ∉{a,b}" then show "x islimpt {a..b}" using assms by auto qed then show "x islimpt {a..b} - s" using islimpt_diff_finite[OF assms(1)] assms by fastforce qed lemma ivl_closure_diff_del: assumes "finite s" "a < b" "(x::real) ∈ {a..b} - s" shows "x ∈ closure (({a..b} - s) - {x})" using ivl_limpt_diff islimpt_in_closure assms by blast lemma ivl_not_trivial_limit_within: assumes "finite s" "a < b" "(x::real) ∈ {a..b} - s" shows "at x within {a..b} - s ≠ bot" using assms ivl_closure_diff_del not_trivial_limit_within by blast lemma vector_derivative_at_within_non_trivial_limit: "at x within s ≠ bot ∧ (f has_vector_derivative f') (at x) ⟹ vector_derivative f (at x within s) = f'" using has_vector_derivative_at_within vector_derivative_within by fastforce lemma vector_derivative_at_within_ivl_diff: "finite s ∧ a < b ∧ (x::real) ∈ {a..b} - s ∧ (f has_vector_derivative f') (at x) ⟹ vector_derivative f (at x within {a..b} - s) = f'" using vector_derivative_at_within_non_trivial_limit ivl_not_trivial_limit_within by fastforce lemma gamma_deriv_at_within_diff: assumes a_leq_b: "a < b" and x_within_bounds: "x ∈ {a..b} - s" and gamma_differentiable: "∀x ∈ {a .. b} - s. γ differentiable at x" and s_subset: "s ⊆ {a..b}" and finite_s: "finite s" shows "vector_derivative γ (at x within {a..b} - s) = vector_derivative γ (at x)" using vector_derivative_at_within_ivl_diff [of "s" "a" "b" "x" "γ" "vector_derivative γ (at x)"] gamma_differentiable x_within_bounds a_leq_b s_subset finite_s by (auto simp add: vector_derivative_works) lemma gamma_deriv_at_within_gen: assumes a_leq_b: "a < b" and x_within_bounds: "x ∈ s" and s_subset: "s ⊆ {a..b}" and gamma_differentiable: "∀x ∈ s. γ differentiable at x" shows "vector_derivative γ (at x within ({a..b})) = vector_derivative γ (at x)" using Derivative.vector_derivative_at_within_ivl[of "γ" "vector_derivative γ (at x)" "x" "a" "b"] gamma_differentiable x_within_bounds a_leq_b s_subset by (auto simp add: vector_derivative_works) lemma derivative_component_fun_component_at_within_gen: assumes gamma_differentiable: "∀x ∈ s. γ differentiable at x" and s_subset: "s ⊆ {0..1}" shows "∀x ∈ s. vector_derivative (λx. γ x) (at x within {0..1}) ∙ (i::'a:: euclidean_space) = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" proof - have gamma_i_component_smooth: "∀x ∈ s. (λx. γ x ∙ i) differentiable at x" using gamma_differentiable by auto show "∀x ∈ s. vector_derivative (λx. γ x) (at x within {0..1}) ∙ i = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" proof fix x::real assume x_within_bounds: "x ∈ s" have gamma_deriv_at_within: "vector_derivative (λx. γ x) (at x within {0..1}) = vector_derivative (λx. γ x) (at x)" using gamma_deriv_at_within_gen[of "0" "1"] x_within_bounds gamma_differentiable s_subset by (auto simp add: vector_derivative_works) then have gamma_component_deriv_at_within: "vector_derivative (λx. γ x ∙ i) (at x) = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" using gamma_deriv_at_within_gen[of "0" "1", where γ = "(λx. γ x ∙ i)"] x_within_bounds gamma_i_component_smooth s_subset by (auto simp add: vector_derivative_works) have gamma_component_deriv_eq_gamma_deriv_component: "vector_derivative (λx. γ x ∙ i) (at x) = vector_derivative (λx. γ x) (at x) ∙ i" using derivative_component_fun_component[of "γ" "x" "i"] gamma_differentiable x_within_bounds by auto show "vector_derivative γ (at x within {0..1}) ∙ i = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" using gamma_component_deriv_eq_gamma_deriv_component gamma_component_deriv_at_within gamma_deriv_at_within by auto qed qed lemma derivative_component_fun_component_at_within: assumes gamma_differentiable: "∀x ∈ {0 .. 1}. γ differentiable at x" shows "∀x ∈ {0..1}. vector_derivative (λx. γ x) (at x within {0..1}) ∙ (i::'a:: euclidean_space) = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" proof - have gamma_i_component_smooth: "∀x ∈ {0 .. 1}. (λx. γ x ∙ i) differentiable at x" using gamma_differentiable by auto show "∀x ∈ {0..1}. vector_derivative (λx. γ x) (at x within {0..1}) ∙ i = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" proof fix x::real assume x_within_bounds: "x ∈ {0..1}" have gamma_deriv_at_within: "vector_derivative (λx. γ x) (at x within {0..1}) = vector_derivative (λx. γ x) (at x)" using gamma_deriv_at_within[of "0" "1"] x_within_bounds gamma_differentiable by (auto simp add: vector_derivative_works) have gamma_component_deriv_at_within: "vector_derivative (λx. γ x ∙ i) (at x) = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" using Derivative.vector_derivative_at_within_ivl[of "(λx. (γ x) ∙ i)" "vector_derivative (λx. (γ x) ∙ i) (at x)" "x" "0" "1"] has_vector_derivative_at_within[of "(λx. γ x ∙ i)" "vector_derivative (λx. γ x ∙ i) (at x)" "x" "{0..1}"] gamma_i_component_smooth x_within_bounds by (simp add: vector_derivative_works) have gamma_component_deriv_eq_gamma_deriv_component: "vector_derivative (λx. γ x ∙ i) (at x) = vector_derivative (λx. γ x) (at x) ∙ i" using derivative_component_fun_component[of "γ" "x" "i"] gamma_differentiable x_within_bounds by auto show "vector_derivative γ (at x within {0..1}) ∙ i = vector_derivative (λx. γ x ∙ i) (at x within {0..1})" using gamma_component_deriv_eq_gamma_deriv_component gamma_component_deriv_at_within gamma_deriv_at_within by auto qed qed lemma straight_path_diffrentiable_x: fixes b :: "real" and y1 ::"real" assumes gamma_def: "γ = (λx. (b, y2 + y1 * x))" shows "∀x. γ differentiable at x" unfolding gamma_def differentiable_def by (fast intro!: derivative_intros) lemma straight_path_diffrentiable_y: fixes b :: "real" and y1 y2 ::"real" assumes gamma_def: "γ = (λx. (y2 + y1 * x , b))" shows "∀x. γ differentiable at x" unfolding gamma_def differentiable_def by (fast intro!: derivative_intros) lemma piecewise_C1_differentiable_on_imp_continuous_on: assumes "f piecewise_C1_differentiable_on s" shows "continuous_on s f" using assms by (auto simp add: piecewise_C1_differentiable_on_def) lemma boring_lemma1: fixes f :: "real⇒real" assumes "(f has_vector_derivative D) (at x)" shows "((λx. (f x, 0)) has_vector_derivative ((D,0::real))) (at x)" proof- have *: "((λx. (f x) *⇩_{R}(1,0)) has_vector_derivative (D *⇩_{R}(1,0))) (at x)" using bounded_linear.has_vector_derivative[OF Real_Vector_Spaces.bounded_linear_scaleR_left assms(1), of "(1,0)"] by auto have "((λx. (f x) *⇩_{R}(1,0)) has_vector_derivative (D,0)) (at x)" proof - have "(D, 0::'a) = D *⇩_{R}(1, 0)" by simp then show ?thesis by (metis (no_types) *) qed then show ?thesis by auto qed lemma boring_lemma2: fixes f :: "real⇒real" assumes "(f has_vector_derivative D) (at x)" shows "((λx. (0, f x)) has_vector_derivative (0, D)) (at x)" proof- have *: "((λx. (f x) *⇩_{R}(0,1)) has_vector_derivative (D *⇩_{R}(0,1))) (at x)" using bounded_linear.has_vector_derivative[OF Real_Vector_Spaces.bounded_linear_scaleR_left assms(1), of "(0,1)"] by auto then have "((λx. (f x) *⇩_{R}(0,1)) has_vector_derivative ((0,D))) (at x)" using scaleR_Pair Real_Vector_Spaces.real_scaleR_def proof - have "(0::'b, D) = D *⇩_{R}(0, 1)" by auto then show ?thesis by (metis (no_types) *) qed then show ?thesis by auto qed lemma pair_prod_smooth_pw_smooth: assumes "(f::real⇒real) C1_differentiable_on s" "(g::real⇒real) piecewise_C1_differentiable_on s" shows "(λx. (f x, g x)) piecewise_C1_differentiable_on s" proof - have f_cont: "continuous_on s f" using assms(1) C1_differentiable_imp_continuous_on by fastforce have g_cont: "continuous_on s g" using assms(2) by (auto simp add: piecewise_C1_differentiable_on_def) obtain t where t:"(finite t ∧ g C1_differentiable_on s - t)" using assms(2) piecewise_C1_differentiable_on_def by auto show ?thesis using piecewise_C1_differentiable_on_components[where ?f = "(λx. (f x, g x))"] apply (simp add: real_pair_basis) using assms(2) piecewise_C1_differentiable_on_def C1_differentiable_on_subset[OF assms(1) Diff_subset, where ?B1 ="t"] t f_cont g_cont by fastforce qed lemma scale_shift_smooth: shows "(λx. a + b * x) C1_differentiable_on s" proof - show "(λx. a + b * x) C1_differentiable_on s" using C1_differentiable_on_mult C1_differentiable_on_add C1_differentiable_on_const C1_differentiable_on_ident by auto qed lemma open_diff: assumes "finite (t::'a::t1_space set)" "open (s::'a set)" shows "open (s -t)" using assms proof(induction "t") show "open s ⟹ open (s - {})" by auto next fix x::"'a::t1_space" fix F::"'a::t1_space set" assume step: "finite F " " x ∉ F" "open s" then have i: "(s - insert x F) = (s - F) - {x}" by auto assume ind_hyp: " (open s ⟹ open (s - F))" show "open (s - insert x F)" apply (simp only: i) using open_delete[of "s -F"] ind_hyp[OF step(3)] by auto qed lemma has_derivative_transform_within: assumes "0 < d" and "x ∈ s" and "∀x'∈s. dist x' x < d ⟶ f x' = g x'" and "(f has_derivative f') (at x within s)" shows "(g has_derivative f') (at x within s)" using assms unfolding has_derivative_within by (force simp add: intro: Lim_transform_within) lemma has_derivative_transform_within_ivl: assumes "(0::real) < b" and "∀x∈{a..b} -s. f x = g x" and "x ∈ {a..b} -s" and "(f has_derivative f') (at x within {a..b} - s)" shows "(g has_derivative f') (at x within {a..b} - s)" using has_derivative_transform_within[of "b" "x" "{a..b} - s"] assms by auto lemma has_vector_derivative_transform_within_ivl: assumes "(0::real) < b" and "∀x∈{a..b} -s . f x = g x" and "x ∈ {a..b} - s" and "(f has_vector_derivative f') (at x within {a..b} - s)" shows "(g has_vector_derivative f') (at x within {a..b} - s)" using assms has_derivative_transform_within_ivl apply (auto simp add: has_vector_derivative_def) by blast lemma has_derivative_transform_at: assumes "0 < d" and "∀x'. dist x' x < d ⟶ f x' = g x'" and "(f has_derivative f') (at x)" shows "(g has_derivative f') (at x)" using has_derivative_transform_within [of d x UNIV f g f'] assms by simp lemma has_vector_derivative_transform_at: assumes "0 < d" and "∀x'. dist x' x < d ⟶ f x' = g x'" and "(f has_vector_derivative f') (at x)" shows "(g has_vector_derivative f') (at x)" using assms unfolding has_vector_derivative_def by (rule has_derivative_transform_at) lemma C1_diff_components_2: assumes "b ∈ Basis" assumes "f C1_differentiable_on s" shows "(λx. f x ∙ b) C1_differentiable_on s" proof - obtain D where D:"(∀x∈s. (f has_derivative (λz. z *⇩_{R}D x)) (at x))" "continuous_on s D" using assms(2) by (fastforce simp add: C1_differentiable_on_def has_vector_derivative_def) show ?thesis proof (simp add: C1_differentiable_on_def has_vector_derivative_def, intro exI conjI) show "continuous_on s (λx. D x ∙ b)" using D continuous_on_componentwise assms(1) by fastforce show "(∀x∈s. ((λx. f x ∙ b) has_derivative (λy. y * (λx. D x ∙ b) x)) (at x))" using has_derivative_inner_left D(1) by fastforce qed qed lemma eq_smooth: assumes "0 < d" "∀x∈s. ∀y. dist x y < d ⟶ f y = g y" (*This crappy condition cannot be loosened :( *) "f C1_differentiable_on s" shows "g C1_differentiable_on s" proof (simp add: C1_differentiable_on_def) obtain D where D: "(∀x∈s. (f has_vector_derivative D x) (at x)) ∧ continuous_on s D" using assms by (auto simp add: C1_differentiable_on_def) then have f: "(∀x∈s. (g has_vector_derivative D x) (at x))" using assms(1-2) by (metis dist_commute has_vector_derivative_transform_at) have "(∀x∈s. (g has_vector_derivative D x) (at x)) ∧ continuous_on s D" using D f by auto then show "∃D. (∀x∈s. (g has_vector_derivative D x) (at x)) ∧ continuous_on s D" by metis qed lemma eq_pw_smooth: assumes "0 < d" "∀x∈s. ∀y. dist x y < d ⟶ f y = g y" (*This crappy condition cannot be loosened :( *) "∀x∈s. f x = g x" "f piecewise_C1_differentiable_on s" shows "g piecewise_C1_differentiable_on s" proof (simp add: piecewise_C1_differentiable_on_def) have g_cont: "continuous_on s g" using assms piecewise_C1_differentiable_const by (simp add: piecewise_C1_differentiable_on_def) obtain t where t: "finite t ∧ f C1_differentiable_on s - t" using assms by (auto simp add: piecewise_C1_differentiable_on_def) then have "g C1_differentiable_on s - t" using assms eq_smooth by blast then show "continuous_on s g ∧ (∃t. finite t ∧ g C1_differentiable_on s - t)" using t g_cont by metis qed lemma scale_piecewise_C1_differentiable_on: assumes "f piecewise_C1_differentiable_on s" shows "(λx. (c::real) * (f x)) piecewise_C1_differentiable_on s" proof (simp add: piecewise_C1_differentiable_on_def, intro conjI) show "continuous_on s (λx. c * f x)" using assms continuous_on_mult_left by (auto simp add: piecewise_C1_differentiable_on_def) show "∃t. finite t ∧ (λx. c * f x) C1_differentiable_on s - t" using assms continuous_on_mult_left by (auto simp add: piecewise_C1_differentiable_on_def) qed lemma eq_smooth_gen: assumes "f C1_differentiable_on s" "∀x. f x = g x" shows "g C1_differentiable_on s" using assms unfolding C1_differentiable_on_def by (metis (no_types, lifting) has_vector_derivative_weaken UNIV_I top_greatest) lemma subpath_compose: shows "(subpath a b γ) = γ o (λx. (b - a) * x + a)" by (auto simp add: subpath_def) lemma subpath_smooth: assumes "γ C1_differentiable_on {0..1}" "0 ≤ a" "a < b" "b ≤ 1" shows "(subpath a b γ) C1_differentiable_on {0..1}" proof- have "γ C1_differentiable_on {a..b}" apply (rule C1_differentiable_on_subset) using assms by auto then have "γ C1_differentiable_on (λx. (b - a) * x + a) ` {0..1}" using ‹a < b› closed_segment_eq_real_ivl closed_segment_real_eq by auto moreover have "finite ({0..1} ∩ (λx. (b - a) * x + a) -` {x})" for x proof - have "((λx. (b - a) * x + a) -` {x}) = {(x -a) /(b-a)}" using assms by (auto simp add: divide_simps) then show ?thesis by auto qed ultimately show ?thesis by (force simp add: subpath_compose intro: C1_differentiable_compose derivative_intros) qed lemma has_vector_derivative_divide[derivative_intros]: fixes a :: "'a::real_normed_field" shows "(f has_vector_derivative x) F ⟹ ((λx. f x / a) has_vector_derivative (x / a)) F" unfolding divide_inverse by (fact has_vector_derivative_mult_left) end