:: Differentiation in Normed Spaces
:: by Noboru Endou and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


theorem :: NDIFF_6:1
for D, E, F being non empty set ex I being Function of (Funcs (D,(Funcs (E,F)))),(Funcs ([:D,E:],F)) st
( I is bijective & ( for f being Function of D,(Funcs (E,F))
for d, e being object st d in D & e in E holds
(I . f) . (d,e) = (f . d) . e ) )
proof end;

theorem Th2: :: NDIFF_6:2
for D, E, F being non empty set ex I being Function of (Funcs (D,(Funcs (E,F)))),(Funcs ([:E,D:],F)) st
( I is bijective & ( for f being Function of D,(Funcs (E,F))
for e, d being object st e in E & d in D holds
(I . f) . (e,d) = (f . d) . e ) )
proof end;

theorem :: NDIFF_6:3
for D, E being non-empty non empty FinSequence
for F being non empty set ex L being Function of (Funcs ((product D),(Funcs ((product E),F)))),(Funcs ((product (E ^ D)),F)) st
( L is bijective & ( for f being Function of (product D),(Funcs ((product E),F))
for e, d being FinSequence st e in product E & d in product D holds
(L . f) . (e ^ d) = (f . d) . e ) )
proof end;

theorem Th4: :: NDIFF_6:4
for X, Y being non empty set ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is bijective & ( for x, y being object st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) )
proof end;

theorem Th5: :: NDIFF_6:5
for X being non-empty non empty FinSequence
for Y being non empty set ex K being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( K is bijective & ( for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*> ) )
proof end;

theorem :: NDIFF_6:6
for D being non empty set
for E being non-empty non empty FinSequence
for F being non empty set ex L being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ((product (E ^ <*D*>)),F)) st
( L is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e ) )
proof end;

definition
let S be set ;
assume A1: S is RealNormSpace ;
func modetrans S -> RealNormSpace equals :Def1: :: NDIFF_6:def 1
S;
correctness
coherence
S is RealNormSpace
;
by A1;
end;

:: deftheorem Def1 defines modetrans NDIFF_6:def 1 :
for S being set st S is RealNormSpace holds
modetrans S = S;

definition
let S, T be RealNormSpace;
func diff_SP (S,T) -> Function means :Def2: :: NDIFF_6:def 2
( dom it = NAT & it . 0 = T & ( for i being Nat holds it . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (it . i))) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = T & ( for i being Nat holds b1 . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b1 . i))) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = T & ( for i being Nat holds b1 . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b1 . i))) ) & dom b2 = NAT & b2 . 0 = T & ( for i being Nat holds b2 . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b2 . i))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines diff_SP NDIFF_6:def 2 :
for S, T being RealNormSpace
for b3 being Function holds
( b3 = diff_SP (S,T) iff ( dom b3 = NAT & b3 . 0 = T & ( for i being Nat holds b3 . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b3 . i))) ) ) );

theorem Th7: :: NDIFF_6:7
for S, T being RealNormSpace holds
( (diff_SP (S,T)) . 0 = T & (diff_SP (S,T)) . 1 = R_NormSpace_of_BoundedLinearOperators (S,T) & (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,T))) )
proof end;

theorem Th8: :: NDIFF_6:8
for S, T being RealNormSpace
for i being Nat holds (diff_SP (S,T)) . i is RealNormSpace
proof end;

theorem Th9: :: NDIFF_6:9
for S, T being RealNormSpace
for i being Nat ex H being RealNormSpace st
( H = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) )
proof end;

definition
let S, T be RealNormSpace;
let i be Nat;
func diff_SP (i,S,T) -> RealNormSpace equals :: NDIFF_6:def 3
(diff_SP (S,T)) . i;
correctness
coherence
(diff_SP (S,T)) . i is RealNormSpace
;
proof end;
end;

:: deftheorem defines diff_SP NDIFF_6:def 3 :
for S, T being RealNormSpace
for i being Nat holds diff_SP (i,S,T) = (diff_SP (S,T)) . i;

theorem Th10: :: NDIFF_6:10
for S, T being RealNormSpace
for i being Nat holds diff_SP ((i + 1),S,T) = R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,T)))
proof end;

