:: Difference and Difference Quotient
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received September 29, 2006
:: Copyright (c) 2006 Association of Mizar Users
:: deftheorem Def1 defines Shift DIFF_1:def 1 :
:: deftheorem Def2 defines Shift DIFF_1:def 2 :
:: deftheorem defines fD DIFF_1:def 3 :
:: deftheorem defines bD DIFF_1:def 4 :
theorem :: DIFF_1:1
:: deftheorem defines cD DIFF_1:def 5 :
definition
let f be
PartFunc of
REAL ,
REAL ;
let h be
real number ;
func forward_difference f,
h -> Functional_Sequence of
REAL ,
REAL means :
Def6:
:: DIFF_1:def 6
(
it . 0 = f & ( for
n being
Element of
NAT holds
it . (n + 1) = fD (it . n),
h ) );
existence
ex b1 being Functional_Sequence of REAL ,REAL st
( b1 . 0 = f & ( for n being Element of NAT holds b1 . (n + 1) = fD (b1 . n),h ) )
uniqueness
for b1, b2 being Functional_Sequence of REAL ,REAL st b1 . 0 = f & ( for n being Element of NAT holds b1 . (n + 1) = fD (b1 . n),h ) & b2 . 0 = f & ( for n being Element of NAT holds b2 . (n + 1) = fD (b2 . n),h ) holds
b1 = b2
end;
:: deftheorem Def6 defines forward_difference DIFF_1:def 6 :
Lm1:
for h being Real
for f being Function of REAL , REAL holds fD f,h is Function of REAL , REAL
;
theorem Th2: :: DIFF_1:2
theorem Th3: :: DIFF_1:3
theorem Th4: :: DIFF_1:4
theorem Th5: :: DIFF_1:5
theorem :: DIFF_1:6
theorem Th7: :: DIFF_1:7
theorem Th8: :: DIFF_1:8
theorem :: DIFF_1:9
theorem :: DIFF_1:10
theorem :: DIFF_1:11
definition
let f be
PartFunc of
REAL ,
REAL ;
let h be
real number ;
func backward_difference f,
h -> Functional_Sequence of
REAL ,
REAL means :
Def7:
:: DIFF_1:def 7
(
it . 0 = f & ( for
n being
Element of
NAT holds
it . (n + 1) = bD (it . n),
h ) );
existence
ex b1 being Functional_Sequence of REAL ,REAL st
( b1 . 0 = f & ( for n being Element of NAT holds b1 . (n + 1) = bD (b1 . n),h ) )
uniqueness
for b1, b2 being Functional_Sequence of REAL ,REAL st b1 . 0 = f & ( for n being Element of NAT holds b1 . (n + 1) = bD (b1 . n),h ) & b2 . 0 = f & ( for n being Element of NAT holds b2 . (n + 1) = bD (b2 . n),h ) holds
b1 = b2
end;
:: deftheorem Def7 defines backward_difference DIFF_1:def 7 :
Lm2:
for h being Real
for f being Function of REAL , REAL holds bD f,h is Function of REAL , REAL
;
theorem Th12: :: DIFF_1:12
theorem :: DIFF_1:13
theorem Th14: :: DIFF_1:14
theorem Th15: :: DIFF_1:15
theorem :: DIFF_1:16
theorem :: DIFF_1:17
theorem :: DIFF_1:18
definition
let f be
PartFunc of
REAL ,
REAL ;
let h be
real number ;
func central_difference f,
h -> Functional_Sequence of
REAL ,
REAL means :
Def8:
:: DIFF_1:def 8
(
it . 0 = f & ( for
n being
Element of
NAT holds
it . (n + 1) = cD (it . n),
h ) );
existence
ex b1 being Functional_Sequence of REAL ,REAL st
( b1 . 0 = f & ( for n being Element of NAT holds b1 . (n + 1) = cD (b1 . n),h ) )
uniqueness
for b1, b2 being Functional_Sequence of REAL ,REAL st b1 . 0 = f & ( for n being Element of NAT holds b1 . (n + 1) = cD (b1 . n),h ) & b2 . 0 = f & ( for n being Element of NAT holds b2 . (n + 1) = cD (b2 . n),h ) holds
b1 = b2
end;
:: deftheorem Def8 defines central_difference DIFF_1:def 8 :
Lm3:
for h being Real
for f being Function of REAL , REAL holds cD f,h is Function of REAL , REAL
;
theorem Th19: :: DIFF_1:19
theorem :: DIFF_1:20
theorem Th21: :: DIFF_1:21
theorem Th22: :: DIFF_1:22
theorem :: DIFF_1:23
theorem :: DIFF_1:24
theorem :: DIFF_1:25
theorem :: DIFF_1:26
theorem :: DIFF_1:27
theorem :: DIFF_1:28
:: deftheorem defines [! DIFF_1:def 9 :
definition
let f be
real-valued Function;
let x0,
x1,
x2 be
real number ;
func [!f,x0,x1,x2!] -> Real equals :: DIFF_1:def 10
([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2);
correctness
coherence
([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2) is Real;
;
end;
:: deftheorem defines [! DIFF_1:def 10 :
definition
let f be
real-valued Function;
let x0,
x1,
x2,
x3 be
real number ;
func [!f,x0,x1,x2,x3!] -> Real equals :: DIFF_1:def 11
([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3);
correctness
coherence
([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3) is Real;
;
end;
:: deftheorem defines [! DIFF_1:def 11 :
for
f being
real-valued Function for
x0,
x1,
x2,
x3 being
real number holds
[!f,x0,x1,x2,x3!] = ([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3);
theorem :: DIFF_1:29
theorem :: DIFF_1:30
theorem Th31: :: DIFF_1:31
theorem Th32: :: DIFF_1:32
theorem :: DIFF_1:33
for
r1,
r2,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL ,
REAL holds
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!])
theorem Th34: :: DIFF_1:34
for
x0,
x1,
x2 being
Real for
f being
Function of
REAL ,
REAL st
x0,
x1,
x2 are_mutually_different holds
(
[!f,x0,x1,x2!] = [!f,x1,x2,x0!] &
[!f,x0,x1,x2!] = [!f,x2,x1,x0!] )
theorem :: DIFF_1:35
for
x0,
x1,
x2 being
Real for
f being
Function of
REAL ,
REAL st
x0,
x1,
x2 are_mutually_different holds
(
[!f,x0,x1,x2!] = [!f,x2,x0,x1!] &
[!f,x0,x1,x2!] = [!f,x1,x0,x2!] )
theorem :: DIFF_1:36
:: deftheorem Def12 defines Sequence-yielding DIFF_1:def 12 :
Lm4:
ex S being Functional_Sequence of REAL ,REAL st
for n being Element of NAT holds S . n is Real_Sequence
Lm5:
for h, x being Real
for f1, f2 being Function of REAL , REAL holds ((fdif (f1 (#) f2),h) . 1) . x = ((f1 . x) * (((fdif f2,h) . 1) . x)) + ((((fdif f1,h) . 1) . x) * (f2 . (x + h)))
theorem :: DIFF_1:37
for
h,
x being
Real for
f1,
f2 being
Function of
REAL ,
REAL for
S being
Seq_Sequence st ( for
n,
i being
Element of
NAT st
i <= n holds
(S . n) . i = ((n choose i) * (((fdif f1,h) . i) . x)) * (((fdif f2,h) . (n -' i)) . (x + (i * h))) ) holds
(
((fdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 &
((fdif (f1 (#) f2),h) . 2) . x = Sum (S . 2),2 )