begin
:: deftheorem Def1 defines Shift DIFF_1:def 1 :
for f being PartFunc of REAL,REAL
for h being real number
for b3 being PartFunc of REAL,REAL holds
( b3 = Shift (f,h) iff ( dom b3 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds
b3 . x = f . (x + h) ) ) );
:: deftheorem Def2 defines Shift DIFF_1:def 2 :
for f being Function of REAL,REAL
for h being real number
for b3 being Function of REAL,REAL holds
( b3 = Shift (f,h) iff for x being Real holds b3 . x = f . (x + h) );
:: deftheorem defines fD DIFF_1:def 3 :
for f being PartFunc of REAL,REAL
for h being real number holds fD (f,h) = (Shift (f,h)) - f;
:: deftheorem defines bD DIFF_1:def 4 :
for f being PartFunc of REAL,REAL
for h being real number holds bD (f,h) = f - (Shift (f,(- h)));
:: deftheorem defines cD DIFF_1:def 5 :
for f being PartFunc of REAL,REAL
for h being real number holds cD (f,h) = (Shift (f,(h / 2))) - (Shift (f,(- (h / 2))));
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:
(
it . 0 = f & ( for
n being
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 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 Nat holds b1 . (n + 1) = fD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = fD ((b2 . n),h) ) holds
b1 = b2
end;
:: deftheorem Def6 defines forward_difference DIFF_1:def 6 :
for f being PartFunc of REAL,REAL
for h being real number
for b3 being Functional_Sequence of REAL,REAL holds
( b3 = forward_difference (f,h) iff ( b3 . 0 = f & ( for n being Nat holds b3 . (n + 1) = fD ((b3 . n),h) ) ) );
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
theorem
theorem
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:
(
it . 0 = f & ( for
n being
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 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 Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = bD ((b2 . n),h) ) holds
b1 = b2
end;
:: deftheorem Def7 defines backward_difference DIFF_1:def 7 :
for f being PartFunc of REAL,REAL
for h being real number
for b3 being Functional_Sequence of REAL,REAL holds
( b3 = backward_difference (f,h) iff ( b3 . 0 = f & ( for n being Nat holds b3 . (n + 1) = bD ((b3 . n),h) ) ) );
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem
theorem
theorem
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:
(
it . 0 = f & ( for
n being
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 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 Nat holds b1 . (n + 1) = cD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = cD ((b2 . n),h) ) holds
b1 = b2
end;
:: deftheorem Def8 defines central_difference DIFF_1:def 8 :
for f being PartFunc of REAL,REAL
for h being real number
for b3 being Functional_Sequence of REAL,REAL holds
( b3 = central_difference (f,h) iff ( b3 . 0 = f & ( for n being Nat holds b3 . (n + 1) = cD ((b3 . n),h) ) ) );
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines [! DIFF_1:def 9 :
for f being real-valued Function
for x0, x1 being real number holds [!f,x0,x1!] = ((f . x0) - (f . x1)) / (x0 - x1);
definition
let f be
real-valued Function;
let x0,
x1,
x2 be
real number ;
func [!f,x0,x1,x2!] -> Real equals
([!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 :
for f being real-valued Function
for x0, x1, x2 being real number holds [!f,x0,x1,x2!] = ([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2);
definition
let f be
real-valued Function;
let x0,
x1,
x2,
x3 be
real number ;
func [!f,x0,x1,x2,x3!] -> Real equals
([!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
theorem
theorem Th31:
theorem Th32:
theorem
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:
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
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
:: deftheorem Def12 defines Sequence-yielding DIFF_1:def 12 :
for S being Functional_Sequence of REAL,REAL holds
( S is Sequence-yielding iff for n being Element of NAT holds S . n is Real_Sequence );
Lm1:
ex S being Functional_Sequence of REAL,REAL st
for n being Element of NAT holds S . n is Real_Sequence
Lm2:
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
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) )
theorem
theorem