[STATEMENT]
lemma higher_differentiable_on_sqrt: "higher_differentiable_on S (\<lambda>x. sqrt (f x)) n"
  if "higher_differentiable_on S f n" "0 \<notin> f ` S" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sqrt (f x)) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n
0 \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sqrt (f x)) n
[PROOF STEP]
proof (induction n arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>higher_differentiable_on S f 0; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0
0 \<notin> f ` S
open S

goal (2 subgoals):
 1. \<And>f. \<lbrakk>higher_differentiable_on S f 0; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f 0
0 \<notin> f ` S
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 0
0 \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sqrt (f x)) 0
[PROOF STEP]
by (auto simp: continuous_intros)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. sqrt (f x)) 0

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?f n; 0 \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (?f x)) n
higher_differentiable_on S f (Suc n)
0 \<notin> f ` S
open S

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
from Suc.prems(1)
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f (Suc n)
[PROOF STEP]
have fn: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (rule higher_differentiable_on_SucD)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f n
[PROOF STEP]
have "continuous_on S f"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
by (rule higher_differentiable_on_imp_continuous_on)
[PROOF STATE]
proof (state)
this:
continuous_on S f

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
with \<open>open S\<close>
[PROOF STATE]
proof (chain)
picking this:
open S
continuous_on S f
[PROOF STEP]
have op: "open (S \<inter> f -` {0<..})" (is "open ?op")
[PROOF STATE]
proof (prove)
using this:
open S
continuous_on S f

goal (1 subgoal):
 1. open (S \<inter> f -` {0<..})
[PROOF STEP]
by (rule open_continuous_vimage') simp
[PROOF STATE]
proof (state)
this:
open (S \<inter> f -` {0<..})

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
from \<open>open S\<close> \<open>continuous_on S f\<close>
[PROOF STATE]
proof (chain)
picking this:
open S
continuous_on S f
[PROOF STEP]
have on: "open (S \<inter> f -` {..<0})" (is "open ?on")
[PROOF STATE]
proof (prove)
using this:
open S
continuous_on S f

goal (1 subgoal):
 1. open (S \<inter> f -` {..<0})
[PROOF STEP]
by (rule open_continuous_vimage') simp
[PROOF STATE]
proof (state)
this:
open (S \<inter> f -` {..<0})

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
have op': "higher_differentiable_on ?op (\<lambda>x. 1) n" and on': "higher_differentiable_on ?on (\<lambda>x. -1) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<inter> f -` {0<..}) (\<lambda>x. 1::'b) n &&& higher_differentiable_on (S \<inter> f -` {..<0}) (\<lambda>x. - (1::'c)) n
[PROOF STEP]
by (rule higher_differentiable_on_const)+
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<inter> f -` {0<..}) (\<lambda>x. 1::?'b1) n
higher_differentiable_on (S \<inter> f -` {..<0}) (\<lambda>x. - (1::?'c1)) n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on (S \<inter> f -` {0<..}) (\<lambda>x. 1::?'b1) n
higher_differentiable_on (S \<inter> f -` {..<0}) (\<lambda>x. - (1::?'c1)) n
[PROOF STEP]
have i: "higher_differentiable_on (?op \<union> ?on) (\<lambda>x. if 0 < f x then 1::real else - 1) n"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<inter> f -` {0<..}) (\<lambda>x. 1::?'b1) n
higher_differentiable_on (S \<inter> f -` {..<0}) (\<lambda>x. - (1::?'c1)) n

goal (1 subgoal):
 1. higher_differentiable_on (S \<inter> f -` {0<..} \<union> S \<inter> f -` {..<0}) (\<lambda>x. if 0 < f x then 1 else - 1) n
[PROOF STEP]
by (auto intro!: higher_differentiable_on_open_Un op on
          higher_differentiable_on_congI[OF _ op'] higher_differentiable_on_congI[OF _ on'])
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<inter> f -` {0<..} \<union> S \<inter> f -` {..<0}) (\<lambda>x. if 0 < f x then 1 else - 1) n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<inter> f -` {0<..} \<union> S \<inter> f -` {..<0}) (\<lambda>x. if 0 < f x then 1 else - 1) n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
have "?op \<union> ?on = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> f -` {0<..} \<union> S \<inter> f -` {..<0} = S
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?f n; 0 \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (?f x)) n
higher_differentiable_on S f (Suc n)
0 \<notin> f ` S
open S

goal (1 subgoal):
 1. S \<inter> f -` {0<..} \<union> S \<inter> f -` {..<0} = S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<inter> f -` {0<..} \<union> S \<inter> f -` {..<0} = S

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S (\<lambda>x. if 0 < f x then 1 else - 1) n
[PROOF STEP]
have i: "higher_differentiable_on S (\<lambda>x. if 0 < f x then 1::real else - 1) n"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S (\<lambda>x. if 0 < f x then 1 else - 1) n

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. if 0 < f x then 1 else - 1) n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. if 0 < f x then 1 else - 1) n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) n; higher_differentiable_on S f (Suc n); 0 \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
from fn i Suc
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f n
higher_differentiable_on S (\<lambda>x. if 0 < f x then 1 else - 1) n
\<lbrakk>higher_differentiable_on S ?f n; 0 \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (?f x)) n
higher_differentiable_on S f (Suc n)
0 \<notin> f ` S
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n
higher_differentiable_on S (\<lambda>x. if 0 < f x then 1 else - 1) n
\<lbrakk>higher_differentiable_on S ?f n; 0 \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sqrt (?f x)) n
higher_differentiable_on S f (Suc n)
0 \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)
[PROOF STEP]
by (auto simp: sqrt_differentiable_on image_iff frechet_derivative_sqrt
        intro!: sqrt_differentiable higher_differentiable_on_mult higher_differentiable_on_inverse
          higher_differentiable_on_divide higher_differentiable_on_const
        cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. sqrt (f x)) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_frechet_derivativeI:
  "higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) i"
  if "higher_differentiable_on X f (Suc i)" "open X" "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) i
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on X f (Suc i)

goal (1 subgoal):
 1. higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) i
[PROOF STEP]
by (induction i arbitrary: f h) auto


[STATEMENT]
lemma higher_differentiable_on_norm:
  "higher_differentiable_on S (\<lambda>x. norm (f x)) n"
  if "higher_differentiable_on S f n" "0 \<notin> f ` S" "open S"
  for f::"_\<Rightarrow>_::real_inner"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. norm (f x)) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. norm (f x)) n
