[STATEMENT]
lemma leibniz_rule':
  "\<And>x. x \<in> S \<Longrightarrow>
      ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v)))
          (at x within S)"
  "(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S"
  if "convex S"
    and c1: "\<And>t x. t \<in> cbox a b \<Longrightarrow> x \<in> S \<Longrightarrow> ((\<lambda>x. f x t) has_derivative fx x t) (at x within S)"
    "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on (S \<times> cbox a b) (\<lambda>(x, t). fx x t i)"
    and i: "\<And>x. x \<in> S \<Longrightarrow> f x integrable_on cbox a b"
  for S::"'a::euclidean_space set"
    and f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)) &&& (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have fx1: "continuous_on S (\<lambda>x. fx x t i)" if "t \<in> cbox a b" "i \<in> Basis" for i t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (\<lambda>x. fx x t i)
[PROOF STEP]
by (rule continuous_Sigma[OF _ c1(2), where y="\<lambda>_. t"]) (auto simp: continuous_intros that)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t \<in> cbox a b; ?i \<in> Basis\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. fx x ?t ?i)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t \<in> cbox a b; ?i \<in> Basis\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. fx x ?t ?i)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
assume "x \<in> S"
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have fx2: "continuous_on (cbox a b) (\<lambda>t. fx x t i)" if "i \<in> Basis" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (cbox a b) (\<lambda>t. fx x t i)
[PROOF STEP]
by (rule continuous_Sigma[OF _ continuous_on_Times_swap[OF c1(2)]])
        (auto simp: continuous_intros that \<open>x \<in> S\<close>)
