:: by Bo Li , Yan Zhang and Xiquan Liang

::

:: Received September 29, 2006

:: Copyright (c) 2006-2012 Association of Mizar Users

begin

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

ex b_{1} being PartFunc of REAL,REAL st

( dom b_{1} = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds

b_{1} . x = f . (x + h) ) )

for b_{1}, b_{2} being PartFunc of REAL,REAL st dom b_{1} = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds

b_{1} . x = f . (x + h) ) & dom b_{2} = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds

b_{2} . x = f . (x + h) ) holds

b_{1} = b_{2}

end;
let h be real number ;

func Shift (f,h) -> PartFunc of REAL,REAL means :Def1: :: DIFF_1:def 1

( dom it = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds

it . x = f . (x + h) ) );

existence ( dom it = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds

it . x = f . (x + h) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Shift DIFF_1:def 1 :

for f being PartFunc of REAL,REAL

for h being real number

for b_{3} being PartFunc of REAL,REAL holds

( b_{3} = Shift (f,h) iff ( dom b_{3} = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds

b_{3} . x = f . (x + h) ) ) );

for f being PartFunc of REAL,REAL

for h being real number

for b

( b

b

definition

let f be Function of REAL,REAL;

let h be real number ;

Shift (f,h) is Function of REAL,REAL

for b_{1} being Function of REAL,REAL holds

( b_{1} = Shift (f,h) iff for x being Real holds b_{1} . x = f . (x + h) )

end;
let h be real number ;

:: original: Shift

redefine func Shift (f,h) -> Function of REAL,REAL means :Def2: :: DIFF_1:def 2

for x being Real holds it . x = f . (x + h);

coherence redefine func Shift (f,h) -> Function of REAL,REAL means :Def2: :: DIFF_1:def 2

for x being Real holds it . x = f . (x + h);

Shift (f,h) is Function of REAL,REAL

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def2 defines Shift DIFF_1:def 2 :

for f being Function of REAL,REAL

for h being real number

for b_{3} being Function of REAL,REAL holds

( b_{3} = Shift (f,h) iff for x being Real holds b_{3} . x = f . (x + h) );

for f being Function of REAL,REAL

for h being real number

for b

( b

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

coherence

(Shift (f,h)) - f is PartFunc of REAL,REAL ;

end;
let h be real number ;

coherence

(Shift (f,h)) - f is PartFunc of REAL,REAL ;

:: 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;

for f being PartFunc of REAL,REAL

for h being real number holds fD (f,h) = (Shift (f,h)) - f;

registration
end;

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

coherence

f - (Shift (f,(- h))) is PartFunc of REAL,REAL ;

end;
let h be real number ;

coherence

f - (Shift (f,(- h))) is PartFunc of REAL,REAL ;

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

for f being PartFunc of REAL,REAL

for h being real number holds bD (f,h) = f - (Shift (f,(- h)));

registration
end;

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

(Shift (f,(h / 2))) - (Shift (f,(- (h / 2)))) is PartFunc of REAL,REAL ;

end;
let h be real number ;

func cD (f,h) -> PartFunc of REAL,REAL equals :: DIFF_1:def 5

(Shift (f,(h / 2))) - (Shift (f,(- (h / 2))));

coherence (Shift (f,(h / 2))) - (Shift (f,(- (h / 2))));

(Shift (f,(h / 2))) - (Shift (f,(- (h / 2)))) is PartFunc of REAL,REAL ;

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

for f being PartFunc of REAL,REAL

for h being real number holds cD (f,h) = (Shift (f,(h / 2))) - (Shift (f,(- (h / 2))));

registration
end;

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

ex b_{1} being Functional_Sequence of REAL,REAL st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = fD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of REAL,REAL st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = fD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = fD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
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 Nat holds it . (n + 1) = fD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = fD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines forward_difference DIFF_1:def 6 :

for f being PartFunc of REAL,REAL

for h being real number

for b_{3} being Functional_Sequence of REAL,REAL holds

( b_{3} = forward_difference (f,h) iff ( b_{3} . 0 = f & ( for n being Nat holds b_{3} . (n + 1) = fD ((b_{3} . n),h) ) ) );

for f being PartFunc of REAL,REAL

for h being real number

for b

( b

notation

let f be PartFunc of REAL,REAL;

let h be real number ;

synonym fdif (f,h) for forward_difference (f,h);

end;
let h be real number ;

synonym fdif (f,h) for forward_difference (f,h);

theorem :: DIFF_1:1

for x, h being Real

for f being PartFunc of REAL,REAL st x in dom f & x + h in dom f holds

(fD (f,h)) . x = (f . (x + h)) - (f . x)

for f being PartFunc of REAL,REAL st x in dom f & x + h in dom f holds

(fD (f,h)) . x = (f . (x + h)) - (f . x)

proof end;

theorem Th2: :: DIFF_1:2

for h being Real

for f being Function of REAL,REAL

for n being Nat holds (fdif (f,h)) . n is Function of REAL,REAL

for f being Function of REAL,REAL

for n being Nat holds (fdif (f,h)) . n is Function of REAL,REAL

proof end;

theorem Th3: :: DIFF_1:3

for h, x being Real

for f being Function of REAL,REAL holds (fD (f,h)) . x = (f . (x + h)) - (f . x)

for f being Function of REAL,REAL holds (fD (f,h)) . x = (f . (x + h)) - (f . x)

proof end;

theorem Th4: :: DIFF_1:4

for h, x being Real

for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - (f . (x - h))

for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - (f . (x - h))

proof end;

theorem Th5: :: DIFF_1:5

for h, x being Real

for f being Function of REAL,REAL holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

for f being Function of REAL,REAL holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

proof end;

theorem :: DIFF_1:6

for n being Element of NAT

for h being Real

for f being Function of REAL,REAL st f is constant holds

for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0

for h being Real

for f being Function of REAL,REAL st f is constant holds

for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0

proof end;

theorem Th7: :: DIFF_1:7

for n being Element of NAT

for r, h, x being Real

for f being Function of REAL,REAL holds ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x)

for r, h, x being Real

for f being Function of REAL,REAL holds ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x)

proof end;

theorem Th8: :: DIFF_1:8

for n being Element of NAT

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x)

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_1:9

