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