[PROOF STEP]
proof (induction n arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>higher_differentiable_on S f 0; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0
(0::'d) \<notin> f ` S
open S

goal (2 subgoals):
 1. \<And>f. \<lbrakk>higher_differentiable_on S f 0; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f 0
(0::'d) \<notin> f ` S
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 0
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. norm (f x)) 0
[PROOF STEP]
by (auto simp: continuous_on_norm)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. norm (f x)) 0

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?f n; (0::'d) \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (?f x)) n
higher_differentiable_on S f (Suc n)
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
from Suc.prems(1)
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f (Suc n)
[PROOF STEP]
have fn: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (rule higher_differentiable_on_SucD)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>higher_differentiable_on S ?f n; (0::'d) \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (?f x)) n
higher_differentiable_on S f (Suc n)
(0::'d) \<notin> f ` S
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?f n; (0::'d) \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. norm (?f x)) n
higher_differentiable_on S f (Suc n)
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)
[PROOF STEP]
by (auto simp: continuous_on_norm frechet_derivative_norm image_iff sgn_div_norm
        cong: higher_differentiable_on_cong
        intro!: differentiable_norm_compose_at higher_differentiable_on_inner
          higher_differentiable_on_inverse
          higher_differentiable_on_mult Suc.IH fn)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. norm (f x)) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_Pair:
  "higher_differentiable_on S f k \<Longrightarrow> higher_differentiable_on S g k \<Longrightarrow>
   higher_differentiable_on S (\<lambda>x. (f x, g x)) k"
  if "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on S g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) k
[PROOF STEP]
proof (induction k arbitrary: f g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S f 0; higher_differentiable_on S g 0\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) 0
 2. \<And>k f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on S g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) k; higher_differentiable_on S f (Suc k); higher_differentiable_on S g (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0

goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S f 0; higher_differentiable_on S g 0\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) 0
 2. \<And>k f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on S g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) k; higher_differentiable_on S f (Suc k); higher_differentiable_on S g (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. (f x, g x)) 0
[PROOF STEP]
unfolding higher_differentiable_on.simps
[PROOF STATE]
proof (prove)
using this:
continuous_on S f
continuous_on S g

goal (1 subgoal):
 1. continuous_on S (\<lambda>x. (f x, g x))
[PROOF STEP]
by (auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. (f x, g x)) 0

goal (1 subgoal):
 1. \<And>k f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on S g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) k; higher_differentiable_on S f (Suc k); higher_differentiable_on S g (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on S g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) k; higher_differentiable_on S f (Suc k); higher_differentiable_on S g (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?f k; higher_differentiable_on S ?g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (?f x, ?g x)) k
higher_differentiable_on S f (Suc k)
higher_differentiable_on S g (Suc k)

goal (1 subgoal):
 1. \<And>k f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on S g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) k; higher_differentiable_on S f (Suc k); higher_differentiable_on S g (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>higher_differentiable_on S ?f k; higher_differentiable_on S ?g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (?f x, ?g x)) k
higher_differentiable_on S f (Suc k)
higher_differentiable_on S g (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?f k; higher_differentiable_on S ?g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (?f x, ?g x)) k
higher_differentiable_on S f (Suc k)
higher_differentiable_on S g (Suc k)

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?f k; higher_differentiable_on S ?g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (?f x, ?g x)) k
higher_differentiable_on S f (Suc k)
higher_differentiable_on S g (Suc k)
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)
[PROOF STEP]
unfolding higher_differentiable_on.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?f k; higher_differentiable_on S ?g k\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (?f x, ?g x)) k
(\<forall>x\<in>S. f differentiable at x) \<and> (\<forall>v. higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) k)
(\<forall>x\<in>S. g differentiable at x) \<and> (\<forall>v. higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) k)
open S

goal (1 subgoal):
 1. (\<forall>x\<in>S. (\<lambda>x. (f x, g x)) differentiable at x) \<and> (\<forall>v. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. (f x, g x)) (at x) v) k)
