:: Difference and Difference Quotient
:: 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 ;
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
 ex b1 being PartFunc of REAL,REAL st
( dom b1 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds
b1 . x = f . (x + h) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of REAL,REAL st dom b1 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds
b1 . x = f . (x + h) ) & dom b2 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds
b2 . x = f . (x + h) ) holds
b1 = b2
proofend;
end;

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

definition
let f be Function of REAL,REAL;
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
 Shift (f,h) is Function of REAL,REAL
proofend;
compatibility
 for b1 being Function of REAL,REAL holds
( b1 = Shift (f,h) iff for x being Real holds b1 . x = f . (x + h) )
proofend;
end;

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

definition
let f be PartFunc of REAL,REAL;
let h be real number ;
func fD (f,h) ->  PartFunc of REAL,REAL equals :: DIFF_1:def 3
(Shift (f,h)) - f;
coherence
 (Shift (f,h)) - f is PartFunc of REAL,REAL ;
end;

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

registration
let f be Function of REAL,REAL;
let h be real number ;
cluster fD (f,h) ->  quasi_total ;
coherence
 fD (f,h) is quasi_total
proofend;
end;

definition
let f be PartFunc of REAL,REAL;
let h be real number ;
func bD (f,h) ->  PartFunc of REAL,REAL equals :: DIFF_1:def 4
f - (Shift (f,(- h)));
coherence
 f - (Shift (f,(- h))) is PartFunc of REAL,REAL ;
end;

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

registration
let f be Function of REAL,REAL;
let h be real number ;
cluster bD (f,h) ->  quasi_total ;
coherence
 bD (f,h) is quasi_total
proofend;
end;

definition
let f be PartFunc of REAL,REAL;
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)))) is PartFunc of REAL,REAL ;
end;

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

registration
let f be Function of REAL,REAL;
let h be real number ;
cluster cD (f,h) ->  quasi_total ;
coherence
 cD (f,h) is quasi_total
proofend;
end;

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

notation
let f be PartFunc of REAL,REAL;
let h be real number ;
synonym  fdif (f,h) for  forward_difference (f,h);
end;

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

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

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

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

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

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

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

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

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

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

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

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

notation
let f be PartFunc of REAL,REAL;
let h be real number ;
synonym  bdif (f,h) for  backward_difference (f,h);
end;

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

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

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

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

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

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

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

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

notation
let f be PartFunc of REAL,REAL;
let h be real number ;
synonym  cdif (f,h) for  central_difference (f,h);
end;

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

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

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

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

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

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

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

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

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

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

definition
let f be real-valued Function;
let x0, x1 be real number ;
func[!f,x0,x1!] ->  Real equals :: DIFF_1:def 9
((f . x0) - (f . x1)) / (x0 - x1);
correctness
coherence
((f . x0) - (f . x1)) / (x0 - x1) is Real;
;
end;

:: 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 :: 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_:_
 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 :: 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
for x0, x1 being Real
for f being Function of REAL,REAL holds [!f,x0,x1!] = [!f,x1,x0!]
proofend;

theorem :: DIFF_1:30
for x0, x1 being Real
for f being Function of REAL,REAL st f is constant holds
[!f,x0,x1!] = 0
proofend;

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!]
proofend;

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!]
proofend;

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

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

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

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

definition
let S be Functional_Sequence of REAL,REAL;
attrS is Sequence-yielding  means :Def12: :: DIFF_1:def 12
 for n being Element of NAT holds S . n is Real_Sequence;
end;

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

registration
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 b1 being Functional_Sequence of REAL,REAL st b1 is Sequence-yielding
proofend;
end;

definition
mode Seq_Sequence is Sequence-yielding Functional_Sequence of REAL,REAL;
end;

definition
let S be Seq_Sequence;
let n be Element of NAT ;
:: original:.
redefine funcS . n ->  Real_Sequence;
coherence
 S . n is Real_Sequence by Def12;
end;

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

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) &amp; ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
proofend;

theorem :: DIFF_1:38
for x, h being Real
for f being PartFunc of REAL,REAL st x in dom f &amp; x - h in dom f holds
(bD (f,h)) . x = (f . x) - (f . (x - h))
proofend;

theorem :: DIFF_1:39
for x, h being Real
for f being PartFunc of REAL,REAL st x + (h / 2) in dom f &amp; x - (h / 2) in dom f holds
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))
proofend;