definition
let S, T be RealNormSpace;
let f be set ;
assume A1: f is PartFunc of S,T ;
func modetrans (f,S,T) -> PartFunc of S,T equals :Def4: :: NDIFF_6:def 4
f;
correctness
coherence
f is PartFunc of S,T
;
by A1;
end;

:: deftheorem Def4 defines modetrans NDIFF_6:def 4 :
for S, T being RealNormSpace
for f being set st f is PartFunc of S,T holds
modetrans (f,S,T) = f;

definition
let S, T be RealNormSpace;
let f be PartFunc of S,T;
let Z be Subset of S;
func diff (f,Z) -> Function means :Def5: :: NDIFF_6:def 5
( dom it = NAT & it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (modetrans ((it . i),S,(diff_SP (i,S,T)))) `| Z ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (modetrans ((b1 . i),S,(diff_SP (i,S,T)))) `| Z ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (modetrans ((b1 . i),S,(diff_SP (i,S,T)))) `| Z ) & dom b2 = NAT & b2 . 0 = f | Z & ( for i being Nat holds b2 . (i + 1) = (modetrans ((b2 . i),S,(diff_SP (i,S,T)))) `| Z ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines diff NDIFF_6:def 5 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for b5 being Function holds
( b5 = diff (f,Z) iff ( dom b5 = NAT & b5 . 0 = f | Z & ( for i being Nat holds b5 . (i + 1) = (modetrans ((b5 . i),S,(diff_SP (i,S,T)))) `| Z ) ) );

theorem Th11: :: NDIFF_6:11
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( (diff (f,Z)) . 0 = f | Z & (diff (f,Z)) . 1 = (f | Z) `| Z & (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z )
proof end;

theorem Th12: :: NDIFF_6:12
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for i being Nat holds (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T))
proof end;

definition
let S, T be RealNormSpace;
let f be PartFunc of S,T;
let Z be Subset of S;
let i be Nat;
func diff (f,i,Z) -> PartFunc of S,(diff_SP (i,S,T)) equals :: NDIFF_6:def 6
(diff (f,Z)) . i;
correctness
coherence
(diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T))
;
by Th12;
end;

:: deftheorem defines diff NDIFF_6:def 6 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for i being Nat holds diff (f,i,Z) = (diff (f,Z)) . i;

theorem Th13: :: NDIFF_6:13
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for i being Nat holds diff (f,(i + 1),Z) = (diff (f,i,Z)) `| Z
proof end;

definition
let S, T be RealNormSpace;
let f be PartFunc of S,T;
let Z be Subset of S;
let n be Nat;
pred f is_differentiable_on n,Z means :: NDIFF_6:def 7
( Z c= dom f & ( for i being Nat st i <= n - 1 holds
modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z ) );
end;

:: deftheorem defines is_differentiable_on NDIFF_6:def 7 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for n being Nat holds
( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z ) ) );

theorem Th14: :: NDIFF_6:14
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for n being Nat holds
( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) ) )
proof end;

theorem Th15: :: NDIFF_6:15
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( f is_differentiable_on 1,Z iff ( Z c= dom f & f | Z is_differentiable_on Z ) )
proof end;

theorem :: NDIFF_6:16
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( f is_differentiable_on 2,Z iff ( Z c= dom f & f | Z is_differentiable_on Z & (f | Z) `| Z is_differentiable_on Z ) )
proof end;

theorem Th17: :: NDIFF_6:17
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
proof end;

theorem Th18: :: NDIFF_6:18
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
Z is open
proof end;

theorem Th19: :: NDIFF_6:19
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
( (diff_SP (S,T)) . i is RealNormSpace & (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) & dom (diff (f,i,Z)) = Z )
proof end;

theorem Th20: :: NDIFF_6:20
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z))
proof end;

theorem :: NDIFF_6:21
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
f + g is_differentiable_on n,Z
proof end;

theorem Th22: :: NDIFF_6:22
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((f - g),i,Z) = (diff (f,i,Z)) - (diff (g,i,Z))
proof end;

theorem :: NDIFF_6:23
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
f - g is_differentiable_on n,Z
proof end;

theorem Th24: :: NDIFF_6:24
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for r being Real
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
proof end;

theorem Th25: :: NDIFF_6:25
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for r being Real
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z
proof end;

theorem :: NDIFF_6:26
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z))
proof end;

theorem :: NDIFF_6:27
for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
- f is_differentiable_on n,Z
proof end;