:: by Noboru Endou and Yasunari Shidama

::

:: Received May 19, 2013

:: Copyright (c) 2013-2016 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 ) )

( 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 ) )

( 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 ) )

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*>] ) )

( 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*> ) )

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 ) )

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
end;

:: deftheorem Def1 defines modetrans NDIFF_6:def 1 :

for S being set st S is RealNormSpace holds

modetrans S = S;

for S being set st S is RealNormSpace holds

modetrans S = S;

definition

let S, T be RealNormSpace;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = T & ( for i being Nat holds b_{1} . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b_{1} . i))) ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = T & ( for i being Nat holds b_{1} . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b_{1} . i))) ) & dom b_{2} = NAT & b_{2} . 0 = T & ( for i being Nat holds b_{2} . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b_{2} . i))) ) holds

b_{1} = b_{2}

end;
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 ( dom it = NAT & it . 0 = T & ( for i being Nat holds it . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (it . i))) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines diff_SP NDIFF_6:def 2 :

for S, T being RealNormSpace

for b_{3} being Function holds

( b_{3} = diff_SP (S,T) iff ( dom b_{3} = NAT & b_{3} . 0 = T & ( for i being Nat holds b_{3} . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b_{3} . i))) ) ) );

for S, T being RealNormSpace

for b

( b

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))) )

( (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 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) )

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;

correctness

coherence

(diff_SP (S,T)) . i is RealNormSpace;

end;
let i be Nat;

correctness

coherence

(diff_SP (S,T)) . i is RealNormSpace;

proof 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;

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)))

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 ;

correctness

coherence

f is PartFunc of S,T;

by A1;

end;
let f be set ;

assume A1: f is PartFunc of S,T ;

correctness

coherence

f is PartFunc of S,T;

by A1;

:: 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;

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;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = f | Z & ( for i being Nat holds b_{1} . (i + 1) = (modetrans ((b_{1} . i),S,(diff_SP (i,S,T)))) `| Z ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = f | Z & ( for i being Nat holds b_{1} . (i + 1) = (modetrans ((b_{1} . i),S,(diff_SP (i,S,T)))) `| Z ) & dom b_{2} = NAT & b_{2} . 0 = f | Z & ( for i being Nat holds b_{2} . (i + 1) = (modetrans ((b_{2} . i),S,(diff_SP (i,S,T)))) `| Z ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof 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_{5} being Function holds

( b_{5} = diff (f,Z) iff ( dom b_{5} = NAT & b_{5} . 0 = f | Z & ( for i being Nat holds b_{5} . (i + 1) = (modetrans ((b_{5} . i),S,(diff_SP (i,S,T)))) `| Z ) ) );

for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S

for b

( b

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 )

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))

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;

correctness

coherence

(diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T));

by Th12;

end;
let f be PartFunc of S,T;

let Z be Subset of S;

let i be Nat;

correctness

coherence

(diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T));

by Th12;

:: 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;

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

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;

end;
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 ) );

( 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 ) );

:: 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 ) ) );

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 ) ) )

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 ) )

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 ) )

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

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

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 )

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))

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

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))

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

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))

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

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))

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

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;