[PROOF STATE]
proof (state)
this:
?i \<in> Basis \<Longrightarrow> continuous_on (cbox a b) (\<lambda>t. fx x t ?i)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?i \<in> Basis \<Longrightarrow> continuous_on (cbox a b) (\<lambda>t. fx x t ?i)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
assume "t \<in> cbox a b"
[PROOF STATE]
proof (state)
this:
t \<in> cbox a b

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have "\<exists>f'. (\<forall>x \<in> S. ((\<lambda>x. f x t) has_derivative blinfun_apply (f' x)) (at x within S) \<and>
      blinfun_apply (f' x) = fx x t) \<and>
      continuous_on S f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f'. (\<forall>x\<in>S. ((\<lambda>x. f x t) has_derivative blinfun_apply (f' x)) (at x within S) \<and> blinfun_apply (f' x) = fx x t) \<and> continuous_on S f'
[PROOF STEP]
by (rule c1_euclidean_blinfunE[OF c1(1)[OF \<open>t \<in> _\<close>] fx1[OF \<open>t \<in> _\<close>]]) (auto, metis)
[PROOF STATE]
proof (state)
this:
\<exists>f'. (\<forall>x\<in>S. ((\<lambda>x. f x t) has_derivative blinfun_apply (f' x)) (at x within S) \<and> blinfun_apply (f' x) = fx x t) \<and> continuous_on S f'

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?t2 \<in> cbox a b \<Longrightarrow> \<exists>f'. (\<forall>x\<in>S. ((\<lambda>x. f x ?t2) has_derivative blinfun_apply (f' x)) (at x within S) \<and> blinfun_apply (f' x) = fx x ?t2) \<and> continuous_on S f'

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t2 \<in> cbox a b \<Longrightarrow> \<exists>f'. (\<forall>x\<in>S. ((\<lambda>x. f x ?t2) has_derivative blinfun_apply (f' x)) (at x within S) \<and> blinfun_apply (f' x) = fx x ?t2) \<and> continuous_on S f'
[PROOF STEP]
obtain fx' where
      fx':
      "\<And>t x. t \<in> cbox a b \<Longrightarrow> x \<in> S \<Longrightarrow> ((\<lambda>x. f x t) has_derivative blinfun_apply (fx' t x)) (at x within S)"
      "\<And>t x. t \<in> cbox a b \<Longrightarrow> x \<in> S \<Longrightarrow> blinfun_apply (fx' t x) = fx x t"
      "\<And>t. t \<in> cbox a b \<Longrightarrow> continuous_on S (fx' t)"
[PROOF STATE]
proof (prove)
using this:
?t2 \<in> cbox a b \<Longrightarrow> \<exists>f'. (\<forall>x\<in>S. ((\<lambda>x. f x ?t2) has_derivative blinfun_apply (f' x)) (at x within S) \<and> blinfun_apply (f' x) = fx x ?t2) \<and> continuous_on S f'

goal (1 subgoal):
 1. (\<And>fx'. \<lbrakk>\<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x t) has_derivative blinfun_apply (fx' t x)) (at x within S); \<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> blinfun_apply (fx' t x) = fx x t; \<And>t. t \<in> cbox a b \<Longrightarrow> continuous_on S (fx' t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t \<in> cbox a b; ?x \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ?t) has_derivative blinfun_apply (fx' ?t ?x)) (at ?x within S)
\<lbrakk>?t \<in> cbox a b; ?x \<in> S\<rbrakk> \<Longrightarrow> blinfun_apply (fx' ?t ?x) = fx ?x ?t
?t \<in> cbox a b \<Longrightarrow> continuous_on S (fx' ?t)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have c: "continuous_on (S \<times> cbox a b) (\<lambda>(x, t). fx' t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (S \<times> cbox a b) (\<lambda>(x, t). fx' t x)
[PROOF STEP]
apply (rule continuous_on_blinfunI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> Basis \<Longrightarrow> continuous_on (S \<times> cbox a b) (\<lambda>x. blinfun_apply (case x of (x, t) \<Rightarrow> fx' t x) i)
[PROOF STEP]
using c1(2)
[PROOF STATE]
proof (prove)
using this:
?i \<in> Basis \<Longrightarrow> continuous_on (S \<times> cbox a b) (\<lambda>(x, t). fx x t ?i)

goal (1 subgoal):
 1. \<And>i. i \<in> Basis \<Longrightarrow> continuous_on (S \<times> cbox a b) (\<lambda>x. blinfun_apply (case x of (x, t) \<Rightarrow> fx' t x) i)
[PROOF STEP]
apply (rule continuous_on_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> Basis \<Longrightarrow> ?i3 i \<in> Basis
 2. \<And>i x. \<lbrakk>i \<in> Basis; x \<in> S \<times> cbox a b\<rbrakk> \<Longrightarrow> (case x of (x, t) \<Rightarrow> fx x t (?i3 i)) = blinfun_apply (case x of (x, t) \<Rightarrow> fx' t x) i
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i x. \<lbrakk>i \<in> Basis; x \<in> S \<times> cbox a b\<rbrakk> \<Longrightarrow> (case x of (x, t) \<Rightarrow> fx x t i) = blinfun_apply (case x of (x, t) \<Rightarrow> fx' t x) i
[PROOF STEP]
by (auto simp: fx' split_beta')
[PROOF STATE]
proof (state)
this:
continuous_on (S \<times> cbox a b) (\<lambda>(x, t). fx' t x)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
from leibniz_rule[of S a b f "\<lambda>x t. fx' t x" x, OF fx'(1) i c \<open>x \<in> S\<close> \<open>convex S\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x t. \<lbrakk>x \<in> S; t \<in> cbox a b\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x t. \<lbrakk>x \<in> S; t \<in> cbox a b\<rbrakk> \<Longrightarrow> x \<in> S; \<And>x. x \<in> S \<Longrightarrow> x \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)
[PROOF STEP]
have "((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x t. \<lbrakk>x \<in> S; t \<in> cbox a b\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x t. \<lbrakk>x \<in> S; t \<in> cbox a b\<rbrakk> \<Longrightarrow> x \<in> S; \<And>x. x \<in> S \<Longrightarrow> x \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)

goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)
[PROOF STEP]
have "((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)

goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x))) (at x within S)

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have fx'xi: "(\<lambda>t. fx' t x) integrable_on cbox a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. fx' t x) integrable_on cbox a b
[PROOF STEP]
apply (rule integrable_continuous)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (cbox a b) (\<lambda>t. fx' t x)
[PROOF STEP]
apply (rule continuous_on_blinfunI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> Basis \<Longrightarrow> continuous_on (cbox a b) (\<lambda>xa. blinfun_apply (fx' xa x) i)
[PROOF STEP]
by (simp add: fx' \<open>x \<in> S\<close> fx2)
[PROOF STATE]
proof (state)
this:
(\<lambda>t. fx' t x) integrable_on cbox a b

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have "blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x)) = (\<lambda>v. integral (cbox a b) (\<lambda>xb. fx x xb v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x)) = (\<lambda>v. integral (cbox a b) (\<lambda>xb. fx x xb v))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x)) v = integral (cbox a b) (\<lambda>xb. fx x xb v)
[PROOF STEP]
apply (subst blinfun_apply_integral)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. (\<lambda>t. fx' t x) integrable_on cbox a b
 2. \<And>v. integral (cbox a b) (\<lambda>y. blinfun_apply (fx' y x) v) = integral (cbox a b) (\<lambda>xb. fx x xb v)
[PROOF STEP]
apply (rule fx'xi)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. integral (cbox a b) (\<lambda>y. blinfun_apply (fx' y x) v) = integral (cbox a b) (\<lambda>xb. fx x xb v)
[PROOF STEP]
by (simp add: \<open>x \<in> S\<close> fx' cong: integral_cong)
[PROOF STATE]
proof (state)
this:
blinfun_apply (integral (cbox a b) (\<lambda>t. fx' t x)) = (\<lambda>v. integral (cbox a b) (\<lambda>xb. fx x xb v))

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. fx x t v))) (at x within S)
 2. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx x xb c))) (at x within S)
[PROOF STEP]
show "((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx x xb c))) (at x within S)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx x xb c))) (at x within S)

goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx x xb c))) (at x within S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx x xb c))) (at x within S)

goal (1 subgoal):
 1. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx ?x2 xb c))) (at ?x2 within S)

goal (1 subgoal):
 1. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx ?x2 xb c))) (at ?x2 within S)
[PROOF STEP]
show "(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>c. integral (cbox a b) (\<lambda>xb. fx ?x2 xb c))) (at ?x2 within S)

goal (1 subgoal):
 1. (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
by (auto simp: differentiable_on_def differentiable_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma leibniz_rule'_higher:
  "higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k"
  if "convex S" "open S"
    and c1: "higher_differentiable_on (S\<times>cbox a b) (\<lambda>(x, t). f x t) k"
    \<comment>\<open>this condition is actually too strong:
      it would suffice if higher partial derivatives (w.r.t. x) are continuous w.r.t. t.
      but it makes the statement short and no need to introduce new constants\<close>
  for S::"'a::euclidean_space set"
    and f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k
[PROOF STEP]
using c1
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, t). f x t) k

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k
[PROOF STEP]
proof (induction k arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) 0 \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) 0
 2. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) 0

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

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) 0
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps intro!: integral_continuous_on_param)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) 0

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> ?f a b) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (?f x)) k
higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (Suc k)

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
define D where "D x = frechet_derivative (\<lambda>(x, y). f x y) (at x)" for x
[PROOF STATE]
proof (state)
this:
D ?x = frechet_derivative (\<lambda>(x, y). f x y) (at ?x)

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
note [continuous_intros] =
    Suc.prems[THEN higher_differentiable_on_imp_continuous_on, THEN continuous_on_compose2,
      of _ "\<lambda>x. (f x, g x)" for f g, unfolded split_beta' fst_conv snd_conv]
[PROOF STATE]
proof (state)
this:
\<lbrakk>continuous_on ?s (\<lambda>x. (?fb4 x, ?g4 x)); (\<lambda>x. (?fb4 x, ?g4 x)) ` ?s \<subseteq> S \<times> cbox a b\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. f (?fb4 x) (?g4 x))

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (Suc k)
[PROOF STEP]
have prems:
    "\<And>xt. xt \<in> S \<times> cbox a b \<Longrightarrow> (\<lambda>(x, y). f x y) differentiable at xt"
    "higher_differentiable_on (S \<times> cbox a b) (\<lambda>x. D x (dx, dt)) k"
    for dx dt
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (Suc k)

goal (1 subgoal):
 1. (\<And>xt. xt \<in> S \<times> cbox a b \<Longrightarrow> (\<lambda>(x, y). f x y) differentiable at xt) &&& higher_differentiable_on (S \<times> cbox a b) (\<lambda>x. D x (dx, dt)) k
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps D_def)
[PROOF STATE]
proof (state)
this:
?xt \<in> S \<times> cbox a b \<Longrightarrow> (\<lambda>(x, y). f x y) differentiable at ?xt
higher_differentiable_on (S \<times> cbox a b) (\<lambda>x. D x (?dx, ?dt)) k

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
from frechet_derivative_worksI[OF this(1), folded D_def]
[PROOF STATE]
proof (chain)
picking this:
?xt1 \<in> S \<times> cbox a b \<Longrightarrow> ((\<lambda>(x, y). f x y) has_derivative D ?xt1) (at ?xt1)
[PROOF STEP]
have D: "x \<in> S \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>(x, y). f x y) has_derivative D (x, t)) (at (x, t))" for x t
[PROOF STATE]
proof (prove)
using this:
?xt1 \<in> S \<times> cbox a b \<Longrightarrow> ((\<lambda>(x, y). f x y) has_derivative D ?xt1) (at ?xt1)

goal (1 subgoal):
 1. \<lbrakk>x \<in> S; t \<in> cbox a b\<rbrakk> \<Longrightarrow> ((\<lambda>(x, y). f x y) has_derivative D (x, t)) (at (x, t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> S; ?t \<in> cbox a b\<rbrakk> \<Longrightarrow> ((\<lambda>(x, y). f x y) has_derivative D (?x, ?t)) (at (?x, ?t))

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
have p1: "((\<lambda>x. (x, t::'b)) has_derivative (\<lambda>h. (h, 0))) (at x within S)" for x t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (x, t)) has_derivative (\<lambda>h. (h, 0::'b))) (at x within S)
[PROOF STEP]
by (auto intro!: derivative_eq_intros)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (x, ?t)) has_derivative (\<lambda>h. (h, 0::'b))) (at ?x within S)

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
have Dx: "x \<in> S \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_derivative (\<lambda>dx. D (x, t) (dx, 0))) (at x within S)" for x t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; t \<in> cbox a b\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x t) has_derivative (\<lambda>dx. D (x, t) (dx, 0::'b))) (at x within S)
[PROOF STEP]
by (drule has_derivative_compose[OF p1 D], assumption) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> S; ?t \<in> cbox a b\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ?t) has_derivative (\<lambda>dx. D (?x, ?t) (dx, 0::'b))) (at ?x within S)

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
have cD: "continuous_on (S \<times> cbox a b) (\<lambda>(x, t). D (x, t) v)" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (S \<times> cbox a b) (\<lambda>(x, t). D (x, t) v)
[PROOF STEP]
apply (rule higher_differentiable_on_imp_continuous_on[where n=k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, t). D (x, t) v) k
[PROOF STEP]
using prems(2)[of "fst v" "snd v"]
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on (S \<times> cbox a b) (\<lambda>x. D x (fst v, snd v)) k

goal (1 subgoal):
 1. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, t). D (x, t) v) k
[PROOF STEP]
by (auto simp: split_beta')
[PROOF STATE]
proof (state)
this:
continuous_on (S \<times> cbox a b) (\<lambda>(x, t). D (x, t) ?v)

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
have fi: "x \<in> S \<Longrightarrow> f x integrable_on cbox a b" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> f x integrable_on cbox a b
[PROOF STEP]
by (rule integrable_continuous) (auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> f ?x integrable_on cbox a b

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
from leibniz_rule'[OF \<open>convex S\<close> Dx cD fi]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> S; \<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x. x \<in> S \<Longrightarrow> x \<in> S; ?x \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))) (at ?x within S)
\<lbrakk>\<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> S; \<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x. x \<in> S \<Longrightarrow> x \<in> S\<rbrakk> \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have ihd: "x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0))))
     (at x within S)"
    and "(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S"
    for x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> S; \<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x. x \<in> S \<Longrightarrow> x \<in> S; ?x \<in> S\<rbrakk> \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))) (at ?x within S)
\<lbrakk>\<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> S; \<And>t x. \<lbrakk>t \<in> cbox a b; x \<in> S\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x. x \<in> S \<Longrightarrow> x \<in> S\<rbrakk> \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S

goal (1 subgoal):
 1. (x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b)))) (at x within S)) &&& (\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))) (at ?x within S)
(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))) (at ?x within S)
(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
[PROOF STEP]
have "x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at x" for x
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))) (at ?x within S)
(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S

goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at x
[PROOF STEP]
using \<open>open S\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))) (at ?x within S)
(\<lambda>x. integral (cbox a b) (f x)) differentiable_on S
open S

goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at x
[PROOF STEP]
by (auto simp: differentiable_on_openD)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at ?x

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at ?x

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
have "higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k
[PROOF STEP]
have *: "frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) =
      (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0)))"
      if "x \<in> S"
      for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) = (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b)))
[PROOF STEP]
apply (rule frechet_derivative_at')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b)))) (at x)
[PROOF STEP]
using ihd(1)[OF that] at_within_open[OF that \<open>open S\<close>]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b)))) (at x within S)
at x within S = at x

goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative (\<lambda>v. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b)))) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at ?x) = (\<lambda>v. integral (cbox a b) (\<lambda>t. D (?x, t) (v, 0::'b)))

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k
[PROOF STEP]
have **: "higher_differentiable_on S (\<lambda>x. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0))) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b))) k
[PROOF STEP]
apply (rule Suc.IH)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> D (a, b) (v, 0::'b)) k
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
?xt \<in> S \<times> cbox a b \<Longrightarrow> (\<lambda>(x, y). f x y) differentiable at ?xt
higher_differentiable_on (S \<times> cbox a b) (\<lambda>x. D x (?dx, ?dt)) k

goal (1 subgoal):
 1. higher_differentiable_on (S \<times> cbox a b) (\<lambda>a. case a of (a, b) \<Rightarrow> D (a, b) (v, 0::'b)) k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. integral (cbox a b) (\<lambda>t. D (x, t) (v, 0::'b))) k

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k
[PROOF STEP]
using \<open>open S\<close>
[PROOF STATE]
proof (prove)
using this:
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k
[PROOF STEP]
by (auto simp: * ** cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) v) k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) ?v) k

goal (1 subgoal):
 1. \<And>k f. \<lbrakk>\<And>f. higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) k; higher_differentiable_on (S \<times> cbox a b) (\<lambda>(x, y). f x y) (Suc k)\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at ?x
higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) ?v) k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> (\<lambda>x. integral (cbox a b) (f x)) differentiable at ?x
higher_differentiable_on S (\<lambda>x. frechet_derivative (\<lambda>x. integral (cbox a b) (f x)) (at x) ?v) k

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. integral (cbox a b) (f x)) (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derivative_is_smooth':
  assumes "(k+1)-smooth_on S f"
  shows "k-smooth_on S (\<lambda>x. frechet_derivative f (at x) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. frechet_derivative f (at x) v)
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
assume "enat n \<le> k"
[PROOF STATE]
proof (state)
this:
enat n \<le> k

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat n \<le> k
[PROOF STEP]
have "Suc n \<le> k + 1"
[PROOF STATE]
proof (prove)
using this:
enat n \<le> k

goal (1 subgoal):
 1. enat (Suc n) \<le> k + 1
[PROOF STEP]
unfolding plus_1_eSuc
[PROOF STATE]
proof (prove)
using this:
enat n \<le> k

goal (1 subgoal):
 1. enat (Suc n) \<le> eSuc k
[PROOF STEP]
by (auto simp: eSuc_def split: enat.splits)
[PROOF STATE]
proof (state)
this:
enat (Suc n) \<le> k + 1

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat (Suc n) \<le> k + 1
[PROOF STEP]
have "higher_differentiable_on S f (Suc n)"
[PROOF STATE]
proof (prove)
using this:
enat (Suc n) \<le> k + 1

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
enat (Suc n) \<le> k + 1
(k + 1)-smooth_on S f

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
by (auto simp: smooth_on_def)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f (Suc n)
[PROOF STEP]
show "higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps(2))
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derivative_is_smooth: "smooth_on S f \<Longrightarrow> smooth_on S (\<lambda>x. frechet_derivative f (at x) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smooth_on S f \<Longrightarrow> smooth_on S (\<lambda>x. frechet_derivative f (at x) v)
[PROOF STEP]
using derivative_is_smooth'[of \<infinity> S f]
[PROOF STATE]
proof (prove)
using this:
(\<infinity> + 1)-smooth_on S f \<Longrightarrow> smooth_on S (\<lambda>x. frechet_derivative f (at x) ?v)

goal (1 subgoal):
 1. smooth_on S f \<Longrightarrow> smooth_on S (\<lambda>x. frechet_derivative f (at x) v)
[PROOF STEP]
by simp


[STATEMENT]
lemma smooth_on_imp_continuous_on: "continuous_on S f" if "k-smooth_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
apply (rule higher_differentiable_on_imp_continuous_on[where n=0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f

goal (1 subgoal):
 1. higher_differentiable_on S f 0
[PROOF STEP]
by (simp add: smooth_on_def enat_0)


[STATEMENT]
lemma smooth_on_imp_differentiable_on[simp]: "f differentiable_on S" if "k-smooth_on S f" "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f differentiable_on S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f
k \<noteq> 0

goal (1 subgoal):
 1. f differentiable_on S
[PROOF STEP]
by (auto simp: smooth_on_def Suc_ile_eq enat_0
      dest!: spec[where x=1]
      intro!: higher_differentiable_on_imp_differentiable_on[where k=1])


[STATEMENT]
lemma smooth_on_cong:
  assumes "k-smooth_on S g" "open S"
    and "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  shows "k-smooth_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S g
open S
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S g n
open S
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. \<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S f n
[PROOF STEP]
by (auto cong: higher_differentiable_on_cong)


[STATEMENT]
lemma smooth_on_open_Un:
  "k-smooth_on S f \<Longrightarrow> k-smooth_on T f \<Longrightarrow> open S \<Longrightarrow> open T \<Longrightarrow> k-smooth_on (S \<union> T) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on T f; open S; open T\<rbrakk> \<Longrightarrow> k-smooth_on (S \<union> T) f
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_open_Un)


[STATEMENT]
lemma smooth_on_open_subsetsI:
  "k-smooth_on S f"
  if "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> k-smooth_on T f

goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> (\<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on T f n)

goal (1 subgoal):
 1. \<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S f n
[PROOF STEP]
by (force intro: higher_differentiable_on_open_subsetsI)


[STATEMENT]
lemma smooth_on_const[intro]: "k-smooth_on S (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. c)
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_const)


[STATEMENT]
lemma smooth_on_id[intro]: "k-smooth_on S (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. x)
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_id)


[STATEMENT]
lemma smooth_on_add_fun: "k-smooth_on S f \<Longrightarrow> k-smooth_on S g \<Longrightarrow> open S \<Longrightarrow> k-smooth_on S (f + g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (f + g)
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_add plus_fun_def)


[STATEMENT]
lemma smooth_on_sum:
  "n-smooth_on S (\<lambda>x. \<Sum>i\<in>F. f i x)"
  if "\<And>i. i \<in> F \<Longrightarrow> finite F \<Longrightarrow> n-smooth_on S (f i)" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n-smooth_on S (\<lambda>x. \<Sum>i\<in>F. f i x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in> F; finite F\<rbrakk> \<Longrightarrow> n-smooth_on S (f ?i)
open S

goal (1 subgoal):
 1. n-smooth_on S (\<lambda>x. \<Sum>i\<in>F. f i x)
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_sum)


[STATEMENT]
lemma (in bounded_bilinear) smooth_on:
  includes no_matrix_mult
  assumes "k-smooth_on S f" "k-smooth_on S g" "open S"
  shows "k-smooth_on S (\<lambda>x. (f x) ** (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. f x ** g x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f
k-smooth_on S g
open S

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. f x ** g x)
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on)


[STATEMENT]
lemma smooth_on_compose2:
  fixes g::"_\<Rightarrow>_::euclidean_space"
  assumes "k-smooth_on T f" "k-smooth_on S g" "open U" "open T" "g ` U \<subseteq> T" "U \<subseteq> S"
  shows "k-smooth_on U (f o g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on U (f \<circ> g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k-smooth_on T f
k-smooth_on S g
open U
open T
g ` U \<subseteq> T
U \<subseteq> S

goal (1 subgoal):
 1. k-smooth_on U (f \<circ> g)
[PROOF STEP]
by (auto simp: smooth_on_def intro!: higher_differentiable_on_compose intro: higher_differentiable_on_subset)


[STATEMENT]
lemma smooth_on_compose:
  fixes g::"_\<Rightarrow>_::euclidean_space"
  assumes "k-smooth_on T f" "k-smooth_on S g" "open S" "open T" "g ` S \<subseteq> T"
  shows "k-smooth_on S (f o g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (f \<circ> g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k-smooth_on T f
k-smooth_on S g
open S
open T
g ` S \<subseteq> T

goal (1 subgoal):
 1. k-smooth_on S (f \<circ> g)
[PROOF STEP]
by (rule smooth_on_compose2) auto


[STATEMENT]
lemma smooth_on_subset:
  "k-smooth_on S f"
  if "k-smooth_on T f" "S \<subseteq> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
using higher_differentiable_on_subset[of T f _ S] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on T f ?n; S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S f ?n
k-smooth_on T f
S \<subseteq> T

goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
by (auto simp: smooth_on_def)


[STATEMENT]
lemma smooth_on_divide:"k-smooth_on S f \<Longrightarrow> k-smooth_on S g \<Longrightarrow> open S \<Longrightarrow>(\<And>x. x \<in> S \<Longrightarrow> g x \<noteq> 0) \<Longrightarrow>
  k-smooth_on S (\<lambda>x. f x / g x)"
  for f::"_\<Rightarrow>_::real_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S; \<And>x. x \<in> S \<Longrightarrow> g x \<noteq> (0::'d)\<rbrakk> \<Longrightarrow> k-smooth_on S (\<lambda>x. f x / g x)
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_divide)


[STATEMENT]
lemma smooth_on_scaleR_fun: "k-smooth_on S g \<Longrightarrow> open S \<Longrightarrow> k-smooth_on S (c *\<^sub>R g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (c *\<^sub>R g)
[PROOF STEP]
by (auto simp: scaleR_fun_def intro!: smooth_on_scaleR )


[STATEMENT]
lemma smooth_on_uminus_fun: "k-smooth_on S g \<Longrightarrow> open S \<Longrightarrow> k-smooth_on S (- g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (- g)
[PROOF STEP]
using smooth_on_scaleR_fun[where c="-1", of k S g]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (- 1 *\<^sub>R g)

goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (- g)
[PROOF STEP]
by auto


[STATEMENT]
lemma smooth_on_minus_fun: "k-smooth_on S f \<Longrightarrow> k-smooth_on S g \<Longrightarrow> open S \<Longrightarrow> k-smooth_on S (f - g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (f - g)
[PROOF STEP]
unfolding diff_conv_add_uminus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (f + - g)
[PROOF STEP]
apply (rule smooth_on_add_fun)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S f
 2. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (- g)
 3. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> open S
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (- g)
 2. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> open S
[PROOF STEP]
apply (rule smooth_on_uminus_fun)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S g
 2. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> open S
 3. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> open S
[PROOF STEP]
by auto


[STATEMENT]
lemma smooth_on_times_fun: "k-smooth_on S f \<Longrightarrow> k-smooth_on S g \<Longrightarrow> open S \<Longrightarrow> k-smooth_on S (f * g)"
  for f g::"_ \<Rightarrow>_::real_normed_algebra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k-smooth_on S f; k-smooth_on S g; open S\<rbrakk> \<Longrightarrow> k-smooth_on S (f * g)
[PROOF STEP]
by (auto simp: times_fun_def intro!: smooth_on_mult)


[STATEMENT]
lemma smooth_on_le:
  "l-smooth_on S f"
  if "k-smooth_on S f" "l \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l-smooth_on S f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f
l \<le> k

goal (1 subgoal):
 1. l-smooth_on S f
[PROOF STEP]
by (auto simp: smooth_on_def)


[STATEMENT]
lemma smooth_on_inverse: "k-smooth_on S (\<lambda>x. inverse (f x))"
  if "k-smooth_on S f" "0 \<notin> f ` S" "open S"
  for f::"_ \<Rightarrow>_::real_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. inverse (f x))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. inverse (f x))
[PROOF STEP]
by (auto simp: smooth_on_def intro!: higher_differentiable_on_inverse)


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

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. norm (f x))
[PROOF STEP]
by (auto simp: smooth_on_def intro!: higher_differentiable_on_norm)


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

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. sqrt (f x))
[PROOF STEP]
by (auto simp: smooth_on_def intro!: higher_differentiable_on_sqrt)


