FDIFF_1: Real Function Differentiability

:: Real Function Differentiability
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem Th1: :: FDIFF_1:1

for Y being Subset of REAL holds
( ( for r being Real holds
( r in Y iff r in REAL ) ) iff Y = REAL )

proof end;

definition

let IT be Real_Sequence;
attr IT is convergent_to_0 means :Def1: :: FDIFF_1:def 1
( IT is non-zero & IT is convergent & lim IT = 0 );

end;

:: deftheorem Def1 defines convergent_to_0 FDIFF_1:def 1 :

registration

cluster V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent_to_0 Element of K21(K22(NAT,REAL));
existence

proof end;

end;

reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:57;

definition

let IT be PartFunc of REAL,REAL;
canceled;
attr IT is REST-like means :Def3: :: FDIFF_1:def 3
( IT is total & ( for h being convergent_to_0 Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) );

end;

:: deftheorem FDIFF_1:def 2 :

:: deftheorem Def3 defines REST-like FDIFF_1:def 3 :

reconsider cf = REAL --> 0 as Function of REAL,REAL by FUNCOP_1:57;

registration

cluster V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued REST-like Element of K21(K22(REAL,REAL));
existence

proof end;

end;

definition

mode REST is REST-like PartFunc of REAL,REAL;

end;

definition

let IT be PartFunc of REAL,REAL;
attr IT is linear means :Def4: :: FDIFF_1:def 4
( IT is total & ex r being Real st
for p being Real holds IT . p = r * p );

end;

:: deftheorem Def4 defines linear FDIFF_1:def 4 :

registration

cluster V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued linear Element of K21(K22(REAL,REAL));
existence

proof end;

end;

definition

mode LINEAR is linear PartFunc of REAL,REAL;

end;

theorem :: FDIFF_1:2

canceled;

theorem :: FDIFF_1:3

canceled;

theorem :: FDIFF_1:4

canceled;

theorem :: FDIFF_1:5

canceled;

theorem Th6: :: FDIFF_1:6

for L1, L2 being LINEAR holds
( L1 + L2 is LINEAR & L1 - L2 is LINEAR )

proof end;

theorem Th7: :: FDIFF_1:7

for r being Real
for L being LINEAR holds r (#) L is LINEAR

proof end;

theorem Th8: :: FDIFF_1:8

for R1, R2 being REST holds
( R1 + R2 is REST & R1 - R2 is REST & R1 (#) R2 is REST )

proof end;

theorem Th9: :: FDIFF_1:9

for r being Real
for R being REST holds r (#) R is REST

proof end;

theorem Th10: :: FDIFF_1:10

for L1, L2 being LINEAR holds L1 (#) L2 is REST-like

proof end;

theorem Th11: :: FDIFF_1:11

for R being REST
for L being LINEAR holds
( R (#) L is REST & L (#) R is REST )

proof end;

definition

let f be PartFunc of REAL,REAL;
let x0 be real number ;
pred f is_differentiable_in x0 means :Def5: :: FDIFF_1:def 5
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) );

end;

:: deftheorem Def5 defines is_differentiable_in FDIFF_1:def 5 :

definition

let f be PartFunc of REAL,REAL;
let x0 be real number ;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) -> Real means :Def6: :: FDIFF_1:def 6
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( it = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines diff FDIFF_1:def 6 :

definition

let f be PartFunc of REAL,REAL;
let X be set ;
pred f is_differentiable_on X means :Def7: :: FDIFF_1:def 7
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) );

end;

:: deftheorem Def7 defines is_differentiable_on FDIFF_1:def 7 :

theorem :: FDIFF_1:12

canceled;

theorem :: FDIFF_1:13

canceled;

theorem :: FDIFF_1:14

canceled;

theorem Th15: :: FDIFF_1:15

for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
X is Subset of REAL

proof end;

theorem Th16: :: FDIFF_1:16

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL 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 :: FDIFF_1:17

for Y being Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Y holds
Y is open

proof end;

definition

let f be PartFunc of REAL,REAL;
let X be set ;
assume A1: f is_differentiable_on X ;
func f `| X -> PartFunc of REAL,REAL means :Def8: :: FDIFF_1:def 8
( dom it = X & ( for x being Real st x in X holds
it . x = diff (f,x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines `| FDIFF_1:def 8 :

theorem :: FDIFF_1:18

canceled;

theorem :: FDIFF_1:19

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ex r being Real st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )

proof end;

registration

let h be convergent_to_0 Real_Sequence;
let n be Element of NAT ;
cluster h ^\ n -> convergent_to_0 ;
coherence

proof end;

end;

theorem Th20: :: FDIFF_1:20

for f being PartFunc of REAL,REAL
for x0 being real number
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 Real_Sequence
for c being V8() 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 Th21: :: FDIFF_1:21

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL 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 Th22: :: FDIFF_1:22

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL 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 Th23: :: FDIFF_1:23

for x0, r being Real
for f being PartFunc of REAL,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 Th24: :: FDIFF_1:24

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )

proof end;

theorem Th25: :: FDIFF_1:25

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )

proof end;

theorem :: FDIFF_1:26

for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL 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 :: FDIFF_1:27

for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL 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 :: FDIFF_1:28

for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL 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 :: FDIFF_1:29

for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL 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 = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) ) )

proof end;

theorem :: FDIFF_1:30

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )

proof end;

theorem :: FDIFF_1:31

for r, p being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )

proof end;

theorem Th32: :: FDIFF_1:32

for f being PartFunc of REAL,REAL
for x0 being real number st f is_differentiable_in x0 holds
f is_continuous_in x0

proof end;

theorem :: FDIFF_1:33

for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
f | X is continuous

proof end;

theorem Th34: :: FDIFF_1:34

for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z

proof end;

theorem :: FDIFF_1:35

ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

definition

let f be PartFunc of REAL,REAL;
attr f is differentiable means :Def9: :: FDIFF_1:def 9
f is_differentiable_on dom f;

end;

:: deftheorem Def9 defines differentiable FDIFF_1:def 9 :

Lm1: {} REAL is closed

proof end;

Lm2: [#] REAL is open

proof end;

registration

cluster V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued differentiable Element of K21(K22(REAL,REAL));
existence

proof end;

end;

theorem :: FDIFF_1:36

for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,REAL st Z c= dom f holds
f is_differentiable_on Z

proof end;