[STATEMENT]
lemma twice_field_differentiable_at_compose:
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at (f x)"
    shows "(\<lambda>x. g (f x)) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
obtain S S'
   where Df_on_S:  "f field_differentiable_on S" and x_int_S: "x \<in> interior S"
     and Dg_on_S': "g field_differentiable_on S'" and fx_int_S': "f x \<in> interior S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; f x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at f x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; f x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
f x \<in> interior S'

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
let ?T = "{x \<in> interior S. f x \<in> interior S'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
have "continuous_on (interior S) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (interior S) f
[PROOF STEP]
by (meson Df_on_S continuous_on_eq_continuous_within continuous_on_subset field_differentiable_imp_continuous_at
         field_differentiable_on_def interior_subset)
[PROOF STATE]
proof (state)
this:
continuous_on (interior S) f

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on (interior S) f
[PROOF STEP]
have "open (interior S \<inter> {x. f x \<in> interior S'})"
[PROOF STATE]
proof (prove)
using this:
continuous_on (interior S) f

goal (1 subgoal):
 1. open (interior S \<inter> {x. f x \<in> interior S'})
[PROOF STEP]
by (metis continuous_open_preimage open_interior vimage_def)
[PROOF STATE]
proof (state)
this:
open (interior S \<inter> {x. f x \<in> interior S'})

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open (interior S \<inter> {x. f x \<in> interior S'})
[PROOF STEP]
have x_int_T: "x \<in> interior ?T"
[PROOF STATE]
proof (prove)
using this:
open (interior S \<inter> {x. f x \<in> interior S'})

goal (1 subgoal):
 1. x \<in> interior {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by (metis (no_types) Collect_conj_eq Collect_mem_eq Int_Collect fx_int_S' interior_eq x_int_S)
[PROOF STATE]
proof (state)
this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
have  Dg_on_fT: "g field_differentiable_on f`?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by (metis (no_types, lifting) Dg_on_S' field_differentiable_on_subset image_Collect_subsetI interior_subset)
[PROOF STATE]
proof (state)
this:
g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
have Df_on_T: "f field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
using  field_differentiable_on_subset Df_on_S
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f field_differentiable_on ?S; ?T \<subseteq> ?S\<rbrakk> \<Longrightarrow> ?f field_differentiable_on ?T
f field_differentiable_on S

goal (1 subgoal):
 1. f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by (metis Collect_subset interior_subset)
[PROOF STATE]
proof (state)
this:
f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
have "(\<lambda>x. g (f x)) field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. g (f x)) field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
unfolding field_differentiable_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{x \<in> interior S. f x \<in> interior S'}. (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
assume x_int: "x \<in> {x \<in> interior S. f x \<in> interior S'}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
have "f field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable at x
[PROOF STEP]
by (metis Df_on_S at_within_interior field_differentiable_on_def interior_subset mem_Collect_eq subsetD x_int)
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
have "g field_differentiable at (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable at (f x)
[PROOF STEP]
by (metis Dg_on_S' at_within_interior field_differentiable_on_def interior_subset mem_Collect_eq subsetD x_int)
[PROOF STATE]
proof (state)
this:
g field_differentiable at (f x)

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f field_differentiable at x
g field_differentiable at (f x)
[PROOF STEP]
have "(g \<circ> f) field_differentiable at x"
[PROOF STATE]
proof (prove)
using this:
f field_differentiable at x
g field_differentiable at (f x)

goal (1 subgoal):
 1. g \<circ> f field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_compose)
[PROOF STATE]
proof (state)
this:
g \<circ> f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<circ> f field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. g (f x)) field_differentiable at x"
[PROOF STATE]
proof (prove)
using this:
g \<circ> f field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. g (f x)) field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
show "(\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. g (f x)) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
using field_differentiable_at_within
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. g (f x)) field_differentiable at x
?f field_differentiable at ?x \<Longrightarrow> ?f field_differentiable at ?x within ?S

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. g (f x)) field_differentiable at x within {x \<in> interior S. f x \<in> interior S'}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. g (f x)) field_differentiable_on {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. g (f x)) field_differentiable_on {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
have "deriv (\<lambda>x. g (f x)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. deriv g (f x)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. deriv g (f x)) field_differentiable at x
[PROOF STEP]
by (metis DERIV_chain2 assms deriv_field_differentiable_at field_differentiable_def once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. deriv g (f x)) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. deriv g (f x)) field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. deriv g (f x)) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x
[PROOF STEP]
using assms field_differentiable_mult[of "\<lambda>x. deriv g (f x)"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. deriv g (f x)) field_differentiable at x
f twice_field_differentiable_at x
g twice_field_differentiable_at f x
\<lbrakk>(\<lambda>x. deriv g (f x)) field_differentiable at ?a within ?S; ?g field_differentiable at ?a within ?S\<rbrakk> \<Longrightarrow> (\<lambda>z. deriv g (f z) * ?g z) field_differentiable at ?a within ?S

goal (1 subgoal):
 1. (\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x
[PROOF STEP]
by (simp add: deriv_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
have "deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x
[PROOF STEP]
using assms Df_on_S x_int_S deriv_cong_ev eventually_deriv_compose
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at f x
f field_differentiable_on S
x \<in> interior S
\<lbrakk>\<forall>\<^sub>F x in nhds ?x. ?f x = ?g x; ?x = ?y\<rbrakk> \<Longrightarrow> deriv ?f ?x = deriv ?g ?y
\<lbrakk>\<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S; ?g twice_field_differentiable_at ?f ?x\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in nhds ?x. deriv (\<lambda>x. ?g (?f x)) x = deriv ?g (?f x) * deriv ?f x

goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x
deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x
deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
using assms eventually_deriv_compose DERIV_deriv_iff_field_differentiable Df_on_S x_int_S
            DERIV_cong_ev[of x x "deriv (\<lambda>x. g (f x))" "\<lambda>x. deriv g (f x) * deriv f x"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. deriv g (f x) * deriv f x) field_differentiable at x
deriv (deriv (\<lambda>x. g (f x))) x = deriv (\<lambda>x. deriv g (f x) * deriv f x) x
f twice_field_differentiable_at x
g twice_field_differentiable_at f x
\<lbrakk>\<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S; ?g twice_field_differentiable_at ?f ?x\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in nhds ?x. deriv (\<lambda>x. ?g (?f x)) x = deriv ?g (?f x) * deriv ?f x
(?f has_field_derivative deriv ?f ?x) (at ?x) = (?f field_differentiable at ?x)
f field_differentiable_on S
x \<in> interior S
\<lbrakk>x = x; \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x; ?u = ?v\<rbrakk> \<Longrightarrow> (deriv (\<lambda>x. g (f x)) has_field_derivative ?u) (at x) = ((\<lambda>x. deriv g (f x) * deriv f x) has_field_derivative ?v) (at x)

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. g (f x)) field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
deriv (\<lambda>x. g (f x)) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. g (f x)) field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
deriv (\<lambda>x. g (f x)) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
using twice_field_differentiable_at_def x_int_T
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. g (f x)) field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
deriv (\<lambda>x. g (f x)) field_differentiable at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x
x \<in> interior {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. (\<lambda>x. g (f x)) twice_field_differentiable_at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. g (f x)) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_const [simp, intro]:
  "(\<lambda>x. a) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. a) twice_field_differentiable_at x
[PROOF STEP]
by (auto intro: exI [of _ UNIV] simp add: twice_field_differentiable_at_def field_differentiable_on_def)


[STATEMENT]
lemma twice_field_differentiable_at_ident [simp, intro]:
  "(\<lambda>x. x) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. x) twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (\<lambda>x. x) field_differentiable at x"
   and "deriv ((\<lambda>x. x)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (\<lambda>x. x) field_differentiable at x &&& deriv (\<lambda>x. x) field_differentiable at x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. x) field_differentiable at x
deriv (\<lambda>x. x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x) twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (\<lambda>x. x) field_differentiable at x
deriv (\<lambda>x. x) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. x) field_differentiable at x
deriv (\<lambda>x. x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x) twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. x) field_differentiable at x
deriv (\<lambda>x. x) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (\<lambda>x. x) field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv (\<lambda>x. x) field_differentiable at x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_cmult [simp, intro]:
"(*) k twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*) k twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (*) k twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (*) k field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (*) k field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (*) k field_differentiable at x

goal (1 subgoal):
 1. (*) k twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (*) k field_differentiable at x

goal (1 subgoal):
 1. (*) k twice_field_differentiable_at x
[PROOF STEP]
have "deriv ((*) k) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv ((*) k) field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv ((*) k) field_differentiable at x

goal (1 subgoal):
 1. (*) k twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (*) k field_differentiable at x
deriv ((*) k) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (*) k field_differentiable at x
deriv ((*) k) field_differentiable at x

goal (1 subgoal):
 1. (*) k twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (*) k field_differentiable at x
deriv ((*) k) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (*) k field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv ((*) k) field_differentiable at x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(*) k twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_uminus [simp, intro]:
  "uminus twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. uminus field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. uminus field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_minus)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. uminus field_differentiable at x

goal (1 subgoal):
 1. uminus twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. uminus field_differentiable at x

goal (1 subgoal):
 1. uminus twice_field_differentiable_at x
[PROOF STEP]
have "deriv uminus field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv uminus field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv uminus field_differentiable at x

goal (1 subgoal):
 1. uminus twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. uminus field_differentiable at x
deriv uminus field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. uminus field_differentiable at x
deriv uminus field_differentiable at x

goal (1 subgoal):
 1. uminus twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. uminus field_differentiable at x
deriv uminus field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. uminus field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv uminus field_differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uminus twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_uminus_fun [intro]:
  assumes "f twice_field_differentiable_at x"
    shows "(\<lambda>x. - f x) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. - f x) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms twice_field_differentiable_at_compose)


[STATEMENT]
lemma deriv_scaleR_right_id [simp]:
  "(deriv ((*\<^sub>R) k)) = (\<lambda>z. k *\<^sub>R 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv ((*\<^sub>R) k) = (\<lambda>z. k *\<^sub>R (1::'a))
[PROOF STEP]
using DERIV_imp_deriv has_field_derivative_scaleR_right DERIV_ident
[PROOF STATE]
proof (prove)
using this:
(?f has_field_derivative ?f') (at ?x) \<Longrightarrow> deriv ?f ?x = ?f'
(?f has_field_derivative ?D) ?F \<Longrightarrow> ((\<lambda>x. ?c *\<^sub>R ?f x) has_field_derivative ?c *\<^sub>R ?D) ?F
((\<lambda>x. x) has_field_derivative (1::?'a)) ?F

goal (1 subgoal):
 1. deriv ((*\<^sub>R) k) = (\<lambda>z. k *\<^sub>R (1::'a))
[PROOF STEP]
by blast


[STATEMENT]
lemma deriv_deriv_scaleR_right_id [simp]:
  "deriv (deriv ((*\<^sub>R) k)) = (\<lambda>z. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv ((*\<^sub>R) k)) = (\<lambda>z. 0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma deriv_scaleR_right:
  "f field_differentiable (at z) \<Longrightarrow> deriv (\<lambda>x. k *\<^sub>R f x) z = k *\<^sub>R deriv f z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable at z \<Longrightarrow> deriv (\<lambda>x. k *\<^sub>R f x) z = k *\<^sub>R deriv f z
[PROOF STEP]
by (simp add: DERIV_imp_deriv field_differentiable_derivI has_field_derivative_scaleR_right)


[STATEMENT]
lemma field_differentiable_scaleR_right [intro]:
  "f field_differentiable F \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) field_differentiable F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable F \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) field_differentiable F
[PROOF STEP]
using field_differentiable_def has_field_derivative_scaleR_right
[PROOF STATE]
proof (prove)
using this:
?f field_differentiable ?F \<equiv> \<exists>f'. (?f has_field_derivative f') ?F
(?f has_field_derivative ?D) ?F \<Longrightarrow> ((\<lambda>x. ?c *\<^sub>R ?f x) has_field_derivative ?c *\<^sub>R ?D) ?F

goal (1 subgoal):
 1. f field_differentiable F \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) field_differentiable F
[PROOF STEP]
by blast


[STATEMENT]
lemma has_field_derivative_scaleR_deriv_right:
  assumes "f twice_field_differentiable_at z"
  shows "((\<lambda>x. k *\<^sub>R deriv f x) has_field_derivative k *\<^sub>R deriv (deriv f) z) (at z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. k *\<^sub>R deriv f x) has_field_derivative k *\<^sub>R deriv (deriv f) z) (at z)
[PROOF STEP]
by (simp add: DERIV_deriv_iff_field_differentiable assms deriv_field_differentiable_at has_field_derivative_scaleR_right)


[STATEMENT]
lemma deriv_scaleR_deriv_right:
  assumes "f twice_field_differentiable_at z"
  shows "deriv (\<lambda>x. k *\<^sub>R deriv f x) z = k *\<^sub>R deriv (deriv f) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R deriv f x) z = k *\<^sub>R deriv (deriv f) z
[PROOF STEP]
using assms deriv_scaleR_right twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at z
?f field_differentiable at ?z \<Longrightarrow> deriv (\<lambda>x. ?k *\<^sub>R ?f x) ?z = ?k *\<^sub>R deriv ?f ?z
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R deriv f x) z = k *\<^sub>R deriv (deriv f) z
[PROOF STEP]
by blast


[STATEMENT]
lemma twice_field_differentiable_at_scaleR [simp, intro]:
  "(*\<^sub>R) k twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*\<^sub>R) k twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (*\<^sub>R) k twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_scaleR_right)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x

goal (1 subgoal):
 1. (*\<^sub>R) k twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x

goal (1 subgoal):
 1. (*\<^sub>R) k twice_field_differentiable_at x
[PROOF STEP]
have "deriv ((*\<^sub>R) k) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv ((*\<^sub>R) k) field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv ((*\<^sub>R) k) field_differentiable at x

goal (1 subgoal):
 1. (*\<^sub>R) k twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x
deriv ((*\<^sub>R) k) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x
deriv ((*\<^sub>R) k) field_differentiable at x

goal (1 subgoal):
 1. (*\<^sub>R) k twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (*\<^sub>R) k field_differentiable at x
deriv ((*\<^sub>R) k) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (*\<^sub>R) k field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv ((*\<^sub>R) k) field_differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(*\<^sub>R) k twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_scaleR_fun [simp, intro]:
  assumes "f twice_field_differentiable_at x"
  shows "(\<lambda>x. k *\<^sub>R f x) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R f x) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms twice_field_differentiable_at_compose)


[STATEMENT]
lemma eventually_deriv_add:
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at x"
    shows "\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
obtain S where Df_on_S: "f field_differentiable_on S" and x_int_S: "x \<in> interior S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S. \<lbrakk>f field_differentiable_on S; x \<in> interior S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>f field_differentiable_on S; x \<in> interior S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S
x \<in> interior S

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
obtain S' where Dg_on_S: "g field_differentiable_on S'" and x_int_S': "x \<in> interior S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g field_differentiable_on S'
x \<in> interior S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
have "x \<in> interior (S \<inter> S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> interior (S \<inter> S')
[PROOF STEP]
by (simp add: x_int_S x_int_S')
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
have Df_on_SS': "f field_differentiable_on (S \<inter> S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable_on S \<inter> S'
[PROOF STEP]
by (meson Df_on_S IntD1 field_differentiable_on_def field_differentiable_within_subset inf_sup_ord(1))
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S \<inter> S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S \<inter> S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
have Dg_on_SS': "g field_differentiable_on (S \<inter> S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable_on S \<inter> S'
[PROOF STEP]
by (meson Dg_on_S IntD2 field_differentiable_on_def field_differentiable_within_subset inf_le2)
[PROOF STATE]
proof (state)
this:
g field_differentiable_on S \<inter> S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g field_differentiable_on S \<inter> S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
have "open (interior (S \<inter> S'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (interior (S \<inter> S'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open (interior (S \<inter> S'))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
open (interior (S \<inter> S'))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
have "\<forall>x\<in> interior (S \<inter> S'). deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
by (metis (full_types) Df_on_SS' Dg_on_SS' at_within_interior deriv_add field_differentiable_on_def in_mono interior_subset)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> interior (S \<inter> S')
f field_differentiable_on S \<inter> S'
g field_differentiable_on S \<inter> S'
open (interior (S \<inter> S'))
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> interior (S \<inter> S')
f field_differentiable_on S \<inter> S'
g field_differentiable_on S \<inter> S'
open (interior (S \<inter> S'))
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
using eventually_nhds
[PROOF STATE]
proof (prove)
using this:
x \<in> interior (S \<inter> S')
f field_differentiable_on S \<inter> S'
g field_differentiable_on S \<inter> S'
open (interior (S \<inter> S'))
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
eventually ?P (nhds ?a) = (\<exists>S. open S \<and> ?a \<in> S \<and> (\<forall>x\<in>S. ?P x))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_add [intro]:
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at x"
    shows "(\<lambda>x. f x + g x) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
obtain S S'
   where Df_on_S:  "f field_differentiable_on S" and x_int_S: "x \<in> interior S"
     and Dg_on_S': "g field_differentiable_on S'" and x_int_S': " x \<in> interior S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
x \<in> interior S'

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
let ?T = "interior (S \<inter> S')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
have x_int_T: "x \<in> interior ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> interior (interior (S \<inter> S'))
[PROOF STEP]
by (simp add: x_int_S x_int_S')
[PROOF STATE]
proof (state)
this:
x \<in> interior (interior (S \<inter> S'))

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
have Df_on_T: "f field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable_on interior (S \<inter> S')
[PROOF STEP]
by (meson Df_on_S field_differentiable_on_subset inf_sup_ord(1) interior_subset)
[PROOF STATE]
proof (state)
this:
f field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
have  Dg_on_fT: "g field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable_on interior (S \<inter> S')
[PROOF STEP]
by (meson Dg_on_S' field_differentiable_on_subset interior_subset le_infE)
[PROOF STATE]
proof (state)
this:
g field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
have "(\<lambda>x. f x + g x) field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x + g x) field_differentiable_on interior (S \<inter> S')
[PROOF STEP]
unfolding field_differentiable_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>interior (S \<inter> S'). (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
assume x_in_T: "x \<in> ?T"
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
have "f field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable at x
[PROOF STEP]
by (metis x_in_T Df_on_T at_within_open field_differentiable_on_def open_interior)
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
have "g field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable at x
[PROOF STEP]
by (metis x_in_T Dg_on_fT at_within_open field_differentiable_on_def open_interior)
[PROOF STATE]
proof (state)
this:
g field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f field_differentiable at x
g field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. f x + g x) field_differentiable at x"
[PROOF STATE]
proof (prove)
using this:
f field_differentiable at x
g field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_add)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
show "(\<lambda>x. f x + g x) field_differentiable at x within ?T"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x + g x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
using field_differentiable_at_within
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x + g x) field_differentiable at x
?f field_differentiable at ?x \<Longrightarrow> ?f field_differentiable at ?x within ?S

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) field_differentiable at x within interior (S \<inter> S')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
have "deriv (\<lambda>x. f x + g x) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
have "deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
[PROOF STEP]
by (simp add: assms once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. deriv f x + deriv g x) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. deriv f x + deriv g x) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_add assms deriv_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. deriv f x + deriv g x) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
(\<lambda>x. deriv f x + deriv g x) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
(\<lambda>x. deriv f x + deriv g x) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
using assms DERIV_deriv_iff_field_differentiable
            DERIV_cong_ev[of x x "deriv (\<lambda>x. f x + g x)" "\<lambda>x. deriv f x + deriv g x"]
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x
(\<lambda>x. deriv f x + deriv g x) field_differentiable at x
f twice_field_differentiable_at x
g twice_field_differentiable_at x
(?f has_field_derivative deriv ?f ?x) (at ?x) = (?f field_differentiable at ?x)
\<lbrakk>x = x; \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x + g x) x = deriv f x + deriv g x; ?u = ?v\<rbrakk> \<Longrightarrow> (deriv (\<lambda>x. f x + g x) has_field_derivative ?u) (at x) = ((\<lambda>x. deriv f x + deriv g x) has_field_derivative ?v) (at x)

goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
by (simp add: eventually_deriv_add field_differentiable_def)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x + g x) field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x + g x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x + g x) field_differentiable_on interior (S \<inter> S')
deriv (\<lambda>x. f x + g x) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x + g x) field_differentiable_on interior (S \<inter> S')
deriv (\<lambda>x. f x + g x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
using twice_field_differentiable_at_def x_int_T
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x + g x) field_differentiable_on interior (S \<inter> S')
deriv (\<lambda>x. f x + g x) field_differentiable at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x
x \<in> interior (interior (S \<inter> S'))

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) twice_field_differentiable_at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deriv_add_id_const [simp]:
  "deriv (\<lambda>x. x + a) = (\<lambda>z. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. x + a) = (\<lambda>z. 1::'a)
[PROOF STEP]
using ext trans[OF deriv_add]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
\<lbrakk>?f1 field_differentiable at ?z1; ?g1 field_differentiable at ?z1; deriv ?f1 ?z1 + deriv ?g1 ?z1 = ?t\<rbrakk> \<Longrightarrow> deriv (\<lambda>w. ?f1 w + ?g1 w) ?z1 = ?t

goal (1 subgoal):
 1. deriv (\<lambda>x. x + a) = (\<lambda>z. 1::'a)
[PROOF STEP]
by force


[STATEMENT]
lemma deriv_deriv_add_id_const [simp]:
  "deriv (deriv (\<lambda>x. x + a)) z = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. x + a)) z = (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma twice_field_differentiable_at_cadd [simp]:
  "(\<lambda>x. x + a) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x + a) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. x + a) twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_add)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x + a) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x + a) twice_field_differentiable_at x
[PROOF STEP]
have "deriv ((\<lambda>x. x + a)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. x + a) field_differentiable at x
[PROOF STEP]
by (simp add: ext)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x + a) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x
deriv (\<lambda>x. x + a) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x
deriv (\<lambda>x. x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x + a) twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. x + a) field_differentiable at x
deriv (\<lambda>x. x + a) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (\<lambda>x. x + a) field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv (\<lambda>x. x + a) field_differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x + a) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_linear [simp, intro]:
  "(\<lambda>x. k * x + a) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. k * x + a) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. k * x + a) twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_add)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k * x + a) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k * x + a) twice_field_differentiable_at x
[PROOF STEP]
have "deriv ((\<lambda>x. k * x + a)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
have "deriv ((\<lambda>x. k * x + a)) = (\<lambda>x. k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. k * x + a) = (\<lambda>x. k)
[PROOF STEP]
by (simp add: ext)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. k * x + a) = (\<lambda>x. k)

goal (1 subgoal):
 1. deriv (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. k * x + a) = (\<lambda>x. k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. k * x + a) = (\<lambda>x. k)

goal (1 subgoal):
 1. deriv (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. k * x + a) field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. k * x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k * x + a) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x
deriv (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x
deriv (\<lambda>x. k * x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k * x + a) twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. k * x + a) field_differentiable at x
deriv (\<lambda>x. k * x + a) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (\<lambda>x. k * x + a) field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv (\<lambda>x. k * x + a) field_differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. k * x + a) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_linearR [simp, intro]:
  "(\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_scaleR_right field_differentiable_add)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x
[PROOF STEP]
have "deriv ((\<lambda>x. k *\<^sub>R x + a)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
have "deriv ((\<lambda>x. k *\<^sub>R x + a)) = (\<lambda>x. k *\<^sub>R 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R x + a) = (\<lambda>x. k *\<^sub>R (1::'a))
[PROOF STEP]
by (simp add: ext once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. k *\<^sub>R x + a) = (\<lambda>x. k *\<^sub>R (1::'a))

goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. k *\<^sub>R x + a) = (\<lambda>x. k *\<^sub>R (1::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. k *\<^sub>R x + a) = (\<lambda>x. k *\<^sub>R (1::'a))

goal (1 subgoal):
 1. deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv (\<lambda>x. k *\<^sub>R x + a) field_differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eventually_deriv_mult:
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at x"
    shows "\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
obtain S and S'
    where "f field_differentiable_on S"   and in_S:  "x \<in> interior S"
      and "g field_differentiable_on S'"  and in_S': "x \<in> interior S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
x \<in> interior S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
x \<in> interior S'
[PROOF STEP]
have Df_on_SS': "f field_differentiable_on (S \<inter> S')"
        and Dg_on_SS': "g field_differentiable_on (S \<inter> S')"
[PROOF STATE]
proof (prove)
using this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
x \<in> interior S'

goal (1 subgoal):
 1. f field_differentiable_on S \<inter> S' &&& g field_differentiable_on S \<inter> S'
[PROOF STEP]
using field_differentiable_on_subset
[PROOF STATE]
proof (prove)
using this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
x \<in> interior S'
\<lbrakk>?f field_differentiable_on ?S; ?T \<subseteq> ?S\<rbrakk> \<Longrightarrow> ?f field_differentiable_on ?T

goal (1 subgoal):
 1. f field_differentiable_on S \<inter> S' &&& g field_differentiable_on S \<inter> S'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S \<inter> S'
g field_differentiable_on S \<inter> S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
have "\<forall>x\<in> interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
assume "x \<in> interior (S \<inter> S')"
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> interior (S \<inter> S')
[PROOF STEP]
have "f field_differentiable (at x)"
          and "g field_differentiable (at x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. f field_differentiable at x &&& g field_differentiable at x
[PROOF STEP]
using Df_on_SS' Dg_on_SS' field_differentiable_on_def at_within_interior interior_subset subsetD
[PROOF STATE]
proof (prove)
using this:
x \<in> interior (S \<inter> S')
f field_differentiable_on S \<inter> S'
g field_differentiable_on S \<inter> S'
?f field_differentiable_on ?s \<equiv> \<forall>x\<in>?s. ?f field_differentiable at x within ?s
?x \<in> interior ?S \<Longrightarrow> at ?x within ?S = at ?x
interior ?S \<subseteq> ?S
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. f field_differentiable at x &&& g field_differentiable at x
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
f field_differentiable at x
g field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f field_differentiable at x
g field_differentiable at x
[PROOF STEP]
show "deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x"
[PROOF STATE]
proof (prove)
using this:
f field_differentiable at x
g field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
have "x \<in> interior (S \<inter> S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> interior (S \<inter> S')
[PROOF STEP]
by (simp add: in_S in_S')
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
have "open (interior (S \<inter> S'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (interior (S \<inter> S'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open (interior (S \<inter> S'))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
x \<in> interior (S \<inter> S')
open (interior (S \<inter> S'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
x \<in> interior (S \<inter> S')
open (interior (S \<inter> S'))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
using eventually_nhds
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>interior (S \<inter> S'). deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
x \<in> interior (S \<inter> S')
open (interior (S \<inter> S'))
eventually ?P (nhds ?a) = (\<exists>S. open S \<and> ?a \<in> S \<and> (\<forall>x\<in>S. ?P x))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_mult [intro]:
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at x"
    shows "(\<lambda>x. f x * g x) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
obtain S S'
   where Df_on_S:  "f field_differentiable_on S" and x_int_S: "x \<in> interior S"
     and Dg_on_S': "g field_differentiable_on S'" and x_int_S': " x \<in> interior S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
x \<in> interior S'

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
let ?T = "interior (S \<inter> S')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
have x_int_T: "x \<in> interior ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> interior (interior (S \<inter> S'))
[PROOF STEP]
by (simp add: x_int_S x_int_S')
[PROOF STATE]
proof (state)
this:
x \<in> interior (interior (S \<inter> S'))

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
have Df_on_T: "f field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable_on interior (S \<inter> S')
[PROOF STEP]
by (meson Df_on_S field_differentiable_on_subset inf_sup_ord(1) interior_subset)
[PROOF STATE]
proof (state)
this:
f field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
have  Dg_on_fT: "g field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable_on interior (S \<inter> S')
[PROOF STEP]
by (meson Dg_on_S' field_differentiable_on_subset interior_subset le_infE)
[PROOF STATE]
proof (state)
this:
g field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
have "(\<lambda>x. f x * g x) field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) field_differentiable_on interior (S \<inter> S')
[PROOF STEP]
unfolding field_differentiable_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>interior (S \<inter> S'). (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
assume x_in_T: "x \<in> ?T"
[PROOF STATE]
proof (state)
this:
x \<in> interior (S \<inter> S')

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
have "f field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable at x
[PROOF STEP]
by (metis x_in_T Df_on_T at_within_open field_differentiable_on_def open_interior)
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
have "g field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable at x
[PROOF STEP]
by (metis x_in_T Dg_on_fT at_within_open field_differentiable_on_def open_interior)
[PROOF STATE]
proof (state)
this:
g field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f field_differentiable at x
g field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. f x * g x) field_differentiable at x"
[PROOF STATE]
proof (prove)
using this:
f field_differentiable at x
g field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_mult)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior (S \<inter> S') \<Longrightarrow> (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
show "(\<lambda>x. f x * g x) field_differentiable at x within ?T"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
using field_differentiable_at_within
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) field_differentiable at x
?f field_differentiable at ?x \<Longrightarrow> ?f field_differentiable at ?x within ?S

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) field_differentiable at x within interior (S \<inter> S')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) field_differentiable_on interior (S \<inter> S')

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
have "deriv (\<lambda>x. f x * g x) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
have "deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
[PROOF STEP]
by (simp add: assms once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. f x * deriv g x + deriv f x * g x) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * deriv g x + deriv f x * g x) field_differentiable at x
[PROOF STEP]
by (rule field_differentiable_add, simp_all add: field_differentiable_mult assms once_field_differentiable_at deriv_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * deriv g x + deriv f x * g x) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
(\<lambda>x. f x * deriv g x + deriv f x * g x) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
(\<lambda>x. f x * deriv g x + deriv f x * g x) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
using assms DERIV_deriv_iff_field_differentiable
            DERIV_cong_ev[of x x "deriv (\<lambda>x. f x * g x)" "\<lambda>x. f x * deriv g x + deriv f x * g x"]
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x
(\<lambda>x. f x * deriv g x + deriv f x * g x) field_differentiable at x
f twice_field_differentiable_at x
g twice_field_differentiable_at x
(?f has_field_derivative deriv ?f ?x) (at ?x) = (?f field_differentiable at ?x)
\<lbrakk>x = x; \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. f x * g x) x = f x * deriv g x + deriv f x * g x; ?u = ?v\<rbrakk> \<Longrightarrow> (deriv (\<lambda>x. f x * g x) has_field_derivative ?u) (at x) = ((\<lambda>x. f x * deriv g x + deriv f x * g x) has_field_derivative ?v) (at x)

goal (1 subgoal):
 1. deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
by (simp add: eventually_deriv_mult field_differentiable_def)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x * g x) field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x * g x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x * g x) field_differentiable_on interior (S \<inter> S')
deriv (\<lambda>x. f x * g x) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) field_differentiable_on interior (S \<inter> S')
deriv (\<lambda>x. f x * g x) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
using twice_field_differentiable_at_def x_int_T
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) field_differentiable_on interior (S \<inter> S')
deriv (\<lambda>x. f x * g x) field_differentiable at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x
x \<in> interior (interior (S \<inter> S'))

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) twice_field_differentiable_at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deriv_sin [simp]: "deriv sin a = cos a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv sin a = cos a
[PROOF STEP]
by (simp add: DERIV_imp_deriv)


[STATEMENT]
lemma deriv_sinf [simp]: "deriv sin = (\<lambda>x. cos x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv sin = cos
[PROOF STEP]
by auto


[STATEMENT]
lemma deriv_cos [simp]: "deriv cos a = - sin a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv cos a = - sin a
[PROOF STEP]
by (simp add: DERIV_imp_deriv)


[STATEMENT]
lemma deriv_cosf [simp]: "deriv cos = (\<lambda>x. - sin x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv cos = (\<lambda>x. - sin x)
[PROOF STEP]
by auto


[STATEMENT]
lemma deriv_sin_minus [simp]:
  "deriv (\<lambda>x. - sin x) a = - deriv (\<lambda>x. sin x) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. - sin x) a = - deriv sin a
[PROOF STEP]
by (simp add: DERIV_imp_deriv Deriv.field_differentiable_minus)


[STATEMENT]
lemma twice_field_differentiable_at_sin [simp, intro]:
  "sin twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin twice_field_differentiable_at x
[PROOF STEP]
by (auto intro!: exI [of _ UNIV] simp add: field_differentiable_at_sin
      field_differentiable_on_def twice_field_differentiable_at_def field_differentiable_at_cos)


[STATEMENT]
lemma twice_field_differentiable_at_sin_fun [intro]:
  assumes "f twice_field_differentiable_at x"
  shows   "(\<lambda>x. sin (f x)) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sin (f x)) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms twice_field_differentiable_at_compose)


[STATEMENT]
lemma twice_field_differentiable_at_cos [simp, intro]:
  "cos twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos twice_field_differentiable_at x
[PROOF STEP]
by (auto intro!: exI [of _ UNIV] simp add:  field_differentiable_within_sin field_differentiable_minus
      field_differentiable_on_def twice_field_differentiable_at_def field_differentiable_at_cos)


[STATEMENT]
lemma twice_field_differentiable_at_cos_fun [intro]:
  assumes "f twice_field_differentiable_at x"
  shows   "(\<lambda>x. cos (f x)) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. cos (f x)) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms twice_field_differentiable_at_compose)


[STATEMENT]
lemma deriv_exp [simp]: "deriv exp x = exp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv exp x = exp x
[PROOF STEP]
using DERIV_exp DERIV_imp_deriv
[PROOF STATE]
proof (prove)
using this:
(exp has_field_derivative exp ?x) (at ?x)
(?f has_field_derivative ?f') (at ?x) \<Longrightarrow> deriv ?f ?x = ?f'

goal (1 subgoal):
 1. deriv exp x = exp x
[PROOF STEP]
by blast


[STATEMENT]
lemma deriv_expf [simp]: "deriv exp = exp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv exp = exp
[PROOF STEP]
by (simp add: ext)


[STATEMENT]
lemma deriv_deriv_exp [simp]: "deriv (deriv exp) x = exp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv exp) x = exp x
[PROOF STEP]
by simp


[STATEMENT]
lemma twice_field_differentiable_at_exp [simp, intro]:
  "exp twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exp twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. exp field_differentiable at x"
   and "deriv exp field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. exp field_differentiable at x &&& deriv exp field_differentiable at x
[PROOF STEP]
by (simp_all add: field_differentiable_within_exp)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. exp field_differentiable at x
deriv exp field_differentiable at x

goal (1 subgoal):
 1. exp twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. exp field_differentiable at x
deriv exp field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. exp field_differentiable at x
deriv exp field_differentiable at x

goal (1 subgoal):
 1. exp twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. exp field_differentiable at x
deriv exp field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. exp field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv exp field_differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
exp twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_exp_fun [simp, intro]:
  assumes "f twice_field_differentiable_at x"
  shows "(\<lambda>x. exp (f x)) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. exp (f x)) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms twice_field_differentiable_at_compose)


[STATEMENT]
lemma deriv_real_sqrt [simp]: "x > 0 \<Longrightarrow> deriv sqrt x = inverse (sqrt x) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> deriv sqrt x = inverse (sqrt x) / 2
[PROOF STEP]
using DERIV_imp_deriv DERIV_real_sqrt
[PROOF STATE]
proof (prove)
using this:
(?f has_field_derivative ?f') (at ?x) \<Longrightarrow> deriv ?f ?x = ?f'
0 < ?x \<Longrightarrow> (sqrt has_real_derivative inverse (sqrt ?x) / 2) (at ?x)

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> deriv sqrt x = inverse (sqrt x) / 2
[PROOF STEP]
by blast


[STATEMENT]
lemma has_real_derivative_inverse_sqrt:
  assumes "x > 0"
  shows "((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)
[PROOF STEP]
have inv_sqrt_mult: "(inverse (sqrt x)/2) * (sqrt x * 2) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (sqrt x) / 2 * (sqrt x * 2) = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. inverse (sqrt x) / 2 * (sqrt x * 2) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse (sqrt x) / 2 * (sqrt x * 2) = 1

goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)
[PROOF STEP]
have inv_sqrt_mult2: "(- inverse ((sqrt x)^3)/2)* x * (sqrt x * 2) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - inverse (sqrt x ^ 3) / 2 * x * (sqrt x * 2) = - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. - inverse (sqrt x ^ 3) / 2 * x * (sqrt x * 2) = - 1
[PROOF STEP]
by (simp add: field_simps power3_eq_cube)
[PROOF STATE]
proof (state)
this:
- inverse (sqrt x ^ 3) / 2 * x * (sqrt x * 2) = - 1

goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- inverse (sqrt x ^ 3) / 2 * x * (sqrt x * 2) = - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- inverse (sqrt x ^ 3) / 2 * x * (sqrt x * 2) = - 1

goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
- inverse (sqrt x ^ 3) / 2 * x * (sqrt x * 2) = - 1
0 < x

goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)
[PROOF STEP]
by (safe intro!: DERIV_imp_deriv derivative_eq_intros)
        (auto intro: derivative_eq_intros inv_sqrt_mult [THEN ssubst] inv_sqrt_mult2 [THEN ssubst]
              simp add: divide_simps power3_eq_cube)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt x ^ 3) / 4)) (at x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deriv_deriv_real_sqrt':
  assumes "x > 0"
  shows "deriv (\<lambda>x. inverse (sqrt x) / 2) x = - inverse ((sqrt x)^3)/4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. inverse (sqrt x) / 2) x = - inverse (sqrt x ^ 3) / 4
[PROOF STEP]
by (simp add: DERIV_imp_deriv assms has_real_derivative_inverse_sqrt)


[STATEMENT]
lemma has_real_derivative_deriv_sqrt:
  assumes "x > 0"
  shows "(deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
have "((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
using assms has_real_derivative_inverse_sqrt
[PROOF STATE]
proof (prove)
using this:
0 < x
0 < ?x \<Longrightarrow> ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - (inverse (sqrt ?x ^ 3) / 4)) (at ?x)

goal (1 subgoal):
 1. ((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
fix xa :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
assume "xa \<in> {0<..}"
[PROOF STATE]
proof (state)
this:
xa \<in> {0<..}

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa \<in> {0<..}
[PROOF STEP]
have "inverse (sqrt xa) / 2 = deriv sqrt xa"
[PROOF STATE]
proof (prove)
using this:
xa \<in> {0<..}

goal (1 subgoal):
 1. inverse (sqrt xa) / 2 = deriv sqrt xa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse (sqrt xa) / 2 = deriv sqrt xa

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xa2 \<in> {0<..} \<Longrightarrow> inverse (sqrt ?xa2) / 2 = deriv sqrt ?xa2

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
?xa2 \<in> {0<..} \<Longrightarrow> inverse (sqrt ?xa2) / 2 = deriv sqrt ?xa2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
?xa2 \<in> {0<..} \<Longrightarrow> inverse (sqrt ?xa2) / 2 = deriv sqrt ?xa2

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
using has_field_derivative_transform_within_open [where S="{0 <..}" and f="(\<lambda>x. inverse (sqrt x) / 2)"]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
?xa2 \<in> {0<..} \<Longrightarrow> inverse (sqrt ?xa2) / 2 = deriv sqrt ?xa2
\<lbrakk>((\<lambda>x. inverse (sqrt x) / 2) has_real_derivative ?f') (at ?a); open {0<..}; ?a \<in> {0<..}; \<And>x. x \<in> {0<..} \<Longrightarrow> inverse (sqrt x) / 2 = ?g x\<rbrakk> \<Longrightarrow> (?g has_real_derivative ?f') (at ?a)

goal (1 subgoal):
 1. (deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)
[PROOF STEP]
by (meson assms greaterThan_iff open_greaterThan)
[PROOF STATE]
proof (state)
this:
(deriv sqrt has_real_derivative - inverse (sqrt x ^ 3) / 4) (at x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deriv_deriv_real_sqrt [simp]:
  assumes "x > 0"
  shows "deriv(deriv sqrt) x = - inverse ((sqrt x)^3)/4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv sqrt) x = - inverse (sqrt x ^ 3) / 4
[PROOF STEP]
using DERIV_imp_deriv assms has_real_derivative_deriv_sqrt
[PROOF STATE]
proof (prove)
using this:
(?f has_field_derivative ?f') (at ?x) \<Longrightarrow> deriv ?f ?x = ?f'
0 < x
0 < ?x \<Longrightarrow> (deriv sqrt has_real_derivative - inverse (sqrt ?x ^ 3) / 4) (at ?x)

goal (1 subgoal):
 1. deriv (deriv sqrt) x = - inverse (sqrt x ^ 3) / 4
[PROOF STEP]
by blast


[STATEMENT]
lemma twice_field_differentiable_at_sqrt [simp, intro]:
  assumes "x > 0"
    shows "sqrt twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
have "sqrt field_differentiable_on {0<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt field_differentiable_on {0<..}
[PROOF STEP]
by (metis DERIV_real_sqrt at_within_open field_differentiable_def field_differentiable_on_def
        greaterThan_iff open_greaterThan)
[PROOF STATE]
proof (state)
this:
sqrt field_differentiable_on {0<..}

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sqrt field_differentiable_on {0<..}

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
have "x \<in> interior {0<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> interior {0<..}
[PROOF STEP]
by (metis assms greaterThan_iff interior_interior interior_real_atLeast)
[PROOF STATE]
proof (state)
this:
x \<in> interior {0<..}

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> interior {0<..}

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
have "deriv sqrt field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv sqrt field_differentiable at x
[PROOF STEP]
using assms field_differentiable_def has_real_derivative_deriv_sqrt
[PROOF STATE]
proof (prove)
using this:
0 < x
?f field_differentiable ?F \<equiv> \<exists>f'. (?f has_field_derivative f') ?F
0 < ?x \<Longrightarrow> (deriv sqrt has_real_derivative - inverse (sqrt ?x ^ 3) / 4) (at ?x)

goal (1 subgoal):
 1. deriv sqrt field_differentiable at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
deriv sqrt field_differentiable at x

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sqrt field_differentiable_on {0<..}
x \<in> interior {0<..}
deriv sqrt field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sqrt field_differentiable_on {0<..}
x \<in> interior {0<..}
deriv sqrt field_differentiable at x

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
using twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
sqrt field_differentiable_on {0<..}
x \<in> interior {0<..}
deriv sqrt field_differentiable at x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. sqrt twice_field_differentiable_at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sqrt twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_sqrt_fun [intro]:
  assumes "f twice_field_differentiable_at x"
    and "f x > 0"
  shows "(\<lambda>x. sqrt (f x)) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sqrt (f x)) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms(1) assms(2) twice_field_differentiable_at_compose)


[STATEMENT]
lemma field_differentiable_power [simp]:
  "(\<lambda>x. x ^ n) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
using DERIV_power DERIV_ident field_differentiable_def
[PROOF STATE]
proof (prove)
using this:
(?f has_field_derivative ?D) (at ?x within ?s) \<Longrightarrow> ((\<lambda>x. ?f x ^ ?n) has_field_derivative of_nat ?n * (?D * ?f ?x ^ (?n - Suc 0))) (at ?x within ?s)
((\<lambda>x. x) has_field_derivative (1::?'a)) ?F
?f field_differentiable ?F \<equiv> \<exists>f'. (?f has_field_derivative f') ?F

goal (1 subgoal):
 1. (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
by blast


[STATEMENT]
lemma deriv_power_fun [simp]:
  assumes "f field_differentiable at x"
    shows "deriv (\<lambda>x. f x ^ n) x = of_nat n * deriv f x * f x ^ (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x ^ n) x = of_nat n * deriv f x * f x ^ (n - 1)
[PROOF STEP]
using DERIV_power[of f "deriv f x"]
[PROOF STATE]
proof (prove)
using this:
(f has_field_derivative deriv f x) (at ?x within ?s) \<Longrightarrow> ((\<lambda>x. f x ^ ?n) has_field_derivative of_nat ?n * (deriv f x * f ?x ^ (?n - Suc 0))) (at ?x within ?s)

goal (1 subgoal):
 1. deriv (\<lambda>x. f x ^ n) x = of_nat n * deriv f x * f x ^ (n - 1)
[PROOF STEP]
by (simp add:  DERIV_imp_deriv assms field_differentiable_derivI mult.assoc [symmetric])


[STATEMENT]
lemma deriv_power [simp]:
  "deriv (\<lambda>x. x ^ n) x = of_nat n * x ^ (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) x = of_nat n * x ^ (n - 1)
[PROOF STEP]
using DERIV_power[of "\<lambda>x. x" 1] DERIV_imp_deriv
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. x) has_field_derivative (1::?'b1)) (at ?x within ?s) \<Longrightarrow> ((\<lambda>x. x ^ ?n) has_field_derivative of_nat ?n * ((1::?'b1) * ?x ^ (?n - Suc 0))) (at ?x within ?s)
(?f has_field_derivative ?f') (at ?x) \<Longrightarrow> deriv ?f ?x = ?f'

goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) x = of_nat n * x ^ (n - 1)
[PROOF STEP]
by force


[STATEMENT]
lemma deriv_deriv_power [simp]:
  "deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
have "(\<lambda>x. x ^ (n - 1)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x ^ (n - 1)) field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x ^ (n - 1)) field_differentiable at x

goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. x ^ (n - 1)) field_differentiable at x
[PROOF STEP]
have "deriv (\<lambda>x. of_nat n * x ^ (n - 1)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x ^ (n - 1)) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. of_nat n * x ^ (n - 1)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
by (simp add: diff_diff_add mult.assoc numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. of_nat n * x ^ (n - 1)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)

goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. of_nat n * x ^ (n - 1)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. of_nat n * x ^ (n - 1)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)

goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)
[PROOF STEP]
by (simp add: ext[OF deriv_power])
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>x. x ^ n)) x = of_nat n * of_nat (n - Suc 0) * x ^ (n - 2)

goal:
No subgoals!
[PROOF STEP]
qed