[PROOF STEP]
by (auto simp: frechet_derivative_pair[of f _ g] cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. (f x, g x)) (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_compose':
  "higher_differentiable_on S (\<lambda>x. f (g x)) n"
  if "higher_differentiable_on T f n" "higher_differentiable_on S g n"  "g ` S \<subseteq> T" "open S" "open T"
  for g::"_\<Rightarrow>_::euclidean_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f (g x)) n
[PROOF STEP]
using higher_differentiable_on_compose[of T f n S g] comp_def that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T; open S; open T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n
?f \<circ> ?g = (\<lambda>x. ?f (?g x))
higher_differentiable_on T f n
higher_differentiable_on S g n
g ` S \<subseteq> T
open S
open T

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f (g x)) n
[PROOF STEP]
by (metis (no_types, lifting) higher_differentiable_on_cong)


[STATEMENT]
lemma higher_differentiable_on_fst:
  "higher_differentiable_on (S \<times> T) fst k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) fst k
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on (S \<times> T) fst 0
 2. \<And>k. higher_differentiable_on (S \<times> T) fst k \<Longrightarrow> higher_differentiable_on (S \<times> T) fst (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> T) fst k

goal (2 subgoals):
 1. higher_differentiable_on (S \<times> T) fst 0
 2. \<And>k. higher_differentiable_on (S \<times> T) fst k \<Longrightarrow> higher_differentiable_on (S \<times> T) fst (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on (S \<times> T) fst k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> T) fst k

goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) fst (Suc k)
[PROOF STEP]
unfolding higher_differentiable_on.simps
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> T) fst k

goal (1 subgoal):
 1. (\<forall>x\<in>S \<times> T. fst differentiable at x) \<and> (\<forall>v. higher_differentiable_on (S \<times> T) (\<lambda>x. frechet_derivative fst (at x) v) k)
[PROOF STEP]
by (auto simp: differentiable_at_fst frechet_derivative_fst frechet_derivative_id higher_differentiable_on_const)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> T) fst (Suc k)

goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) fst 0
[PROOF STEP]
qed (auto simp: higher_differentiable_on.simps continuous_on_fst)


[STATEMENT]
lemma higher_differentiable_on_snd:
  "higher_differentiable_on (S \<times> T) snd k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) snd k
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on (S \<times> T) snd 0
 2. \<And>k. higher_differentiable_on (S \<times> T) snd k \<Longrightarrow> higher_differentiable_on (S \<times> T) snd (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> T) snd k

goal (2 subgoals):
 1. higher_differentiable_on (S \<times> T) snd 0
 2. \<And>k. higher_differentiable_on (S \<times> T) snd k \<Longrightarrow> higher_differentiable_on (S \<times> T) snd (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on (S \<times> T) snd k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> T) snd k

goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) snd (Suc k)
[PROOF STEP]
unfolding higher_differentiable_on.simps
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> T) snd k

goal (1 subgoal):
 1. (\<forall>x\<in>S \<times> T. snd differentiable at x) \<and> (\<forall>v. higher_differentiable_on (S \<times> T) (\<lambda>x. frechet_derivative snd (at x) v) k)
[PROOF STEP]
by (auto intro!: continuous_intros
        simp: differentiable_at_snd frechet_derivative_snd frechet_derivative_id higher_differentiable_on_const)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> T) snd (Suc k)

goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) snd 0
[PROOF STEP]
qed (auto simp: higher_differentiable_on.simps continuous_on_snd)


[STATEMENT]
lemma higher_differentiable_on_fst_comp:
  "higher_differentiable_on S (\<lambda>x. fst (f x)) k"
  if "higher_differentiable_on S f k" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. fst (f x)) k
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f k
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. fst (f x)) k
[PROOF STEP]
by (induction k arbitrary: f)
    (auto intro!: continuous_intros differentiable_at_fst
      cong: higher_differentiable_on_cong
      simp: higher_differentiable_on.simps frechet_derivative_fst)


[STATEMENT]
lemma higher_differentiable_on_snd_comp:
  "higher_differentiable_on S (\<lambda>x. snd (f x)) k"
  if "higher_differentiable_on S f k" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. snd (f x)) k
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f k
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. snd (f x)) k
[PROOF STEP]
by (induction k arbitrary: f)
    (auto intro!: continuous_intros differentiable_at_snd
      cong: higher_differentiable_on_cong
      simp: higher_differentiable_on.simps frechet_derivative_snd)


[STATEMENT]
lemma higher_differentiable_on_Pair':
  "higher_differentiable_on S f k \<Longrightarrow> higher_differentiable_on T g k \<Longrightarrow>
   higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) k"
  if S: "open S" and T: "open T"
  for f::"_::euclidean_space\<Rightarrow>_" and g::"_::euclidean_space\<Rightarrow>_"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>higher_differentiable_on S f k; higher_differentiable_on T g k\<rbrakk> \<Longrightarrow> higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) k
[PROOF STEP]
by (auto intro!: higher_differentiable_on_Pair open_Times S T
      higher_differentiable_on_fst
      higher_differentiable_on_snd
      higher_differentiable_on_compose'[where f=f and T=S]
      higher_differentiable_on_compose'[where f=g and T=T])


[STATEMENT]
lemma higher_differentiable_on_sin: "higher_differentiable_on S (\<lambda>x. sin (f x::real)) n"
  and higher_differentiable_on_cos: "higher_differentiable_on S (\<lambda>x. cos (f x::real)) n"
  if f: "higher_differentiable_on S f n" and S: "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sin (f x)) n &&& higher_differentiable_on S (\<lambda>x. cos (f x)) n
[PROOF STEP]
unfolding atomize_conj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on S f 0 \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) 0 \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) 0
 2. \<And>n. \<lbrakk>higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n; higher_differentiable_on S f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) (Suc n) \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
higher_differentiable_on S f (Suc n)

goal (2 subgoals):
 1. higher_differentiable_on S f 0 \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) 0 \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) 0
 2. \<And>n. \<lbrakk>higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n; higher_differentiable_on S f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) (Suc n) \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
higher_differentiable_on S f (Suc n)
[PROOF STEP]
have "higher_differentiable_on S f n"
    "higher_differentiable_on S (\<lambda>x. sin (f x)) n"
    "higher_differentiable_on S (\<lambda>x. cos (f x)) n"
    "\<And>x. x \<in> S \<Longrightarrow> f differentiable at x"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. (higher_differentiable_on S f n &&& higher_differentiable_on S (\<lambda>x. sin (f x)) n) &&& higher_differentiable_on S (\<lambda>x. cos (f x)) n &&& (\<And>x. x \<in> S \<Longrightarrow> f differentiable at x)
[PROOF STEP]
using higher_differentiable_on_SucD
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
higher_differentiable_on S f (Suc n)
higher_differentiable_on ?S ?f (Suc ?n) \<Longrightarrow> higher_differentiable_on ?S ?f ?n

goal (1 subgoal):
 1. (higher_differentiable_on S f n &&& higher_differentiable_on S (\<lambda>x. sin (f x)) n) &&& higher_differentiable_on S (\<lambda>x. cos (f x)) n &&& (\<And>x. x \<in> S \<Longrightarrow> f differentiable at x)
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n
higher_differentiable_on S (\<lambda>x. sin (f x)) n
higher_differentiable_on S (\<lambda>x. cos (f x)) n
?x \<in> S \<Longrightarrow> f differentiable at ?x

goal (2 subgoals):
 1. higher_differentiable_on S f 0 \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) 0 \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) 0
 2. \<And>n. \<lbrakk>higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n; higher_differentiable_on S f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) (Suc n) \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) (Suc n)
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
higher_differentiable_on S f (Suc n)
higher_differentiable_on S f n
higher_differentiable_on S (\<lambda>x. sin (f x)) n
higher_differentiable_on S (\<lambda>x. cos (f x)) n
?x \<in> S \<Longrightarrow> f differentiable at ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) n \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) n
higher_differentiable_on S f (Suc n)
higher_differentiable_on S f n
higher_differentiable_on S (\<lambda>x. sin (f x)) n
higher_differentiable_on S (\<lambda>x. cos (f x)) n
?x \<in> S \<Longrightarrow> f differentiable at ?x

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. sin (f x)) (Suc n) \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) (Suc n)
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps sin_differentiable_at cos_differentiable_at
        frechet_derivative_sin frechet_derivative_cos S
        intro!: higher_differentiable_on_mult higher_differentiable_on_uminus
        cong: higher_differentiable_on_cong[OF S])
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. sin (f x)) (Suc n) \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) (Suc n)

goal (1 subgoal):
 1. higher_differentiable_on S f 0 \<Longrightarrow> higher_differentiable_on S (\<lambda>x. sin (f x)) 0 \<and> higher_differentiable_on S (\<lambda>x. cos (f x)) 0
[PROOF STEP]
qed (auto simp: higher_differentiable_on.simps intro!: continuous_intros)


[STATEMENT]
lemma frechet_derivative_nth_derivative_commute:
  "frechet_derivative (\<lambda>x. nth_derivative i f x h) (at x) h =
    nth_derivative i (\<lambda>x. frechet_derivative f (at x) h) x h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. nth_derivative i f x h) (at x) h = nth_derivative i (\<lambda>x. frechet_derivative f (at x) h) x h
[PROOF STEP]
by (induction i arbitrary: f) auto


[STATEMENT]
lemma nth_derivative_funpow:
  "nth_derivative i f x h = ((\<lambda>f x. frechet_derivative f (at x) h) ^^ i) f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_derivative i f x h = ((\<lambda>f x. frechet_derivative f (at x) h) ^^ i) f x
[PROOF STEP]
by (induction i arbitrary: f) (auto simp del: funpow.simps simp: funpow_Suc_right)


[STATEMENT]
lemma nth_derivative_exists:
  "\<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and>
    f' h = nth_derivative (Suc i) f x h"
  if "higher_differentiable_on X f (Suc i)" "open X" "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on X f (Suc i)

goal (1 subgoal):
 1. \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h
[PROOF STEP]
proof (induction i arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. higher_differentiable_on X f (Suc 0) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative 0 f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc 0) f x h
 2. \<And>i f. \<lbrakk>\<And>f. higher_differentiable_on X f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h; higher_differentiable_on X f (Suc (Suc i))\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on X f (Suc 0)

goal (2 subgoals):
 1. \<And>f. higher_differentiable_on X f (Suc 0) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative 0 f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc 0) f x h
 2. \<And>i f. \<lbrakk>\<And>f. higher_differentiable_on X f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h; higher_differentiable_on X f (Suc (Suc i))\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on X f (Suc i)
open X
x \<in> X
higher_differentiable_on X f (Suc 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on X f (Suc i)
open X
x \<in> X
higher_differentiable_on X f (Suc 0)

goal (1 subgoal):
 1. \<exists>f'. ((\<lambda>x. nth_derivative 0 f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc 0) f x h
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps that dest!: frechet_derivative_worksI)
[PROOF STATE]
proof (state)
this:
\<exists>f'. ((\<lambda>x. nth_derivative 0 f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc 0) f x h

goal (1 subgoal):
 1. \<And>i f. \<lbrakk>\<And>f. higher_differentiable_on X f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h; higher_differentiable_on X f (Suc (Suc i))\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i f. \<lbrakk>\<And>f. higher_differentiable_on X f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h; higher_differentiable_on X f (Suc (Suc i))\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on X ?f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i ?f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) ?f x h
higher_differentiable_on X f (Suc (Suc i))

goal (1 subgoal):
 1. \<And>i f. \<lbrakk>\<And>f. higher_differentiable_on X f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h; higher_differentiable_on X f (Suc (Suc i))\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on X f (Suc (Suc i))
[PROOF STEP]
have "\<And>x. x \<in> X \<Longrightarrow> f differentiable at x" "higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) (Suc i)"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on X f (Suc (Suc i))

goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> f differentiable at x) &&& higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) (Suc i)
[PROOF STEP]
unfolding higher_differentiable_on.simps(2)[where n = "Suc i"]
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>X. f differentiable at x) \<and> (\<forall>v. higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) v) (Suc i))

goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> f differentiable at x) &&& higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> f differentiable at ?x
higher_differentiable_on X (\<lambda>x. frechet_derivative f (at x) h) (Suc i)

goal (1 subgoal):
 1. \<And>i f. \<lbrakk>\<And>f. higher_differentiable_on X f (Suc i) \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative i f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) f x h; higher_differentiable_on X f (Suc (Suc i))\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
from Suc.IH[OF this(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f'. ((\<lambda>x. nth_derivative i (\<lambda>a. frechet_derivative f (at a) h) x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) (\<lambda>a. frechet_derivative f (at a) h) x h
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>f'. ((\<lambda>x. nth_derivative i (\<lambda>a. frechet_derivative f (at a) h) x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc i) (\<lambda>a. frechet_derivative f (at a) h) x h

goal (1 subgoal):
 1. \<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f'. ((\<lambda>x. nth_derivative (Suc i) f x h) has_derivative f') (at x) \<and> f' h = nth_derivative (Suc (Suc i)) f x h

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_derivatives_exists:
  assumes "higher_differentiable_on X f n" "open X"
  obtains Df where
    "\<And>a h. Df a 0 h = f a"
    "\<And>a h i. i < n \<Longrightarrow> a \<in> X \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a)"
    "\<And>a i. i \<le> n \<Longrightarrow> a \<in> X \<Longrightarrow> Df a i H = nth_derivative i f a H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "higher_differentiable_on X f (Suc i)" if "i < n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on X f (Suc i)
[PROOF STEP]
apply (rule higher_differentiable_on_le[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc i \<le> n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. Suc i \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> higher_differentiable_on X f (Suc ?i)

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from nth_derivative_exists[OF this assms(2)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i < n; ?x \<in> X\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative ?i f x ?h) has_derivative f') (at ?x) \<and> f' ?h = nth_derivative (Suc ?i) f ?x ?h
[PROOF STEP]
have "\<forall>i\<in>{..<n}. \<forall>x \<in> X. \<exists>f'. ((\<lambda>x. nth_derivative i f x H) has_derivative f') (at x) \<and> f' H = nth_derivative (Suc i) f x H"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < n; ?x \<in> X\<rbrakk> \<Longrightarrow> \<exists>f'. ((\<lambda>x. nth_derivative ?i f x ?h) has_derivative f') (at ?x) \<and> f' ?h = nth_derivative (Suc ?i) f ?x ?h

goal (1 subgoal):
 1. \<forall>i\<in>{..<n}. \<forall>x\<in>X. \<exists>f'. ((\<lambda>x. nth_derivative i f x H) has_derivative f') (at x) \<and> f' H = nth_derivative (Suc i) f x H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{..<n}. \<forall>x\<in>X. \<exists>f'. ((\<lambda>x. nth_derivative i f x H) has_derivative f') (at x) \<and> f' H = nth_derivative (Suc i) f x H

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this[unfolded bchoice_iff]
[PROOF STATE]
proof (chain)
picking this:
\<exists>fa. \<forall>i\<in>{..<n}. \<forall>x\<in>X. ((\<lambda>x. nth_derivative i f x H) has_derivative fa i x) (at x) \<and> fa i x H = nth_derivative (Suc i) f x H
[PROOF STEP]
obtain f' where f': "i < n \<Longrightarrow> x \<in> X \<Longrightarrow> ((\<lambda>x. nth_derivative i f x H) has_derivative f' x i) (at x)"
    "i < n \<Longrightarrow> x \<in> X \<Longrightarrow> f' x i H = nth_derivative (Suc i) f x H" for x i
[PROOF STATE]
proof (prove)
using this:
\<exists>fa. \<forall>i\<in>{..<n}. \<forall>x\<in>X. ((\<lambda>x. nth_derivative i f x H) has_derivative fa i x) (at x) \<and> fa i x H = nth_derivative (Suc i) f x H

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>\<And>x i. \<lbrakk>i < n; x \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>x. nth_derivative i f x H) has_derivative f' x i) (at x); \<And>x i. \<lbrakk>i < n; x \<in> X\<rbrakk> \<Longrightarrow> f' x i H = nth_derivative (Suc i) f x H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?x \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>x. nth_derivative ?i f x H) has_derivative f' ?x ?i) (at ?x)
\<lbrakk>?i < n; ?x \<in> X\<rbrakk> \<Longrightarrow> f' ?x ?i H = nth_derivative (Suc ?i) f ?x H

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define Df where "Df a i h = (if i = 0 then f a else f' a (i - 1) h)" for a i h
[PROOF STATE]
proof (state)
this:
Df ?a ?i ?h = (if ?i = 0 then f ?a else f' ?a (?i - 1) ?h)

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "Df a 0 h = f a" for a h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Df a 0 h = f a
[PROOF STEP]
by (auto simp: Df_def)
[PROOF STATE]
proof (state)
this:
Df ?a 0 ?h = f ?a

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Df ?a 0 ?h = f ?a

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "i < n \<Longrightarrow> a \<in> X \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a)"
    for i a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a)
[PROOF STEP]
apply (auto simp: Df_def[abs_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. if i = 0 then f a else f' a (i - 1) H) has_derivative f' a i) (at a)
[PROOF STEP]
using _ \<open>open X\<close>
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
open X

goal (1 subgoal):
 1. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. if i = 0 then f a else f' a (i - 1) H) has_derivative f' a i) (at a)
[PROOF STEP]
apply (rule has_derivative_transform_within_open)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> (?f2 has_derivative f' a i) (at a)
 2. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> a \<in> X
 3. \<And>x. \<lbrakk>i < n; a \<in> X; x \<in> X\<rbrakk> \<Longrightarrow> ?f2 x = (if i = 0 then f x else f' x (i - 1) H)
[PROOF STEP]
apply (rule f')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> i < n
 2. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> a \<in> X
 3. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> a \<in> X
 4. \<And>x. \<lbrakk>i < n; a \<in> X; x \<in> X\<rbrakk> \<Longrightarrow> nth_derivative i f x H = (if i = 0 then f x else f' x (i - 1) H)
[PROOF STEP]
apply (auto simp: f')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a ?i H) has_derivative Df ?a (Suc ?i)) (at ?a)

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a ?i H) has_derivative Df ?a (Suc ?i)) (at ?a)

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "i \<le> n \<Longrightarrow> a \<in> X \<Longrightarrow> Df a i H = nth_derivative i f a H" for i a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H
[PROOF STEP]
by (auto simp: Df_def f')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i \<le> n; ?a \<in> X\<rbrakk> \<Longrightarrow> Df ?a ?i H = nth_derivative ?i f ?a H

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> X\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Df ?a 0 ?h = f ?a
\<lbrakk>?i < n; ?a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a ?i H) has_derivative Df ?a (Suc ?i)) (at ?a)
\<lbrakk>?i \<le> n; ?a \<in> X\<rbrakk> \<Longrightarrow> Df ?a ?i H = nth_derivative ?i f ?a H
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Df ?a 0 ?h = f ?a
\<lbrakk>?i < n; ?a \<in> X\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a ?i H) has_derivative Df ?a (Suc ?i)) (at ?a)
\<lbrakk>?i \<le> n; ?a \<in> X\<rbrakk> \<Longrightarrow> Df ?a ?i H = nth_derivative ?i f ?a H

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_derivative_differentiable:
  assumes "higher_differentiable_on S f (Suc n)" "x \<in> S"
  shows "(\<lambda>x. nth_derivative n f x v) differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. nth_derivative n f x v) differentiable at x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)
x \<in> S

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative n f x v) differentiable at x
[PROOF STEP]
by (induction n arbitrary: f) (auto simp: higher_differentiable_on.simps)


[STATEMENT]
lemma higher_differentiable_on_imp_continuous_nth_derivative:
  assumes "higher_differentiable_on S f n"
  shows "continuous_on S (\<lambda>x. nth_derivative n f x v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (\<lambda>x. nth_derivative n f x v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. continuous_on S (\<lambda>x. nth_derivative n f x v)
[PROOF STEP]
by (induction n arbitrary: f) (auto simp: higher_differentiable_on.simps)


[STATEMENT]
lemma frechet_derivative_at_real_eq_scaleR:
  "frechet_derivative f (at x) v = v *\<^sub>R frechet_derivative f (at x) 1"
  if "f differentiable (at x)" "NO_MATCH 1 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative f (at x) v = v *\<^sub>R frechet_derivative f (at x) 1
[PROOF STEP]
by (simp add: frechet_derivative_eq_vector_derivative that)


[STATEMENT]
lemma higher_differentiable_on_real_Suc:
  "higher_differentiable_on S f (Suc n) \<longleftrightarrow>
     (\<forall>x\<in>S. f differentiable (at x)) \<and>
      (higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) 1) n)"
  if "open S"
  for S::"real set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n) = ((\<forall>x\<in>S. f differentiable at x) \<and> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) 1) n)
[PROOF STEP]
using \<open>open S\<close>
[PROOF STATE]
proof (prove)
using this:
open S

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n) = ((\<forall>x\<in>S. f differentiable at x) \<and> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) 1) n)
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps frechet_derivative_at_real_eq_scaleR
      intro!: higher_differentiable_on_scaleR higher_differentiable_on_const
      cong: higher_differentiable_on_cong)


[STATEMENT]
lemma higher_differentiable_on_real_SucI:
  fixes S::"real set"
  assumes
    "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative n f x 1) differentiable at x"
    "continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1)"
    "higher_differentiable_on S f n"
    and o: "open S"
  shows "higher_differentiable_on S f (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative n f x 1) differentiable at ?x
continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1)
higher_differentiable_on S f n
open S

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
proof (induction n arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative 0 f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc 0) f x 1); higher_differentiable_on S f 0; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc 0)
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative n f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1); higher_differentiable_on S f n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n); \<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative (Suc n) f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc (Suc n)) f x 1); higher_differentiable_on S f (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative 0 f x 1) differentiable at ?x
continuous_on S (\<lambda>x. nth_derivative (Suc 0) f x 1)
higher_differentiable_on S f 0
open S

goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative 0 f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc 0) f x 1); higher_differentiable_on S f 0; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc 0)
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative n f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1); higher_differentiable_on S f n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n); \<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative (Suc n) f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc (Suc n)) f x 1); higher_differentiable_on S f (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative 0 f x 1) differentiable at ?x
continuous_on S (\<lambda>x. nth_derivative (Suc 0) f x 1)
higher_differentiable_on S f 0
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative 0 f x 1) differentiable at ?x
continuous_on S (\<lambda>x. nth_derivative (Suc 0) f x 1)
higher_differentiable_on S f 0
open S

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc 0)
[PROOF STEP]
by (auto simp: higher_differentiable_on_real_Suc higher_differentiable_on.simps(1) o)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f (Suc 0)

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative n f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1); higher_differentiable_on S f n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n); \<And>x. x \<in> S \<Longrightarrow> (\<lambda>x. nth_derivative (Suc n) f x 1) differentiable at x; continuous_on S (\<lambda>x. nth_derivative (Suc (Suc n)) f x 1); higher_differentiable_on S f (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc (Suc n))
[PROOF STEP]
qed (fastforce simp: higher_differentiable_on_real_Suc)


[STATEMENT]
lemma higher_differentiable_on_real_Suc':
  "open S \<Longrightarrow> higher_differentiable_on S f (Suc n) \<longleftrightarrow>
    (\<forall>v. continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1)) \<and>
    (\<forall>x\<in>S. \<forall>v. (\<lambda>x. nth_derivative n f x 1) differentiable (at x)) \<and> higher_differentiable_on S f n"
  for S::"real set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open S \<Longrightarrow> higher_differentiable_on S f (Suc n) = ((\<forall>v. continuous_on S (\<lambda>x. nth_derivative (Suc n) f x 1)) \<and> (\<forall>x\<in>S. \<forall>v. (\<lambda>x. nth_derivative n f x 1) differentiable at x) \<and> higher_differentiable_on S f n)
[PROOF STEP]
apply (auto simp: nth_derivative_differentiable
      dest: higher_differentiable_on_SucD
      intro: higher_differentiable_on_real_SucI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>open S; higher_differentiable_on S f (Suc n)\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. nth_derivative n (\<lambda>x. frechet_derivative f (at x) 1) x 1)
[PROOF STEP]
by (auto simp: higher_differentiable_on_real_Suc higher_differentiable_on.simps(1)
      higher_differentiable_on_imp_continuous_nth_derivative)


[STATEMENT]
lemma closed_segment_subsetD:
  "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> (X + x *\<^sub>R H) \<in> S"
  if "closed_segment X (X + H) \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> X + x *\<^sub>R H \<in> S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
closed_segment X (X + H) \<subseteq> S

goal (1 subgoal):
 1. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> X + x *\<^sub>R H \<in> S
[PROOF STEP]
by (rule subsetD) (auto simp: closed_segment_def algebra_simps intro!: exI[where x=x])


[STATEMENT]
lemma higher_differentiable_Taylor:
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::banach"
    and H::"'a"
    and Df::"'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
  assumes "n > 0"
  assumes hd: "higher_differentiable_on S f n" "open S"
  assumes cs: "closed_segment X (X + H) \<subseteq> S"
  defines "i \<equiv> \<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R nth_derivative n f (X + x *\<^sub>R H) H"
  shows "(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}" (is ?th1)
  and "f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i" (is ?th2)
  and "i integrable_on {0..1}" (is ?th3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1} &&& f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i &&& i integrable_on {0..1}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
from higher_derivatives_exists[OF hd]
[PROOF STATE]
proof (chain)
picking this:
(\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i ?H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> S\<rbrakk> \<Longrightarrow> Df a i ?H = nth_derivative i f a ?H\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain Df where Df: "(\<And>a h. Df a 0 h = f a)"
    "(\<And>a h i. i < n \<Longrightarrow> a \<in> S \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a))"
    "\<And>a i. i \<le> n \<Longrightarrow> a \<in> S \<Longrightarrow> Df a i H = nth_derivative i f a H"
[PROOF STATE]
proof (prove)
using this:
(\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i ?H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> S\<rbrakk> \<Longrightarrow> Df a i ?H = nth_derivative i f a ?H\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Df. \<lbrakk>\<And>a h. Df a 0 h = f a; \<And>a h i. \<lbrakk>i < n; a \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a i H) has_derivative Df a (Suc i)) (at a); \<And>a i. \<lbrakk>i \<le> n; a \<in> S\<rbrakk> \<Longrightarrow> Df a i H = nth_derivative i f a H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Df ?a1 0 ?h1 = f ?a1
\<lbrakk>?i1 < n; ?a1 \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a ?i1 H) has_derivative Df ?a1 (Suc ?i1)) (at ?a1)
\<lbrakk>?i1 \<le> n; ?a1 \<in> S\<rbrakk> \<Longrightarrow> Df ?a1 ?i1 H = nth_derivative ?i1 f ?a1 H

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
from multivariate_Taylor_integral[OF \<open>n > 0\<close>, of Df H f X, OF Df(1,2)] cs
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> i < n; \<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> a \<in> S; closed_segment X (X + H) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
\<lbrakk>\<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> i < n; \<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> a \<in> S; closed_segment X (X + H) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} (\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H)
\<lbrakk>\<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> i < n; \<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> a \<in> S; closed_segment X (X + H) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> (\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) integrable_on {0..1}
closed_segment X (X + H) \<subseteq> S
[PROOF STEP]
have mt: "((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral
     f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H))
     {0..1}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> i < n; \<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> a \<in> S; closed_segment X (X + H) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
\<lbrakk>\<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> i < n; \<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> a \<in> S; closed_segment X (X + H) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} (\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H)
\<lbrakk>\<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> i < n; \<And>a i d. \<lbrakk>a \<in> closed_segment X (X + H); i < n\<rbrakk> \<Longrightarrow> a \<in> S; closed_segment X (X + H) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> (\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) integrable_on {0..1}
closed_segment X (X + H) \<subseteq> S

goal (1 subgoal):
 1. ((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
from cs
[PROOF STATE]
proof (chain)
picking this:
closed_segment X (X + H) \<subseteq> S
[PROOF STEP]
have "X \<in> S"
[PROOF STATE]
proof (prove)
using this:
closed_segment X (X + H) \<subseteq> S

goal (1 subgoal):
 1. X \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<in> S

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
show ?th1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
[PROOF STEP]
apply (rule has_integral_eq_rhs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (i has_integral ?j) {0..1}
 2. f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) = ?j
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R nth_derivative n f (X + x *\<^sub>R H) H) has_integral ?j) {0..1}
 2. f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) = ?j
[PROOF STEP]
using negligible_empty _ mt
[PROOF STATE]
proof (prove)
using this:
negligible {}
PROP ?psi \<Longrightarrow> PROP ?psi
((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}

goal (2 subgoals):
 1. ((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R nth_derivative n f (X + x *\<^sub>R H) H) has_integral ?j) {0..1}
 2. f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) = ?j
[PROOF STEP]
apply (rule has_integral_spike)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0..1} - {} \<Longrightarrow> ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R nth_derivative n f (X + x *\<^sub>R H) H = ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H
 2. f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) = f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)
[PROOF STEP]
using closed_segment_subsetD[OF cs]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?x; ?x \<le> 1\<rbrakk> \<Longrightarrow> X + ?x *\<^sub>R H \<in> S

goal (2 subgoals):
 1. \<And>x. x \<in> {0..1} - {} \<Longrightarrow> ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R nth_derivative n f (X + x *\<^sub>R H) H = ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H
 2. f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) = f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)
[PROOF STEP]
by (auto simp: Df \<open>X \<in> S\<close>)
[PROOF STATE]
proof (state)
this:
(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}

goal (2 subgoals):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i
 2. i integrable_on {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
[PROOF STEP]
show ?th2 ?th3
[PROOF STATE]
proof (prove)
using this:
(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}

goal (1 subgoal):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i &&& i integrable_on {0..1}
[PROOF STEP]
unfolding has_integral_iff
[PROOF STATE]
proof (prove)
using this:
i integrable_on {0..1} \<and> integral {0..1} i = f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H)

goal (1 subgoal):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i &&& i integrable_on {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} i
i integrable_on {0..1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frechet_derivative_componentwise:
  "frechet_derivative f (at a) v = (\<Sum>i\<in>Basis. (v \<bullet> i) * (frechet_derivative f (at a) i))"
  if "f differentiable at a"
  for f::"'a::euclidean_space \<Rightarrow> real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative f (at a) v = (\<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at a) i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. frechet_derivative f (at a) v = (\<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at a) i)
[PROOF STEP]
have "linear (frechet_derivative f (at a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (frechet_derivative f (at a))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f differentiable at a

goal (1 subgoal):
 1. linear (frechet_derivative f (at a))
[PROOF STEP]
by (rule linear_frechet_derivative)
[PROOF STATE]
proof (state)
this:
linear (frechet_derivative f (at a))

goal (1 subgoal):
 1. frechet_derivative f (at a) v = (\<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at a) i)
[PROOF STEP]
from Linear_Algebra.linear_componentwise[OF this, of v 1]
[PROOF STATE]
proof (chain)
picking this:
frechet_derivative f (at a) v \<bullet> 1 = (\<Sum>i\<in>Basis. v \<bullet> i * (frechet_derivative f (at a) i \<bullet> 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
frechet_derivative f (at a) v \<bullet> 1 = (\<Sum>i\<in>Basis. v \<bullet> i * (frechet_derivative f (at a) i \<bullet> 1))

goal (1 subgoal):
 1. frechet_derivative f (at a) v = (\<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at a) i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
frechet_derivative f (at a) v = (\<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at a) i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_Taylor1:
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::banach"
  assumes hd: "higher_differentiable_on S f 2" "open S"
  assumes cs: "closed_segment X (X + H) \<subseteq> S"
  defines "i \<equiv> \<lambda>x. ((1 - x)) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H"
  shows "(i has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1}"
    and "f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} i"
    and "i integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1} &&& f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} i &&& i integrable_on {0..1}
[PROOF STEP]
using higher_differentiable_Taylor[OF _ hd cs]
[PROOF STATE]
proof (prove)
using this:
0 < 2 \<Longrightarrow> ((\<lambda>x. ((1 - x) ^ (2 - 1) / fact (2 - 1)) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) has_integral f (X + H) - (\<Sum>i<2. (1 / fact i) *\<^sub>R nth_derivative i f X H)) {0..1}
0 < 2 \<Longrightarrow> f (X + H) = (\<Sum>i<2. (1 / fact i) *\<^sub>R nth_derivative i f X H) + integral {0..1} (\<lambda>x. ((1 - x) ^ (2 - 1) / fact (2 - 1)) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H)
0 < 2 \<Longrightarrow> (\<lambda>x. ((1 - x) ^ (2 - 1) / fact (2 - 1)) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) integrable_on {0..1}

goal (1 subgoal):
 1. (i has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1} &&& f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} i &&& i integrable_on {0..1}
[PROOF STEP]
by (auto simp: numeral_2_eq_2 i_def)


[STATEMENT]
lemma differentiable_on_open_blinfunE:
  assumes "f differentiable_on S" "open S"
  obtains f' where "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume "x \<in> S"
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
f differentiable_on S
open S
x \<in> S
[PROOF STEP]
obtain f' where f': "(f has_derivative f') (at x)"
[PROOF STATE]
proof (prove)
using this:
f differentiable_on S
open S
x \<in> S

goal (1 subgoal):
 1. (\<And>f'. (f has_derivative f') (at x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: differentiable_on_openD simp: differentiable_def)
[PROOF STATE]
proof (state)
this:
(f has_derivative f') (at x)

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f has_derivative f') (at x)
[PROOF STEP]
have "bounded_linear f'"
[PROOF STATE]
proof (prove)
using this:
(f has_derivative f') (at x)

goal (1 subgoal):
 1. bounded_linear f'
[PROOF STEP]
by (rule has_derivative_bounded_linear)
[PROOF STATE]
proof (state)
this:
bounded_linear f'

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_linear f'
[PROOF STEP]
obtain bf' where "f' = blinfun_apply bf'"
[PROOF STATE]
proof (prove)
using this:
bounded_linear f'

goal (1 subgoal):
 1. (\<And>bf'. f' = blinfun_apply bf' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
f' = blinfun_apply bf'

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' = blinfun_apply bf'
[PROOF STEP]
have "\<exists>bf'. (f has_derivative blinfun_apply bf') (at x)"
[PROOF STATE]
proof (prove)
using this:
f' = blinfun_apply bf'

goal (1 subgoal):
 1. \<exists>bf'. (f has_derivative blinfun_apply bf') (at x)
[PROOF STEP]
using f'
[PROOF STATE]
proof (prove)
using this:
f' = blinfun_apply bf'
(f has_derivative f') (at x)

goal (1 subgoal):
 1. \<exists>bf'. (f has_derivative blinfun_apply bf') (at x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>bf'. (f has_derivative blinfun_apply bf') (at x)

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> S \<Longrightarrow> \<exists>bf'. (f has_derivative blinfun_apply bf') (at ?x2)

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> S \<Longrightarrow> \<exists>bf'. (f has_derivative blinfun_apply bf') (at ?x2)
[PROOF STEP]
obtain f' where "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> S \<Longrightarrow> \<exists>bf'. (f has_derivative blinfun_apply bf') (at ?x2)

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' ?x)) (at ?x)

goal (1 subgoal):
 1. (\<And>f'. (\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' ?x)) (at ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (f' ?x)) (at ?x)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_blinfunI1:
  "continuous_on X f"
  if "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on X (\<lambda>x. blinfun_apply (f x) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on X f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i \<in> Basis \<Longrightarrow> continuous_on X (\<lambda>x. blinfun_apply (f x) ?i)

goal (1 subgoal):
 1. continuous_on X f
[PROOF STEP]
by (auto simp: continuous_on_def intro: tendsto_componentwise1)


[STATEMENT]
lemma c1_euclidean_blinfunE:
  fixes f::"'a::euclidean_space\<Rightarrow>'b::real_normed_vector"
  assumes "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>x. f' x i)"
  obtains bf' where
    "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S)"
    "continuous_on S bf'"
    "\<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>x. f' x ?i)
[PROOF STEP]
have "bounded_linear (f' x)" if "x \<in> S" for x
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>x. f' x ?i)

goal (1 subgoal):
 1. bounded_linear (f' x)
[PROOF STEP]
by (auto intro!: has_derivative_bounded_linear that)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> bounded_linear (f' ?x)

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> bounded_linear (f' ?x)
[PROOF STEP]
obtain bf' where bf': "\<forall>x \<in> S. f' x = blinfun_apply (bf' x)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> bounded_linear (f' ?x)

goal (1 subgoal):
 1. (\<And>bf'. \<forall>x\<in>S. f' x = blinfun_apply (bf' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> bounded_linear (f' x)) \<Longrightarrow> \<exists>bf'. \<forall>x\<in>S. f' x = blinfun_apply (bf' x)
[PROOF STEP]
apply (rule bchoice)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> bounded_linear (f' x)) \<Longrightarrow> \<forall>x\<in>S. \<exists>y. f' x = blinfun_apply y
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> bounded_linear (f' x); x \<in> S\<rbrakk> \<Longrightarrow> \<exists>y. f' x = blinfun_apply y
[PROOF STEP]
by (metis bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. f' x = blinfun_apply (bf' x)

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>x. f' x ?i)
\<forall>x\<in>S. f' x = blinfun_apply (bf' x)
[PROOF STEP]
have "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>x. f' x ?i)
\<forall>x\<in>S. f' x = blinfun_apply (bf' x)

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' ?x)) (at ?x within S)

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' ?x)) (at ?x within S)

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have f_tendsto: "((\<lambda>n. f' n j) \<longlongrightarrow> f' x j) (at x within S)"
    if "x \<in> S" "j \<in> Basis"
    for x j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>n. f' n j) \<longlongrightarrow> f' x j) (at x within S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>x. f' x ?i)

goal (1 subgoal):
 1. ((\<lambda>n. f' n j) \<longlongrightarrow> f' x j) (at x within S)
[PROOF STEP]
by (auto simp: continuous_on_def that)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> S; ?j \<in> Basis\<rbrakk> \<Longrightarrow> ((\<lambda>n. f' n ?j) \<longlongrightarrow> f' ?x ?j) (at ?x within S)

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "continuous_on S bf'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S bf'
[PROOF STEP]
by (rule continuous_on_blinfunI1) (simp add: bf'[rule_format, symmetric] assms)
[PROOF STATE]
proof (state)
this:
continuous_on S bf'

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
continuous_on S bf'

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x
[PROOF STEP]
using bf'
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. f' x = blinfun_apply (bf' x)

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> blinfun_apply (bf' ?x) = f' ?x

goal (1 subgoal):
 1. (\<And>bf'. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' x)) (at x within S); continuous_on S bf'; \<And>x. x \<in> S \<Longrightarrow> blinfun_apply (bf' x) = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' ?x)) (at ?x within S)
continuous_on S bf'
?x \<in> S \<Longrightarrow> blinfun_apply (bf' ?x) = f' ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (f has_derivative blinfun_apply (bf' ?x)) (at ?x within S)
continuous_on S bf'
?x \<in> S \<Longrightarrow> blinfun_apply (bf' ?x) = f' ?x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_Sigma:
  assumes defined: "y \<in> Pi T X"
  assumes f_cont: "continuous_on (Sigma T X) (\<lambda>(t, x). f t x)"
  assumes y_cont: "continuous_on T y"
  shows "continuous_on T (\<lambda>x. f x (y x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on T (\<lambda>x. f x (y x))
[PROOF STEP]
using
    defined
    continuous_on_compose2[OF
      continuous_on_subset[where t="(\<lambda>x. (x, y x)) ` T", OF f_cont]
      continuous_on_Pair[OF continuous_on_id y_cont]]