for n being Element of NAT

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x)

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_1:10

for n being Element of NAT

for r1, r2, h, x being Real

for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))

for r1, r2, h, x being Real

for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_1:11

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x)

for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x)

proof end;

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

ex b_{1} being Functional_Sequence of REAL,REAL st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = bD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of REAL,REAL st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = bD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = bD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
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 Nat holds it . (n + 1) = bD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = bD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines backward_difference DIFF_1:def 7 :

for f being PartFunc of REAL,REAL

for h being real number

for b_{3} being Functional_Sequence of REAL,REAL holds

( b_{3} = backward_difference (f,h) iff ( b_{3} . 0 = f & ( for n being Nat holds b_{3} . (n + 1) = bD ((b_{3} . n),h) ) ) );

for f being PartFunc of REAL,REAL

for h being real number

for b

( b

notation

let f be PartFunc of REAL,REAL;

let h be real number ;

synonym bdif (f,h) for backward_difference (f,h);

end;
let h be real number ;

synonym bdif (f,h) for backward_difference (f,h);

theorem Th12: :: DIFF_1:12

for h being Real

for f being Function of REAL,REAL

for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL

for f being Function of REAL,REAL

for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL

proof end;

theorem :: DIFF_1:13

for n being Element of NAT

for h being Real

for f being Function of REAL,REAL st f is constant holds

for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0

for h being Real

for f being Function of REAL,REAL st f is constant holds

for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0

proof end;

theorem Th14: :: DIFF_1:14

for n being Element of NAT

for r, h, x being Real

for f being Function of REAL,REAL holds ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x)

for r, h, x being Real

for f being Function of REAL,REAL holds ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x)

proof end;

theorem Th15: :: DIFF_1:15

for n being Element of NAT

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x)

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_1:16

for n being Element of NAT

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x)

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_1:17

for n being Element of NAT

for r1, r2, h, x being Real

for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x))

for r1, r2, h, x being Real

for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_1:18

for h, x being Real

for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x)

for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x)

proof end;

definition

let f be PartFunc of REAL,REAL;

let h be real number ;

ex b_{1} being Functional_Sequence of REAL,REAL st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = cD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of REAL,REAL st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = cD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = cD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
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 Nat holds it . (n + 1) = cD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = cD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines central_difference DIFF_1:def 8 :

for f being PartFunc of REAL,REAL

for h being real number

for b_{3} being Functional_Sequence of REAL,REAL holds

( b_{3} = central_difference (f,h) iff ( b_{3} . 0 = f & ( for n being Nat holds b_{3} . (n + 1) = cD ((b_{3} . n),h) ) ) );

