:: 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 b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = T & ( for i being Nat holds b₁ . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b₁ . i))) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = T & ( for i being Nat holds b₁ . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b₁ . i))) ) & dom b₂ = NAT & b₂ . 0 = T & ( for i being Nat holds b₂ . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b₂ . i))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines diff_SP NDIFF_6:def 2 :
for S, T being RealNormSpace
for b₃ being Function holds
( b₃ = diff_SP (S,T) iff ( dom b₃ = NAT & b₃ . 0 = T & ( for i being Nat holds b₃ . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b₃ . 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 b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = f | Z & ( for i being Nat holds b₁ . (i + 1) = (modetrans ((b₁ . i),S,(diff_SP (i,S,T)))) `| Z ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = f | Z & ( for i being Nat holds b₁ . (i + 1) = (modetrans ((b₁ . i),S,(diff_SP (i,S,T)))) `| Z ) & dom b<sub>2</sub> = NAT & b<sub>2</sub> . 0 = f | Z & ( for i being Nat holds b<sub>2</sub> . (i + 1) = (modetrans ((b<sub>2</sub> . i),S,(diff_SP (i,S,T)))) `| Z ) holds
b₁ = b₂

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 b₅ being Function holds
( b₅ = diff (f,Z) iff ( dom b₅ = NAT & b₅ . 0 = f | Z & ( for i being Nat holds b₅ . (i + 1) = (modetrans ((b₅ . 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;