[PROOF STATE]
proof (prove)
using this:
y \<in> Pi T X
\<lbrakk>(\<lambda>x. (x, y x)) ` T \<subseteq> Sigma T X; (\<lambda>x. (x, y x)) ` T \<subseteq> (\<lambda>x. (x, y x)) ` T\<rbrakk> \<Longrightarrow> continuous_on T (\<lambda>x. case (x, y x) of (t, x) \<Rightarrow> f t x)

goal (1 subgoal):
 1. continuous_on T (\<lambda>x. f x (y x))
[PROOF STEP]
by auto


[STATEMENT]
lemma continuous_on_Times_swap:
  "continuous_on (X \<times> Y) (\<lambda>(x, y). f x y)"
  if "continuous_on (Y \<times> X) (\<lambda>(y, x). f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (X \<times> Y) (\<lambda>(x, y). f x y)
[PROOF STEP]
using continuous_on_compose2[OF that continuous_on_swap, where s="X \<times> Y"]
[PROOF STATE]
proof (prove)
using this:
prod.swap ` (X \<times> Y) \<subseteq> Y \<times> X \<Longrightarrow> continuous_on (X \<times> Y) (\<lambda>x. case prod.swap x of (y, x) \<Rightarrow> f x y)

goal (1 subgoal):
 1. continuous_on (X \<times> Y) (\<lambda>(x, y). f x y)
[PROOF STEP]
by (auto simp: split_beta' product_swap)