for f being PartFunc of REAL,REAL

for h being real number

for b

( b

notation

let f be PartFunc of REAL,REAL;

let h be real number ;

synonym cdif (f,h) for central_difference (f,h);

end;
let h be real number ;

synonym cdif (f,h) for central_difference (f,h);

theorem Th19: :: DIFF_1:19

for h being Real

for f being Function of REAL,REAL

for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL

for f being Function of REAL,REAL

for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL

proof end;

theorem :: DIFF_1:20

for n being Element of NAT

for h being Real

for f being Function of REAL,REAL st f is constant holds

for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0

for h being Real

for f being Function of REAL,REAL st f is constant holds

for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0

proof end;

theorem Th21: :: DIFF_1:21

for n being Element of NAT

for r, h, x being Real

for f being Function of REAL,REAL holds ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x)

for r, h, x being Real

for f being Function of REAL,REAL holds ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x)

proof end;

theorem Th22: :: DIFF_1:22

for n being Element of NAT

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x)

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_1:23

for n being Element of NAT

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x)

for h, x being Real

for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_1:24

for n being Element of NAT

for r1, r2, h, x being Real

for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x))

for r1, r2, h, x being Real

for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_1:25

for h, x being Real

for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x)

for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x)

proof end;

theorem :: DIFF_1:26

for n being Element of NAT

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h))

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h))

proof end;

theorem :: DIFF_1:27

for n being Element of NAT

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h))

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h))

proof end;

theorem :: DIFF_1:28

for n being Element of NAT

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2))

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2))

proof end;

definition

let f be real-valued Function;

let x0, x1 be real number ;

correctness

coherence

((f . x0) - (f . x1)) / (x0 - x1) is Real;

;

end;
let x0, x1 be real number ;

correctness

coherence

((f . x0) - (f . x1)) / (x0 - x1) is Real;

;

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

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 ;

correctness

coherence

([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2) is Real;

;

end;
let x0, x1, x2 be real number ;

correctness

coherence

([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2) is Real;

;

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

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 ;

coherence

([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3) is Real;

;

end;
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 ([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3);

coherence

([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3) is Real;

;

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

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 Th31: :: DIFF_1:31

for r, x0, x1 being Real

for f being Function of REAL,REAL holds [!(r (#) f),x0,x1!] = r * [!f,x0,x1!]

for f being Function of REAL,REAL holds [!(r (#) f),x0,x1!] = r * [!f,x0,x1!]

proof end;

theorem Th32: :: DIFF_1:32

for x0, x1 being Real

for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!]

for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!]

proof end;

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

for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!])

proof end;

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

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

proof end;

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

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

proof end;

theorem :: DIFF_1:36

for m, n being Element of NAT

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x

for h, x being Real

for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x

proof end;

definition

let S be Functional_Sequence of REAL,REAL;

end;
attr S is Sequence-yielding means :Def12: :: DIFF_1:def 12

for n being Element of NAT holds S . n is Real_Sequence;

for n being Element of NAT holds S . n is Real_Sequence;

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

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

proof end;

registration

ex b_{1} being Functional_Sequence of REAL,REAL st b_{1} is Sequence-yielding
end;

cluster non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Sequence-yielding for Element of bool [:NAT,(PFuncs (REAL,REAL)):];

existence ex b

proof end;

definition

let S be Seq_Sequence;

let n be Element of NAT ;

:: original: .

redefine func S . n -> Real_Sequence;

coherence

S . n is Real_Sequence by Def12;

end;
let n be Element of NAT ;

:: original: .

redefine func S . n -> Real_Sequence;

coherence

S . n is Real_Sequence by Def12;

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)))

proof end;

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) )

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) )

proof end;

theorem :: DIFF_1:38

for x, h being Real

for f being PartFunc of REAL,REAL st x in dom f & x - h in dom f holds

(bD (f,h)) . x = (f . x) - (f . (x - h))

for f being PartFunc of REAL,REAL st x in dom f & x - h in dom f holds

(bD (f,h)) . x = (f . x) - (f . (x - h))

proof end;

theorem :: DIFF_1:39

for x, h being Real

for f being PartFunc of REAL,REAL st x + (h / 2) in dom f & x - (h / 2) in dom f holds

(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

for f being PartFunc of REAL,REAL st x + (h / 2) in dom f & x - (h / 2) in dom f holds

(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

proof end;