[STATEMENT]
lemma smooth_on_frechet_derivative:
  "\<infinity>-smooth_on UNIV (\<lambda>x. frechet_derivative f (at x) v)"
  if "\<infinity>-smooth_on UNIV f"
    \<comment>\<open>TODO: generalize\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smooth_on UNIV (\<lambda>x. frechet_derivative f (at x) v)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
smooth_on UNIV f

goal (1 subgoal):
 1. smooth_on UNIV (\<lambda>x. frechet_derivative f (at x) v)
[PROOF STEP]
apply (auto simp: smooth_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n. higher_differentiable_on UNIV f n \<Longrightarrow> higher_differentiable_on UNIV (\<lambda>x. frechet_derivative f (at x) v) n
[PROOF STEP]
apply (rule higher_differentiable_on_frechet_derivativeI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<forall>n. higher_differentiable_on UNIV f n \<Longrightarrow> higher_differentiable_on UNIV f (Suc n)
 2. \<And>n. \<forall>n. higher_differentiable_on UNIV f n \<Longrightarrow> open UNIV
 3. \<And>n. \<forall>n. higher_differentiable_on UNIV f n \<Longrightarrow> ?x4 n \<in> UNIV
[PROOF STEP]
by auto


[STATEMENT]
lemma smooth_onD: "higher_differentiable_on S f n" if "m-smooth_on S f" "enat n \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
m-smooth_on S f
enat n \<le> m

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (auto simp: smooth_on_def)


[STATEMENT]
lemma (in bounded_linear) higher_differentiable_on: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on S f 0
 2. \<And>n. higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. higher_differentiable_on S f 0
 2. \<And>n. higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f 0
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps linear_continuous_on bounded_linear_axioms)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0

goal (1 subgoal):
 1. \<And>n. higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. \<And>n. higher_differentiable_on S f n \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
apply (auto simp: higher_differentiable_on.simps frechet_derivative higher_differentiable_on_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>higher_differentiable_on S f n; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable at x
[PROOF STEP]
using bounded_linear_axioms
[PROOF STATE]
proof (prove)
using this:
bounded_linear f

goal (1 subgoal):
 1. \<And>x. \<lbrakk>higher_differentiable_on S f n; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable at x
[PROOF STEP]
apply (rule bounded_linear_imp_differentiable)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in bounded_linear) smooth_on: "k-smooth_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S f
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on)


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

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. snd (f x))
[PROOF STEP]
by (auto simp: smooth_on_def)


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

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. fst (f x))
[PROOF STEP]
by (auto simp: smooth_on_def)


[STATEMENT]
lemma smooth_on_sin: "n-smooth_on S (\<lambda>x. sin (f x::real))" if "n-smooth_on S f" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n-smooth_on S (\<lambda>x. sin (f x))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n-smooth_on S f
open S

goal (1 subgoal):
 1. n-smooth_on S (\<lambda>x. sin (f x))
[PROOF STEP]
by (auto simp: smooth_on_def intro!: higher_differentiable_on_sin)


[STATEMENT]
lemma smooth_on_cos: "n-smooth_on S (\<lambda>x. cos (f x::real))" if "n-smooth_on S f" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n-smooth_on S (\<lambda>x. cos (f x))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n-smooth_on S f
open S

goal (1 subgoal):
 1. n-smooth_on S (\<lambda>x. cos (f x))
[PROOF STEP]
by (auto simp: smooth_on_def intro!: higher_differentiable_on_cos)