begin
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
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!] )
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) )