:: by Hiroyuki Okazaki , Noboru Endou , Keiko Narita and Yasunari Shidama

::

:: Received October 13, 2010

:: Copyright (c) 2010-2019 Association of Mizar Users

set cs = seq_const 0;

theorem Th1: :: NDIFF_3:1

for G being RealNormSpace

for s1 being Real_Sequence

for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds

( seq is convergent & lim seq = 0. G )

for s1 being Real_Sequence

for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds

( seq is convergent & lim seq = 0. G )

proof end;

theorem Th2: :: NDIFF_3:2

for G being RealNormSpace

for k being Element of NAT

for s1 being Real_Sequence

for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k

for k being Element of NAT

for s1 being Real_Sequence

for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k

proof end;

definition

let F be RealNormSpace;

let IT be PartFunc of REAL, the carrier of F;

end;
let IT be PartFunc of REAL, the carrier of F;

attr IT is RestFunc-like means :Def1: :: NDIFF_3:def 1

( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) );

( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) );

:: deftheorem Def1 defines RestFunc-like NDIFF_3:def 1 :

for F being RealNormSpace

for IT being PartFunc of REAL, the carrier of F holds

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) ) );

for F being RealNormSpace

for IT being PartFunc of REAL, the carrier of F holds

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) ) );

registration

let F be RealNormSpace;

ex b_{1} being PartFunc of REAL, the carrier of F st b_{1} is RestFunc-like

end;
cluster V1() V4( REAL ) V5( the carrier of F) Function-like RestFunc-like for Element of K16(K17(REAL, the carrier of F));

existence ex b

proof end;

definition
end;

:: deftheorem Def2 defines linear NDIFF_3:def 2 :

for F being RealNormSpace

for IT being Function of REAL, the carrier of F holds

( IT is linear iff ex r being Point of F st

for p being Real holds IT /. p = p * r );

for F being RealNormSpace

for IT being Function of REAL, the carrier of F holds

( IT is linear iff ex r being Point of F st

for p being Real holds IT /. p = p * r );

registration

let F be RealNormSpace;

ex b_{1} being Function of REAL, the carrier of F st b_{1} is linear

end;
cluster V1() V4( REAL ) V5( the carrier of F) V6() Function-like total quasi_total linear for Element of K16(K17(REAL, the carrier of F));

existence ex b

proof end;

definition
end;

theorem Th3: :: NDIFF_3:3

for F being RealNormSpace

for L1, L2 being LinearFunc of F holds

( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )

for L1, L2 being LinearFunc of F holds

( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )

proof end;

theorem Th4: :: NDIFF_3:4

for F being RealNormSpace

for r being Real

for L being LinearFunc of F holds r (#) L is LinearFunc of F

for r being Real

for L being LinearFunc of F holds r (#) L is LinearFunc of F

proof end;

theorem Th5: :: NDIFF_3:5

for F being RealNormSpace

for h1, h2 being PartFunc of REAL, the carrier of F

for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

for h1, h2 being PartFunc of REAL, the carrier of F

for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

proof end;

theorem Th6: :: NDIFF_3:6

for F being RealNormSpace

for h1, h2 being PartFunc of REAL, the carrier of F

for seq being Real_Sequence st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

for h1, h2 being PartFunc of REAL, the carrier of F

for seq being Real_Sequence st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

proof end;

theorem Th7: :: NDIFF_3:7

for F being RealNormSpace

for R1, R2 being RestFunc of F holds

( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )

for R1, R2 being RestFunc of F holds

( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )

proof end;

definition

let F be RealNormSpace;

let f be PartFunc of REAL, the carrier of F;

let x0 be Real;

end;
let f be PartFunc of REAL, the carrier of F;

let x0 be Real;

pred f is_differentiable_in x0 means :: NDIFF_3:def 3

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) );

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) );

:: deftheorem defines is_differentiable_in NDIFF_3:def 3 :

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for x0 being Real holds

( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) );

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for x0 being Real holds

( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) );

definition

let F be RealNormSpace;

let f be PartFunc of REAL, the carrier of F;

let x0 be Real;

assume A1: f is_differentiable_in x0 ;

ex b_{1} being Point of F ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b_{1} = L /. 1 & ( for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) )

for b_{1}, b_{2} being Point of F st ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b_{1} = L /. 1 & ( for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b_{2} = L /. 1 & ( for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of REAL, the carrier of F;

let x0 be Real;

assume A1: f is_differentiable_in x0 ;

func diff (f,x0) -> Point of F means :Def4: :: NDIFF_3:def 4

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( it = L /. 1 & ( for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) );

existence ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( it = L /. 1 & ( for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) );

ex b

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) )

proof end;

uniqueness for b

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines diff NDIFF_3:def 4 :

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for x0 being Real st f is_differentiable_in x0 holds

for b_{4} being Point of F holds

( b_{4} = diff (f,x0) iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b_{4} = L /. 1 & ( for x being Real st x in N holds

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) );

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for x0 being Real st f is_differentiable_in x0 holds

for b

( b

( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st

( b

(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) );

definition

let F be RealNormSpace;

let f be PartFunc of REAL, the carrier of F;

let X be set ;

end;
let f be PartFunc of REAL, the carrier of F;

let X be set ;

pred f is_differentiable_on X means :: NDIFF_3:def 5

( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) );

( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) );

:: deftheorem defines is_differentiable_on NDIFF_3:def 5 :

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for X being set holds

( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) ) );

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for X being set holds

( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) ) );

theorem Th9: :: NDIFF_3:9

for F being RealNormSpace

for X being set

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds

X is Subset of REAL by XBOOLE_1:1;

for X being set

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds

X is Subset of REAL by XBOOLE_1:1;

theorem Th10: :: NDIFF_3:10

for F being RealNormSpace

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds

f is_differentiable_in x ) ) )

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds

f is_differentiable_in x ) ) )

proof end;

theorem :: NDIFF_3:11

for F being RealNormSpace

for Y being Subset of REAL

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds

Y is open

for Y being Subset of REAL

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds

Y is open

proof end;

definition

let F be RealNormSpace;

let f be PartFunc of REAL, the carrier of F;

let X be set ;

assume A1: f is_differentiable_on X ;

ex b_{1} being PartFunc of REAL, the carrier of F st

( dom b_{1} = X & ( for x being Real st x in X holds

b_{1} . x = diff (f,x) ) )

for b_{1}, b_{2} being PartFunc of REAL, the carrier of F st dom b_{1} = X & ( for x being Real st x in X holds

b_{1} . x = diff (f,x) ) & dom b_{2} = X & ( for x being Real st x in X holds

b_{2} . x = diff (f,x) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of REAL, the carrier of F;

let X be set ;

assume A1: f is_differentiable_on X ;

func f `| X -> PartFunc of REAL, the carrier of F means :Def6: :: NDIFF_3:def 6

( dom it = X & ( for x being Real st x in X holds

it . x = diff (f,x) ) );

existence ( dom it = X & ( for x being Real st x in X holds

it . x = diff (f,x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines `| NDIFF_3:def 6 :

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for X being set st f is_differentiable_on X holds

for b_{4} being PartFunc of REAL, the carrier of F holds

( b_{4} = f `| X iff ( dom b_{4} = X & ( for x being Real st x in X holds

b_{4} . x = diff (f,x) ) ) );

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for X being set st f is_differentiable_on X holds

for b

( b

b

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem :: NDIFF_3:12

for F being RealNormSpace

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0. F ) )

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0. F ) )

proof end;

theorem Th13: :: NDIFF_3:13

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for x0 being Real

for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

for f being PartFunc of REAL, the carrier of F

for x0 being Real

for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

proof end;

theorem Th14: :: NDIFF_3:14

for F being RealNormSpace

for x0 being Real

for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

for x0 being Real

for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

proof end;

theorem Th15: :: NDIFF_3:15

for F being RealNormSpace

for x0 being Real

for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )

for x0 being Real

for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )

proof end;

theorem Th16: :: NDIFF_3:16

for F being RealNormSpace

for x0 being Real

for f being PartFunc of REAL, the carrier of F

for r being Real st f is_differentiable_in x0 holds

( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )

for x0 being Real

for f being PartFunc of REAL, the carrier of F

for r being Real st f is_differentiable_in x0 holds

( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )

proof end;

theorem :: NDIFF_3:17

for F being RealNormSpace

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )

proof end;

theorem :: NDIFF_3:18

for F being RealNormSpace

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )

proof end;

theorem :: NDIFF_3:19

for F being RealNormSpace

for r being Real

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds

((r (#) f) `| Z) . x = r * (diff (f,x)) ) )

for r being Real

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds

((r (#) f) `| Z) . x = r * (diff (f,x)) ) )

proof end;

theorem :: NDIFF_3:20

for F being RealNormSpace

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom f & f | Z is constant holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = 0. F ) )

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom f & f | Z is constant holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = 0. F ) )

proof end;

theorem Th21: :: NDIFF_3:21

for F being RealNormSpace

for r, p being Point of F

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds

f /. x = (x * r) + p ) holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = r ) )

for r, p being Point of F

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds

f /. x = (x * r) + p ) holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = r ) )

proof end;

theorem Th22: :: NDIFF_3:22

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F

for x0 being Real st f is_differentiable_in x0 holds

f is_continuous_in x0

for f being PartFunc of REAL, the carrier of F

for x0 being Real st f is_differentiable_in x0 holds

f is_continuous_in x0

proof end;

theorem :: NDIFF_3:23

for F being RealNormSpace

for X being set

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds

f | X is continuous

for X being set

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds

f | X is continuous

proof end;

theorem Th24: :: NDIFF_3:24

for F being RealNormSpace

for X being set

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

for X being set

for Z being open Subset of REAL

for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

proof end;

Lm1: {} REAL is closed

;

:: deftheorem Def7 defines differentiable NDIFF_3:def 7 :

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F holds

( f is differentiable iff f is_differentiable_on dom f );

for F being RealNormSpace

for f being PartFunc of REAL, the carrier of F holds

( f is differentiable iff f is_differentiable_on dom f );

Lm2: [#] REAL is open

by XBOOLE_1:37, Lm1;

registration

let F be RealNormSpace;

ex b_{1} being Function of REAL, the carrier of F st b_{1} is differentiable

end;
cluster V1() V4( REAL ) V5( the carrier of F) V6() Function-like total quasi_total differentiable for Element of K16(K17(REAL, the carrier of F));

existence ex b

proof end;

theorem :: NDIFF_3:26

for F being RealNormSpace

for Z being open Subset of REAL

for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds

f is_differentiable_on Z by Def7, Th24;

for Z being open Subset of REAL

for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds

f is_differentiable_on Z by Def7, Th24;