Theory Derivs
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]
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"
"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"
"∀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