:: Difference of Function on Vector Space over $\mathbbF$
:: by Kenichi Arai , Ken Wakabayashi and Hiroyuki Okazaki
::
:: Received September 26, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, NUMBERS, CARD_1, SUBSET_1, ARYTM_3, SUPINF_2,
ARYTM_1, RELAT_1, MESFUNC1, FUNCT_1, VECTSP_1, FUNCT_7, DIFF_1, PARTFUN1,
SEQFUNC, VALUED_1, MEMBER_1, TARSKI, NAT_1, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, ORDINAL1,
PARTFUN1, FUNCT_2,
NUMBERS, XCMPLX_0, NAT_1, SEQFUNC, STRUCT_0, ALGSTR_0, RLVECT_1,
VECTSP_1, VFUNCT_1, BINOM;
constructors NAT_1, RELSET_1, VECTSP_1, SEQFUNC, VFUNCT_1, BINOM, ALGSTR_1;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, XBOOLE_0,
PARTFUN1, ALGSTR_1, FUNCT_2, VFUNCT_1, NAT_1;
requirements NUMERALS, SUBSET, ARITHM, BOOLE;
definitions TARSKI;
equalities ALGSTR_0;
theorems FUNCT_2, RLVECT_1, TARSKI, VECTSP_1, PARTFUN1, FUNCT_1, XBOOLE_0,
SUBSET_1, VFUNCT_1, BINOM;
schemes NAT_1, PARTFUN2, RECDEF_1, SEQ_1, XBOOLE_0;
begin
reserve C for non empty set;
reserve GF for Field,
V for VectSp of GF,
v,u for Element of V,
W for Subset of V;
reserve f,f1,f2,f3 for PartFunc of C,V;
definition
let C;
let GF,V;
let f be PartFunc of C,V;
let r be Element of GF;
deffunc F(Element of C) = r * (f/.$1);
defpred P[set] means $1 in dom f;
func r(#)f -> PartFunc of C,V means
:Def4X:
dom it = dom f &
for c being Element of C st c in dom it holds it/.c = r * (f/.c);
existence
proof
consider F be PartFunc of C,V such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F/.c = F(c)
from PARTFUN2:sch 2;
take F;
thus thesis by A1,A2,SUBSET_1:3;
end;
uniqueness
proof
set X = dom f;
thus for f,g being PartFunc of C,V st
(dom f = X & for c be Element of C st c in dom f holds f/.c = F(c)) &
(dom g = X & for c be Element of
C st c in dom g holds g/.c = F(c)) holds f = g from PARTFUN2:sch 3;
end;
end;
registration
let C,GF,V;
let f be Function of C,V;
let r be Element of GF;
cluster r(#)f -> total;
coherence
proof
dom (r(#)f) = dom f by Def4X
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
definition
let GF,V,v,W;
func v ++ W -> Subset of V equals
{v + u : u in W};
coherence
proof
set Y = {v + u : u in W};
defpred Sep[object] means ex u st $1 = v + u & u in W;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of V & Sep[x]
from XBOOLE_0:sch 1;
for x be object st x in X holds x in the carrier of V by A1;
then reconsider X as Subset of V by TARSKI:def 3;
A2: Y c= X
proof
let x be object;
assume x in Y;
then ex u st x = v + u & u in W;
hence thesis by A1;
end;
X c= Y
proof
let x be object;
assume x in X;
then ex u st x = v + u & u in W by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
definition
let F,G be Field;
let V be VectSp of F;
let W be VectSp of G;
let f be PartFunc of V,W;
let h be Element of V;
func Shift (f,h) -> PartFunc of V,W means
:Def1:
dom it = (-h) ++ (dom f) &
(for x being Element of V st x in (-h) ++ (dom f) holds it.x = f.(x+h));
existence
proof
deffunc F(Element of V) = In(f.($1+h),the carrier of W);
set X = -h ++ dom f;
defpred P[set] means $1 in X;
consider F being PartFunc of V,W such that
A1: (for x be Element of V holds x in dom F iff P[x]) & for x be
Element of V st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
take F;
for y being object st y in X holds y in dom F by A1; then
A2: X c= dom F by TARSKI:def 3;
for y being object st y in dom F holds y in X by A1;
then dom F c= X by TARSKI:def 3;
hence dom F = X by A2,XBOOLE_0:def 10;
for x be Element of V st x in X holds F.x = f.(x+h)
proof
let x be Element of V;
assume
A3: x in X; then
A4: F.x = F(x) by A1;
consider u be Element of V such that
A5: x = (-h) + u & u in dom f by A3;
x + h = u + ((-h)+h) by RLVECT_1:def 3,A5
.= u + 0.V by VECTSP_1:16
.= u by RLVECT_1:def 4;
hence thesis by A4,SUBSET_1:def 8,PARTFUN1:4,A5;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be PartFunc of V,W;
set X = -h ++ dom f;
assume that
A6: dom f1 = X and
A7: for x be Element of V st x in X holds f1.x = f.(x+h) and
A8: dom f2 = X and
A9: for x be Element of V st x in X holds f2.x = f.(x+h);
for x being Element of V st x in dom f1 holds f1.x = f2.x
proof
let x be Element of V;
assume
A10: x in dom f1;
then f1.x = f.(x+h) by A6,A7;
hence thesis by A6,A9,A10;
end;
hence f1 = f2 by A6,A8,PARTFUN1:5;
end;
end;
theorem MEASURE624:
for x being Element of V, A being Subset of V st A = the carrier of V
holds x ++ A = A
proof
let x be Element of V, A be Subset of V;
assume
P0: A = the carrier of V;
for y being object holds y in x ++ A iff y in A
proof
let y be object;
y in A implies y in x ++ A
proof
assume y in A;
then reconsider w = y as Element of V;
(w - x) + x = w - (x-x) by RLVECT_1:29
.= w - 0.V by RLVECT_1:15
.= w by RLVECT_1:13;
hence y in x ++ A by P0;
end;
hence thesis by P0;
end;
hence x ++ A = A by TARSKI:2;
end;
definition
let F,G be Field;
let V be VectSp of F;
let W be VectSp of G;
let f be Function of V,W;
let h be Element of V;
redefine func Shift(f,h) -> Function of V,W means :: redefines Shift (VSDIFF_1, definition)
:Def2:
for x be Element of V holds it.x = f.(x+h);
coherence
proof
dom Shift(f,h) = -h ++ dom f & dom f = the carrier of V
by Def1,FUNCT_2:def 1;
then dom Shift(f,h) = the carrier of V by MEASURE624;
hence thesis by FUNCT_2:def 1;
end;
compatibility
proof
for IT being Function of V,W holds
IT = Shift(f,h) iff for x be Element of V holds IT.x = f.(x+h)
proof
let IT be Function of V,W;
hereby
assume
A1: IT = Shift(f,h);
let x be Element of V;
dom Shift(f,h) = the carrier of V by A1,FUNCT_2:def 1;
then x in dom Shift(f,h);
then x in (-h ++ dom f) by Def1;
hence IT.x = f.(x+h) by A1,Def1;
end;
dom Shift(f,h) = -h ++ dom f & dom f = the carrier of V
by Def1,FUNCT_2:def 1;
then dom Shift(f,h) = the carrier of V by MEASURE624;
then
A2: dom IT = dom Shift(f,h) by FUNCT_2:def 1;
assume
A3: for x be Element of V holds IT.x = f.(x+h);
for x being Element of V st x in dom IT holds IT.x = Shift(f,h).x
proof
let x be Element of V;
assume x in dom IT; then
A4: x in (-h ++ dom f) by A2,Def1;
IT.x = f.(x+h) by A3;
hence thesis by A4,Def1;
end;
hence thesis by A2,PARTFUN1:5;
end;
hence thesis;
end;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be PartFunc of V,W;
func fD(f,h) -> PartFunc of V,W equals
Shift(f,h) - f;
coherence;
end;
registration
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
cluster fD(f,h) -> quasi_total;
coherence
proof
dom fD(f,h) = dom Shift(f,h) /\ dom f by VFUNCT_1:def 2
.= (the carrier of V) /\ dom f by FUNCT_2:def 1
.= (the carrier of V) /\ (the carrier of V) by FUNCT_2:def 1
.= the carrier of V;
hence thesis by FUNCT_2:def 1;
end;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be PartFunc of V,W;
func bD(f,h) -> PartFunc of V,W equals
f - Shift(f,-h);
coherence;
end;
registration
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
cluster bD(f,h) -> quasi_total;
coherence
proof
dom bD(f,h) = dom Shift(f,-h) /\ dom f by VFUNCT_1:def 2
.= (the carrier of V) /\ dom f by FUNCT_2:def 1
.= (the carrier of V) /\ (the carrier of V) by FUNCT_2:def 1
.= (the carrier of V);
hence thesis by FUNCT_2:def 1;
end;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be PartFunc of V,W;
func cD(f,h) -> PartFunc of V,W equals
Shift(f,(2*1.F)"*h) - Shift(f,-(2*1.F)"*h);
coherence;
end;
registration
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
cluster cD(f,h) -> quasi_total;
coherence
proof
dom cD(f,h) = dom Shift(f,(2*1.F)"*h) /\ dom Shift(f,-(2*1.F)"*h)
by VFUNCT_1:def 2
.= (the carrier of V) /\ dom Shift(f,-(2*1.F)"*h) by FUNCT_2:def 1
.= (the carrier of V) /\ (the carrier of V) by FUNCT_2:def 1
.= (the carrier of V);
hence thesis by FUNCT_2:def 1;
end;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
func forward_difference(f,h) ->
Functional_Sequence of the carrier of V,the carrier of W means
:Def6:
it.0 = f & for n being Nat holds it.(n+1) = fD(it.n,h);
existence
proof
reconsider fZ = f as Element of PFuncs(the carrier of V,the carrier of W)
by PARTFUN1:45;
defpred R[set,set,set] means
ex g being PartFunc of V, W st $2 = g &
$3 = fD(g,h);
A1: for n be Nat
for x being Element of PFuncs(the carrier of V,the carrier of W)
ex y being Element of PFuncs(the carrier of V,the carrier of W) st R[n,x,y]
proof
let n be Nat;
let x be Element of PFuncs (the carrier of V,the carrier of W);
reconsider x9 = x as PartFunc of the carrier of V,the carrier of W
by PARTFUN1:46;
reconsider y = fD(x9,h) as Element of PFuncs (the carrier of V,
the carrier of W) by PARTFUN1:45;
ex w being PartFunc of the carrier of V,the carrier of W st x = w &
y = fD(w,h);
hence thesis;
end;
consider g be sequence of PFuncs(the carrier of V,the carrier of W)
such that
A2: g.0 = fZ & for n being Nat holds R[n,g.n,g.(n+1)]
from RECDEF_1:sch 2(A1);
reconsider g as Functional_Sequence of the carrier of V,the carrier of W;
take g;
thus g.0 = f by A2;
let i be Nat;
R[i,g.i,g.(i+1)] by A2;
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be Functional_Sequence of the carrier of V,the carrier of W;
assume that
A3: seq1.0 = f and
A4: for n be Nat holds seq1.(n+1) = fD(seq1.n,h) and
A5: seq2.0 = f and
A6: for n be Nat holds seq2.(n+1) = fD(seq2.n,h);
defpred P[Nat] means seq1.$1 = seq2.$1;
A7: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A8: P[k];
thus seq1.(k+1) = fD(seq1.k,h) by A4
.= seq2.(k+1) by A6,A8;
end;
A9: P[0] by A3,A5;
for n be Nat holds P[n] from NAT_1:sch 2(A9,A7);
then for n being Element of NAT holds P[n];
hence seq1 = seq2 by FUNCT_2:63;
end;
end;
notation
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
synonym fdif(f,h) for forward_difference(f,h);
end;
reserve F,G for Field,
V for VectSp of F,
W for VectSp of G;
reserve f,f1,f2 for Function of V, W;
reserve x,h for Element of V;
reserve r,r1,r2 for Element of G;
theorem Th01:
for f being PartFunc of V, W st x in dom f & x + h in dom f holds
fD(f,h)/.x = f/.(x+h) - f/.x
proof
let f be PartFunc of V, W;
assume
A1: x in dom f & x + h in dom f;
A2: dom Shift(f,h) = -h ++ dom f by Def1;
(-h) + (x+h) = x + (h+(-h)) by RLVECT_1:def 3
.= x + 0.V by VECTSP_1:16
.= x by RLVECT_1:def 4; then
A4: x in (-h) ++ dom f by A1;
A5: Shift(f,h)/.x = Shift(f,h).x by A2,A4,PARTFUN1:def 6
.= f.(x+h) by Def1,A4
.= f/.(x+h) by A1,PARTFUN1:def 6;
x in (dom Shift(f,h)) /\ dom f by A4,A2,A1,XBOOLE_0:def 4;
then x in dom fD(f,h) by VFUNCT_1:def 2;
hence fD(f,h)/.x = f/.(x+h) - f/.x by A5,VFUNCT_1:def 2;
end;
theorem Th2:
for n be Nat holds
fdif(f,h).n is Function of V, W
proof
defpred X[Nat] means fdif(f,h).$1 is Function of V,W;
A1: for k be Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume fdif(f,h).k is Function of V,W;
then fD(fdif(f,h).k,h) is Function of V,W;
hence thesis by Def6;
end;
A2: X[0] by Def6;
for n be Nat holds X[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th3:
fD(f,h)/.x = f/.(x+h) - f/.x
proof
dom f = the carrier of V by FUNCT_2:def 1;
hence fD(f,h)/.x = f/.(x+h) - f/.x by Th01;
end;
theorem Th4:
bD(f,h)/.x = f/.x - f/.(x-h)
proof
P1:dom f = the carrier of V by FUNCT_2:def 1;
dom Shift(f,-h) = the carrier of V by FUNCT_2:def 1;
then x in (dom f) /\ (dom Shift(f,-h)) by P1; then
P2: x in dom (f - Shift(f,-h)) by VFUNCT_1:def 2;
thus bD(f,h)/.x = f/.x - (Shift(f,-h))/.x by P2, VFUNCT_1:def 2
.= f/.x - f/.(x-h) by Def2;
end;
theorem Th5:
cD(f,h)/.x = f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h)
proof
dom (Shift(f,(2*1.F)"*h) - Shift(f,-(2*1.F)"*h))
= the carrier of V by FUNCT_2:def 1;
hence cD(f,h)/.x = Shift(f,(2*1.F)"*h)/.x - Shift(f,-(2*1.F)"*h)/.x
by VFUNCT_1:def 2
.= f/.(x+(2*1.F)"*h) - Shift(f,-(2*1.F)"*h)/.x by Def2
.= f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h) by Def2;
end;
reserve n,m,k for Nat;
theorem
f is constant implies for x holds fdif(f,h).(n+1)/.x = 0.W
proof
assume
A1: f is constant;
A2: for x holds f/.(x+h) - f/.x = 0.W
proof
let x;
x + h in the carrier of V; then
A3: x + h in dom f by FUNCT_2:def 1;
x in the carrier of V;
then x in dom f by FUNCT_2:def 1;
then f/.x = f/.(x+h) by A1,A3,FUNCT_1:def 10;
hence thesis by RLVECT_1:15;
end;
for x holds fdif(f,h).(n+1)/.x = 0.W
proof
defpred X[Nat] means for x holds fdif(f,h).($1+1)/.x = 0.W;
A4: for k st X[k] holds X[k+1]
proof
let k;
assume
A5: for x holds fdif(f,h).(k+1)/.x = 0.W;
let x;
A6: fdif(f,h).(k+1)/.(x+h) = 0.W by A5;
reconsider fdk = fdif(f,h).(k+1) as Function of V,W by Th2;
(fdif(f,h).(k+2))/.x = (fdif(f,h).(k+1+1))/.x
.= fD(fdif(f,h).(k+1),h)/.x by Def6
.= fdk/.(x+h) - fdk/.x by Th3
.= 0.W - 0.W by A5,A6
.= 0.W by RLVECT_1:15;
hence thesis;
end;
A8: X[0]
proof
let x;
thus fdif(f,h).(0+1)/.x = fD(fdif(f,h).0,h)/.x by Def6
.= fD(f,h)/.x by Def6
.= f/.(x+h) - f/.x by Th3
.= 0.W by A2;
end;
for n holds X[n] from NAT_1:sch 2(A8,A4);
hence thesis;
end;
hence thesis;
end;
theorem Th7:
fdif(r(#)f,h).(n+1)/.x = r* fdif(f,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds fdif(r(#)f,h).($1+1)/.x = r*fdif(f,h).($1+1)/.x;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds fdif(r(#)f,h).(k+1)/.x = r* fdif(f,h).(k+1)/.x;
let x;
A3: fdif(r(#)f,h).(k+1)/.x = r * fdif(f,h).(k+1)/.x &
fdif(r(#)f,h).(k+1)/.(x+h) = r * fdif(f,h).(k+1)/.(x+h) by A2;
reconsider rfdk = fdif(r(#)f,h).(k+1) as Function of V,W by Th2;
reconsider fdk = fdif(f,h).(k+1) as Function of V,W by Th2;
fdif(r(#)f,h).(k+1+1)/.x = fD(fdif(r(#)f,h).(k+1),h)/.x by Def6
.= rfdk/.(x+h) - rfdk/.x by Th3
.= r * (fdk/.(x+h) - fdk/.x) by VECTSP_1:23,A3
.= r * fD(fdk,h)/.x by Th3
.= r * fdif(f,h).(k+1+1)/.x by Def6;
hence thesis;
end;
A6: X[0]
proof
let x;
x in the carrier of V; then
A7: x in dom (r(#)f) by FUNCT_2:def 1;
x + h in the carrier of V; then
A8: x + h in dom (r(#)f) by FUNCT_2:def 1;
fdif(r(#)f,h).(0+1)/.x = fD(fdif(r(#)f,h).0,h)/.x by Def6
.= fD(r(#)f,h)/.x by Def6
.= (r(#)f)/.(x+h) - (r(#)f)/.x by Th3
.= r * f/.(x+h) - (r(#)f)/.x by A8,Def4X
.= r * f/.(x+h) - r * f/.x by A7,Def4X
.= r * (f/.(x+h) - f/.x) by VECTSP_1:23
.= r * fD(f,h)/.x by Th3
.= r * fD(fdif(f,h).0,h)/.x by Def6
.= r * fdif(f,h).(0+1)/.x by Def6;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
theorem Th8:
fdif(f1+f2,h).(n+1)/.x = fdif(f1,h).(n+1)/.x + fdif(f2,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds fdif(f1+f2,h).($1+1)/.x = fdif(f1,h).($1+1)/.x
+ fdif(f2,h).($1+1)/.x;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds
fdif(f1+f2,h).(k+1)/.x = fdif(f1,h).(k+1)/.x + fdif(f2,h).(k+1)/.x;
let x;
A3: fdif(f1+f2,h).(k+1)/.x = fdif(f1,h).(k+1)/.x + fdif(f2,h).(k+1)/.x &
fdif(f1+f2,h).(k+1)/.(x+h)
= fdif(f1,h).(k+1)/.(x+h) + fdif(f2,h).(k+1)/.(x + h) by A2;
reconsider fdiff12 = fdif(f1+f2,h).(k+1) as Function of V,W by Th2;
reconsider fdiff2 = fdif(f2,h).(k+1) as Function of V,W by Th2;
reconsider fdiff1 = fdif(f1,h).(k+1) as Function of V,W by Th2;
A6: fD(fdif(f1,h).(k+1),h)/.x = fD(fdiff1,h)/.x
.= fdif(f1,h).(k+1)/.(x+h) - fdif(f1,h).(k+1)/.x by Th3;
A7: fD(fdif(f2,h).(k+1),h)/.x = fD(fdiff2,h)/.x
.= fdif(f2,h).(k+1)/.(x+h) - fdif(f2,h).(k+1)/.x by Th3;
fdif(f1+f2,h).(k+1+1)/.x = fD(fdif(f1+f2,h).(k+1),h)/.x by Def6
.= fdiff12/.(x+h) - fdiff12/.x by Th3
.= fdif(f1,h).(k+1)/.(x+h) + fdif(f2,h).(k+1)/.(x+h)
- fdif(f2,h).(k+1)/.x - fdif(f1,h).(k+1)/.x by RLVECT_1:27,A3
.= fdif(f1,h).(k+1)/.(x+h) + (fdif(f2,h).(k+1)/.(x+h)
- fdif(f2,h).(k+1)/.x) - fdif(f1,h).(k+1)/.x by RLVECT_1:28
.= (fdif(f2,h).(k+1)/.(x+h) - fdif(f2,h).(k+1)/.x)
+ (fdif(f1,h).(k+1)/.(x+h)- fdif(f1,h).(k+1)/.x) by RLVECT_1:28
.= fdif(f1,h).(k+1+1)/.x + fD(fdif(f2,h).(k+1),h)/.x by Def6,A6,A7
.= fdif(f1,h).(k+1+1)/.x + fdif(f2,h).(k+1+1)/.x by Def6;
hence thesis;
end;
B1: dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1
.= (the carrier of V) /\ dom f2 by FUNCT_2:def 1
.= (the carrier of V) /\ (the carrier of V) by FUNCT_2:def 1
.= the carrier of V;
A7: X[0]
proof
let x;
fdif(f1+f2,h).(0+1)/.x = fD(fdif(f1+f2,h).0,h)/.x by Def6
.= fD(f1+f2,h)/.x by Def6
.= (f1+f2)/.(x+h) - (f1+f2)/.x by Th3
.= f1/.(x+h) + f2/.(x+h) - (f1+f2)/.x by B1,VFUNCT_1:def 1
.= f1/.(x+h) + f2/.(x+h) - (f1/.x + f2/.x) by B1,VFUNCT_1:def 1
.= (f1/.(x+h) + f2/.(x+h) - f2/.x) - f1/.x by RLVECT_1:27
.= (f1/.(x+h) + (f2/.(x+h) - f2/.x)) - f1/.x by RLVECT_1:28
.= (f2/.(x+h) - f2/.x) + (f1/.(x+h) - f1/.x) by RLVECT_1:28
.= fD(f1,h)/.x + (f2/.(x+h) - f2/.x) by Th3
.= fD(f1,h)/.x + fD(f2,h)/.x by Th3
.= fD(fdif(f1,h).0,h)/.x + fD(f2,h)/.x by Def6
.= fD(fdif(f1,h).0,h)/.x + fD(fdif(f2,h).0,h)/.x by Def6
.= fdif(f1,h).(0+1)/.x + fD(fdif(f2,h).0,h)/.x by Def6
.= fdif(f1,h).(0+1)/.x + fdif(f2,h).(0+1)/.x by Def6;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem
fdif(f1-f2,h).(n+1)/.x = fdif(f1,h).(n+1)/.x - fdif(f2,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds fdif(f1-f2,h).($1+1)/.x = fdif(f1,h).($1+1)/.x
- fdif(f2,h).($1+1)/.x;
A1: X[0]
proof
let x;
x in the carrier of V;
then x in dom f1 & x in dom f2 by FUNCT_2:def 1;
then x in dom f1 /\ dom f2 by XBOOLE_0:def 4; then
A2: x in dom (f1-f2) by VFUNCT_1:def 2;
x + h in the carrier of V;
then x + h in dom f1 & x + h in dom f2 by FUNCT_2:def 1;
then x + h in dom f1 /\ dom f2 by XBOOLE_0:def 4; then
A3: x + h in dom (f1-f2) by VFUNCT_1:def 2;
fdif(f1-f2,h).(0+1)/.x = fD(fdif(f1-f2,h).0,h)/.x by Def6
.= fD(f1-f2,h)/.x by Def6
.= (f1-f2)/.(x+h) - (f1-f2)/.x by Th3
.= f1/.(x+h) - f2/.(x+h) - (f1-f2)/.x by A3,VFUNCT_1:def 2
.= f1/.(x+h) - f2/.(x+h) - (f1/.x - f2/.x) by A2,VFUNCT_1:def 2
.= (f1/.(x+h) - f2/.(x+h) - f1/.x) + f2/.x by RLVECT_1:29
.= (f1/.(x+h) - (f1/.x + f2/.(x+h))) + f2/.x by RLVECT_1:27
.= ((f1/.(x+h) - f1/.x) - f2/.(x+h)) + f2/.x by RLVECT_1:27
.= ((fD(f1,h)/.x) - f2/.(x+h)) + f2/.x by Th3
.= fD(f1,h).x - (f2/.(x+h) - f2/.x) by RLVECT_1:29
.= fD(f1,h)/.x - fD(f2,h)/.x by Th3
.= fD(fdif(f1,h).0,h)/.x - fD(f2,h)/.x by Def6
.= fD(fdif(f1,h).0,h)/.x - fD(fdif(f2,h).0,h)/.x by Def6
.= fdif(f1,h).(0+1)/.x - fD(fdif(f2,h).0,h)/.x by Def6
.= fdif(f1,h).(0+1)/.x - fdif(f2,h).(0+1)/.x by Def6;
hence thesis;
end;
A4: for k st X[k] holds X[k+1]
proof
let k;
assume
A5: for x holds
fdif(f1-f2,h).(k+1)/.x = fdif(f1,h).(k+1)/.x - fdif(f2,h).(k+1)/.x;
let x;
A6: fdif(f1-f2,h).(k+1)/.x = fdif(f1,h).(k+1)/.x - fdif(f2,h).(k+1)/.x &
fdif(f1-f2,h).(k+1)/.(x+h)
= fdif(f1,h).(k+1)/.(x+h) - fdif(f2,h).(k+1)/.(x+h) by A5;
reconsider fd12k1 = fdif(f1-f2,h).(k+1) as Function of V, W by Th2;
reconsider fd2k = fdif(f2,h).(k+1) as Function of V,W by Th2;
reconsider fd1k = fdif(f1,h).(k+1) as Function of V, W by Th2;
reconsider fdiff12 = fdif(f1-f2,h).(k+1) as Function of V, W by Th2;
reconsider fdiff2 = fdif(f2,h).(k+1) as Function of V, W by Th2;
reconsider fdiff1 = fdif(f1,h).(k+1) as Function of V, W by Th2;
A12: fD(fdif(f1,h).(k+1),h)/.x = fD(fdiff1,h)/.x
.= fdif(f1,h).(k+1)/.(x+h) - fdif(f1,h).(k+1)/.x by Th3;
A13: fD(fdif(f2,h).(k+1),h)/.x = fD(fdiff2,h)/.x
.= fdif(f2,h).(k+1)/.(x+h) - fdif(f2,h).(k+1)/.x by Th3;
fdif(f1-f2,h).(k+1+1)/.x = fD(fdif(f1-f2,h).(k+1),h)/.x by Def6
.= fd12k1/.(x+h) - fd12k1/.x by Th3
.= (fdif(f1,h).(k+1)/.(x+h) + (-fdif(f2,h).(k+1)/.(x+h))
- fdif(f1,h).(k+1)/.x) + fdif(f2,h).(k+1)/.x by RLVECT_1:29,A6
.= (fdif(f1,h).(k+1)/.(x+h) + ((-fdif(f2,h).(k+1)/.(x+h))
+(-fdif(f1,h).(k+1)/.x))) + fdif(f2,h).(k+1)/.x by RLVECT_1:def 3
.= (fdif(f1,h).(k+1)/.(x+h) + ((-fdif(f1,h).(k+1)/.x))
- fdif(f2,h).(k+1)/.(x+h)) + fdif(f2,h).(k+1)/.x by RLVECT_1:def 3
.= fD(fdif(f1,h).(k+1),h)/.x - (fdif(f2,h).(k+1)/.(x+h)
- fdif(f2,h).(k+1)/.x) by A12,RLVECT_1:29
.= fdif(f1,h).(k+1+1)/.x - fD(fdif(f2,h).(k+1),h)/.x by Def6,A13
.= fdif(f1,h).(k+1+1)/.x - fdif(f2,h).(k+1+1)/.x by Def6;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A1,A4);
hence thesis;
end;
theorem
fdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= r1 * (fdif(f1,h).(n+1)/.x) + r2 * (fdif(f2,h).(n+1)/.x)
proof
set g1 = r1(#)f1;
set g2 = r2(#)f2;
reconsider g1n1 = fdif(g1,h).(n+1) as Function of V, W by Th2;
reconsider g2n1 = fdif(g2,h).(n+1) as Function of V, W by Th2;
fdif(r1(#)f1+r2(#)f2,h).(n+1)/.x = fdif(g1,h).(n+1)/.x + fdif(g2,h).(n+1)/.x
by Th8
.= r1 * (fdif(f1,h).(n+1)/.x) + fdif(g2,h).(n+1)/.x by Th7
.= r1 * (fdif(f1,h).(n+1)/.x) + r2 * (fdif(f2,h).(n+1)/.x) by Th7;
hence thesis;
end;
theorem
(fdif(f,h).1)/.x = Shift(f,h)/.x - f/.x
proof
set f1 = Shift(f,h);
(fdif(f,h).1)/.x = fdif(f,h).(0+1)/.x
.= fD(fdif(f,h).0,h)/.x by Def6
.= fD(f,h)/.x by Def6
.= f/.(x+h) - f/.x by Th3
.= f1/.x - f/.x by Def2;
hence thesis;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
func backward_difference(f,h) ->
Functional_Sequence of the carrier of V,the carrier of W means
it.0 = f & for n being Nat holds it.(n+1) = bD(it.n,h);
existence
proof
reconsider fZ = f as Element of PFuncs(the carrier of V,the carrier of W)
by PARTFUN1:45;
defpred R[set,set,set] means ex g being PartFunc of V,W
st $2 = g & $3 = bD(g,h);
A1: for n being Nat for x being Element of PFuncs(the carrier of V,
the carrier of W) ex y being Element of PFuncs(the carrier of V,
the carrier of W) st R[n,x,y]
proof
let n be Nat;
let x be Element of PFuncs (the carrier of V,the carrier of W);
reconsider x9 = x as PartFunc of V,W by PARTFUN1:46;
reconsider y = bD(x9,h) as Element of PFuncs (the carrier of V,
the carrier of W) by PARTFUN1:45;
ex w being PartFunc of V,W st x = w & y = bD(w,h);
hence thesis;
end;
consider g be sequence of PFuncs (the carrier of V,the carrier of W)
such that
A2: g.0 = fZ & for n being Nat holds R[n,g.n,g.(n+1)] from RECDEF_1:sch 2(A1);
reconsider g as Functional_Sequence of the carrier of V,the carrier of W;
take g;
thus g.0 = f by A2;
let i be Nat;
R[i,g.i,g.(i+1)] by A2;
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be Functional_Sequence of the carrier of V,
the carrier of W;
assume that
A3: seq1.0 = f and
A4: for n be Nat holds seq1.(n+1) = bD(seq1.n,h) and
A5: seq2.0 = f and
A6: for n be Nat holds seq2.(n+1) = bD(seq2.n,h);
defpred P[Nat] means seq1.$1 = seq2.$1;
A7: for k st P[k] holds P[k+1]
proof
let k;
assume
A8: P[k];
thus seq1.(k+1) = bD(seq1.k,h) by A4
.= seq2.(k+1) by A6,A8;
end;
A9: P[0] by A3,A5;
for n holds P[n] from NAT_1:sch 2(A9,A7);
then for n being Element of NAT holds P[n];
hence seq1 = seq2 by FUNCT_2:63;
end;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
func backward_difference(f,h) ->
Functional_Sequence of the carrier of V,the carrier of W means
:Def7:
it.0 = f & for n being Nat holds it.(n+1) = bD(it.n,h);
existence
proof
reconsider fZ = f as Element of PFuncs ((the carrier of V),
(the carrier of W)) by PARTFUN1:45;
defpred R[set,set,set] means ex g being PartFunc of V,W st $2 = g &
$3 = bD(g,h);
A1: for n being Nat for x being Element of PFuncs((the carrier of V),
(the carrier of W)) ex y being Element of PFuncs((the carrier of V),
(the carrier of W)) st R[n,x,y]
proof
let n be Nat;
let x be Element of PFuncs ((the carrier of V),(the carrier of W));
reconsider x9 = x as PartFunc of V,W by PARTFUN1:46;
reconsider y = bD(x9,h) as Element of PFuncs((the carrier of V),
(the carrier of W)) by PARTFUN1:45;
ex w being PartFunc of V,W st x = w &
y = bD(w,h);
hence thesis;
end;
consider g be sequence of PFuncs((the carrier of V),(the carrier of W))
such that
A2: g.0 = fZ & for n being Nat holds R[n,g.n,g.(n+1)] from
RECDEF_1:sch 2(A1);
reconsider g as Functional_Sequence of the carrier of V,
the carrier of W;
take g;
thus g.0 = f by A2;
let i be Nat;
R[i,g.i,g.(i+1)] by A2;
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be Functional_Sequence of the carrier of V,
the carrier of W;
assume that
A3: seq1.0 = f and
A4: for n be Nat holds seq1.(n+1) = bD(seq1.n,h) and
A5: seq2.0 = f and
A6: for n be Nat holds seq2.(n+1) = bD(seq2.n,h);
defpred P[Nat] means seq1.$1 = seq2.$1;
A7: for k st P[k] holds P[k+1]
proof
let k;
assume
A8: P[k];
thus seq1.(k+1) = bD(seq1.k,h) by A4
.= seq2.(k+1) by A6,A8;
end;
A9: P[0] by A3,A5;
for n holds P[n] from NAT_1:sch 2(A9,A7);
then for n being Element of NAT holds P[n];
hence seq1 = seq2 by FUNCT_2:63;
end;
end;
notation
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be Function of V,W;
synonym bdif(f,h) for backward_difference(f,h);
end;
theorem Th12:
for n be Nat holds
bdif(f,h).n is Function of V,W
proof
defpred X[Nat] means bdif(f,h).$1 is Function of V,W;
A1: for k be Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume bdif(f,h).k is Function of V,W;
then bD(bdif(f,h).k,h) is Function of V, W;
hence thesis by Def7;
end;
A2: X[0] by Def7;
for n be Nat holds X[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
f is constant implies for x holds bdif(f,h).(n+1)/.x = 0.W
proof
assume
A1: f is constant;
A2: for x holds f/.x - f/.(x-h) = 0.W
proof
let x;
x - h in the carrier of V; then
A3: x - h in dom f by FUNCT_2:def 1;
x in the carrier of V;
then x in dom f by FUNCT_2:def 1;
then f/.x = f/.(x-h) by A1,A3,FUNCT_1:def 10;
hence thesis by RLVECT_1:15;
end;
for x holds bdif(f,h).(n+1)/.x = 0.W
proof
defpred X[Nat] means for x holds bdif(f,h).($1+1)/.x = 0.W;
A4: for k st X[k] holds X[k+1]
proof
let k;
assume
A5: for x holds bdif(f,h).(k+1)/.x = 0.W;
let x;
A6: bdif(f,h).(k+1)/.(x-h) = 0.W by A5;
A7: bdif(f,h).(k+1) is Function of V,W by Th12;
(bdif(f,h).(k+2))/.x = (bdif(f,h).(k+1+1))/.x
.= bD(bdif(f,h).(k+1),h)/.x by Def7
.= bdif(f,h).(k+1)/.x - bdif(f,h).(k+1)/.(x-h) by A7,Th4
.= 0.W - 0.W by A5,A6
.= 0.W by RLVECT_1:15;
hence thesis;
end;
A8: X[0]
proof
let x;
thus bdif(f,h).(0+1)/.x = bD(bdif(f,h).0,h)/.x by Def7
.= bD(f,h)/.x by Def7
.= f/.x - f/.(x-h) by Th4
.= 0.W by A2;
end;
for n holds X[n] from NAT_1:sch 2(A8,A4);
hence thesis;
end;
hence thesis;
end;
theorem Th14:
bdif(r(#)f,h).(n+1)/.x = r * bdif(f,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds bdif(r(#)f,h).($1+1)/.x = r * bdif(f,h).($1+1)/.x;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds bdif(r(#)f,h).(k+1)/.x = r * bdif(f,h).(k+1)/.x;
let x;
A3: bdif(r(#)f,h).(k+1)/.x = r * bdif(f,h).(k+1)/.x &
bdif(r(#)f,h).(k+1)/.(x-h) = r * bdif(f,h).(k+1)/.(x-h) by A2;
A4: bdif(r(#)f,h).(k+1) is Function of V,W by Th12;
A5: bdif(f,h).(k+1) is Function of V,W by Th12;
bdif(r(#)f,h).(k+1+1)/.x = bD(bdif(r(#)f,h).(k+1),h)/.x by Def7
.= bdif(r(#)f,h).(k+1)/.x - bdif(r(#)f,h).(k+1)/.(x-h) by A4,Th4
.= r * (bdif(f,h).(k+1)/.x - bdif(f,h).(k+1)/.(x-h)) by VECTSP_1:23,A3
.= r * bD(bdif(f,h).(k+1),h)/.x by A5,Th4
.= r * bdif(f,h).(k+1+1)/.x by Def7;
hence thesis;
end;
A6: X[0]
proof
let x;
x in the carrier of V;
then
A7: x in dom (r(#)f) by FUNCT_2:def 1;
x - h in the carrier of V;
then
A8: x - h in dom (r(#)f) by FUNCT_2:def 1;
bdif(r(#)f,h).(0+1)/.x = bD(bdif(r(#)f,h).0,h)/.x by Def7
.= bD(r(#)f,h)/.x by Def7
.= (r(#)f)/.x - (r(#)f)/.(x-h) by Th4
.= (r(#)f)/.x - r * f/.(x-h) by A8,Def4X
.= r * f/.x - r * f/.(x-h) by A7,Def4X
.= r * (f/.x - f/.(x-h)) by VECTSP_1:23
.= r * bD(f,h)/.x by Th4
.= r * bD(bdif(f,h).0,h)/.x by Def7
.= r * bdif(f,h).(0+1)/.x by Def7;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
theorem Th15:
bdif(f1+f2,h).(n+1)/.x = bdif(f1,h).(n+1)/.x + bdif(f2,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds bdif(f1+f2,h).($1+1)/.x = bdif(f1,h).($1+1)/.x
+ bdif(f2,h).($1+1)/.x;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds
bdif(f1+f2,h).(k+1)/.x = bdif(f1,h).(k+1)/.x + bdif(f2,h).(k+1)/.x;
let x;
A3: bdif(f1+f2,h).(k+1)/.x = bdif(f1,h).(k+1)/.x + bdif(f2,h).(k+1)/.x &
bdif(f1+f2,h).(k+1)/.(x-h)
= bdif(f1,h).(k+1)/.(x-h) + bdif(f2,h).(k+1)/.(x-h) by A2;
A4: bdif(f1+f2,h).(k+1) is Function of V,W by Th12;
A5: bdif(f2,h).(k+1) is Function of V, W by Th12;
A6: bdif(f1,h).(k+1) is Function of V, W by Th12;
bdif(f1+f2,h).(k+1+1)/.x = bD(bdif(f1+f2,h).(k+1),h)/.x by Def7
.= bdif(f1+f2,h).(k+1)/.x - bdif(f1+f2,h).(k+1)/.(x-h) by A4,Th4
.= (bdif(f2,h).(k+1)/.x + bdif(f1,h).(k+1)/.x - bdif(f1,h).(k+1)/.(x-h))
- bdif(f2,h).(k+1)/.(x-h) by RLVECT_1:27,A3
.= (bdif(f2,h).(k+1)/.x + (bdif(f1,h).(k+1)/.x - bdif(f1,h).(k+1)/.(x-h)))
- bdif(f2,h).(k+1)/.(x-h) by RLVECT_1:28
.= (bdif(f1,h).(k+1)/.x - bdif(f1,h).(k+1)/.(x-h)) + (bdif(f2,h).(k+1)/.x
- bdif(f2,h).(k+1)/.(x-h)) by RLVECT_1:28
.= bD(bdif(f1,h).(k+1),h)/.x + (bdif(f2,h).(k+1)/.x
- bdif(f2,h).(k+1)/.(x-h)) by A6,Th4
.= bD(bdif(f1,h).(k+1),h)/.x + bD(bdif(f2,h).(k+1),h)/.x by A5,Th4
.= bdif(f1,h).(k+1+1)/.x + bD(bdif(f2,h).(k+1),h)/.x by Def7
.= bdif(f1,h).(k+1+1)/.x + bdif(f2,h).(k+1+1)/.x by Def7;
hence thesis;
end;
A7: X[0]
proof
let x;
reconsider xx = x, h as Element of V;
B0: dom (f1+f2)= dom f1 /\ dom f2 by VFUNCT_1:def 1
.= (the carrier of V) /\ dom f2 by FUNCT_2:def 1
.= (the carrier of V) /\ (the carrier of V) by FUNCT_2:def 1
.= the carrier of V;
bdif(f1+f2,h).(0+1)/.x = bD(bdif(f1+f2,h).0,h)/.x by Def7
.= bD(f1+f2,h)/.x by Def7
.= (f1+f2)/.x - (f1+f2)/.(x-h) by Th4
.= f1/.xx + f2/.xx - (f1+f2)/.(xx-h) by B0, VFUNCT_1:def 1
.= (f1/.x + f2/.x) - (f1/.(x-h) + f2/.(x-h)) by B0,VFUNCT_1:def 1
.= ((f1/.x + f2/.x) - f1/.(x-h)) - f2/.(x-h) by RLVECT_1:27
.= (f2/.x + (f1/.x - f1/.(x-h))) - f2/.(x-h) by RLVECT_1:28
.= (f1/.x - f1/.(x-h)) + (f2/.x - f2/.(x-h)) by RLVECT_1:28
.= bD(f1,h)/.x + (f2/.x - f2/.(x-h)) by Th4
.= bD(f1,h)/.x + bD(f2,h)/.x by Th4
.= bD(bdif(f1,h).0,h)/.x + bD(f2,h)/.x by Def7
.= bD(bdif(f1,h).0,h)/.x + bD(bdif(f2,h).0,h)/.x by Def7
.= bdif(f1,h).(0+1)/.x + bD(bdif(f2,h).0,h)/.x by Def7
.= bdif(f1,h).(0+1)/.x + bdif(f2,h).(0+1)/.x by Def7;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem
bdif(f1-f2,h).(n+1)/.x = bdif(f1,h).(n+1)/.x - bdif(f2,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds bdif(f1-f2,h).($1+1)/.x = bdif(f1,h).($1+1)/.x
- bdif(f2,h).($1+1)/.x;
A1: X[0]
proof
let x;
x in the carrier of V;
then x in dom f1 & x in dom f2 by FUNCT_2:def 1;
then x in dom f1 /\ dom f2 by XBOOLE_0:def 4;
then
A2: x in dom (f1-f2) by VFUNCT_1:def 2;
x - h in the carrier of V;
then x - h in dom f1 & x - h in dom f2 by FUNCT_2:def 1;
then x - h in dom f1 /\ dom f2 by XBOOLE_0:def 4;
then
A3: x - h in dom (f1-f2) by VFUNCT_1:def 2;
bdif(f1-f2,h).(0+1)/.x = bD(bdif(f1-f2,h).0,h)/.x by Def7
.= bD(f1-f2,h)/.x by Def7
.= (f1-f2)/.x - (f1-f2)/.(x-h) by Th4
.= f1/.x - f2/.x - (f1-f2)/.(x-h) by A2,VFUNCT_1:def 2
.= (f1/.x - f2/.x) - (f1/.(x-h) - f2/.(x-h)) by A3,VFUNCT_1:def 2
.= (f1/.x - f2/.x - f1/.(x-h)) + f2/.(x-h) by RLVECT_1:29
.= (f1/.x - (f1/.(x-h) + f2/.x)) + f2/.(x-h) by RLVECT_1:27
.= ((f1/.x - f1/.(x-h)) - f2/.x) + f2/.(x-h) by RLVECT_1:27
.= (f1/.x - f1/.(x-h)) -(f2/.x - f2/.(x-h)) by RLVECT_1:29
.= bD(f1,h)/.x - (f2/.x - f2/.(x-h)) by Th4
.= bD(f1,h)/.x - bD(f2,h)/.x by Th4
.= bD(bdif(f1,h).0,h)/.x - bD(f2,h)/.x by Def7
.= bD(bdif(f1,h).0,h)/.x - bD(bdif(f2,h).0,h)/.x by Def7
.= bdif(f1,h).(0+1)/.x - bD(bdif(f2,h).0,h)/.x by Def7
.= bdif(f1,h).(0+1)/.x - bdif(f2,h).(0+1)/.x by Def7;
hence thesis;
end;
A4: for k st X[k] holds X[k+1]
proof
let k;
assume
A5: for x holds
bdif(f1-f2,h).(k+1)/.x = bdif(f1,h).(k+1)/.x - bdif(f2,h).(k+1)/.x;
let x;
A6: bdif(f1-f2,h).(k+1)/.x = bdif(f1,h).(k+1)/.x - bdif(f2,h).(k+1)/.x &
bdif(f1-f2,h).(k+1)/.(x-h)
= bdif(f1,h).(k+1)/.(x-h) - bdif(f2,h).(k+1)/.(x-h) by A5;
A7: bdif(f1-f2,h).(k+1) is Function of V,W by Th12;
A8: bdif(f2,h).(k+1) is Function of V,W by Th12;
A9: bdif(f1,h).(k+1) is Function of V,W by Th12;
bdif(f1-f2,h).(k+1+1)/.x = bD(bdif(f1-f2,h).(k+1),h)/.x by Def7
.= bdif(f1-f2,h).(k+1)/.x - bdif(f1-f2,h).(k+1)/.(x-h) by A7,Th4
.= (bdif(f1,h).(k+1)/.x - bdif(f2,h).(k+1)/.x - bdif(f1,h).(k+1)/.(x-h))
+ bdif(f2,h).(k+1)/.(x-h) by RLVECT_1:29,A6
.= (bdif(f1,h).(k+1)/.x - (bdif(f1,h).(k+1)/.(x-h) + bdif(f2,h).(k+1)/.x))
+ bdif(f2,h).(k+1)/.(x-h) by RLVECT_1:27
.= ((bdif(f1,h).(k+1)/.x - bdif(f1,h).(k+1)/.(x-h)) - bdif(f2,h).(k+1)/.x)
+ bdif(f2,h).(k+1)/.(x-h) by RLVECT_1:27
.= (bdif(f1,h).(k+1)/.x - bdif(f1,h).(k+1)/.(x-h)) - (bdif(f2,h).(k+1)/.x
- bdif(f2,h).(k+1)/.(x-h)) by RLVECT_1:29
.= bD(bdif(f1,h).(k+1),h)/.x - (bdif(f2,h).(k+1)/.x
- bdif(f2,h).(k+1)/.(x-h)) by A9,Th4
.= bD(bdif(f1,h).(k+1),h)/.x - bD(bdif(f2,h).(k+1),h)/.x by A8,Th4
.= bdif(f1,h).(k+1+1)/.x - bD(bdif(f2,h).(k+1),h)/.x by Def7
.= bdif(f1,h).(k+1+1)/.x - bdif(f2,h).(k+1+1)/.x by Def7;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A1,A4);
hence thesis;
end;
theorem
bdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= r1 * bdif(f1,h).(n+1)/.x + r2 * bdif(f2,h).(n+1)/.x
proof
set g1 = r1(#)f1;
set g2 = r2(#)f2;
bdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= bdif(g1,h).(n+1)/.x + bdif(g2,h).(n+1)/.x by Th15
.= r1 * bdif(f1,h).(n+1)/.x + bdif(g2,h).(n+1)/.x by Th14
.= r1 * bdif(f1,h).(n+1)/.x + r2 * bdif(f2,h).(n+1)/.x by Th14;
hence thesis;
end;
theorem
(bdif(f,h).1)/.x = f/.x - Shift(f,-h)/.x
proof
set f2 = Shift(f,-h);
(bdif(f,h).1)/.x = bdif(f,h).(0+1)/.x
.= bD(bdif(f,h).0,h)/.x by Def7
.= bD(f,h)/.x by Def7
.= f/.x - f/.(x-h) by Th4
.= f/.x - f2/.x by Def2;
hence thesis;
end;
definition
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be PartFunc of V,W;
func central_difference(f,h) ->
Functional_Sequence of (the carrier of V),(the carrier of W) means
:Def8:
it.0 = f & for n be Nat holds it.(n+1) = cD(it.n,h);
existence
proof
reconsider fZ = f as Element of PFuncs((the carrier of V),
(the carrier of W)) by PARTFUN1:45;
defpred R[set,set,set] means ex g being PartFunc of V,W st $2 = g &
$3 = cD(g,h);
A1: for n being Nat
for x being Element of PFuncs((the carrier of V),(the carrier of W))
ex y being Element of PFuncs((the carrier of V),(the carrier of W))
st R[n,x,y]
proof
let n be Nat;
let x be Element of PFuncs((the carrier of V),(the carrier of W));
reconsider x9 = x as PartFunc of V,W by PARTFUN1:46;
reconsider y = cD(x9,h) as Element of PFuncs((the carrier of V),
(the carrier of W)) by PARTFUN1:45;
ex w being PartFunc of V,W st x = w & y = cD(w,h);
hence thesis;
end;
consider g be sequence of PFuncs ((the carrier of V),(the carrier of W))
such that
A2: g.0 = fZ & for n being Nat holds R[n,g.n,g.(n+1)] from RECDEF_1:sch 2(A1);
reconsider g as Functional_Sequence of (the carrier of V),
(the carrier of W);
take g;
thus g.0 = f by A2;
let i be Nat;
R[i,g.i,g.(i+1)] by A2;
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be Functional_Sequence of (the carrier of V),
the carrier of W;
assume that
A3: seq1.0 = f and
A4: for n be Nat holds seq1.(n+1) = cD(seq1.n,h) and
A5: seq2.0 = f and
A6: for n be Nat holds seq2.(n+1) = cD(seq2.n,h);
defpred P[Nat] means seq1.$1 = seq2.$1;
A7: for k st P[k] holds P[k+1]
proof
let k;
assume
A8: P[k];
thus seq1.(k+1) = cD(seq1.k,h) by A4
.= seq2.(k+1) by A6,A8;
end;
A9: P[0] by A3,A5;
for n holds P[n] from NAT_1:sch 2(A9,A7);
then for n being Element of NAT holds P[n];
hence seq1 = seq2 by FUNCT_2:63;
end;
end;
notation
let F,G be Field;
let V be VectSp of F;
let h be Element of V;
let W be VectSp of G;
let f be PartFunc of V,W;
synonym cdif(f,h) for central_difference(f,h);
end;
theorem Th19:
for n being Nat holds
cdif(f,h).n is Function of V,W
proof
defpred X[Nat] means cdif(f,h).$1 is Function of V,W;
A1: for k be Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume cdif(f,h).k is Function of V,W;
then cD(cdif(f,h).k,h) is Function of V,W;
hence thesis by Def8;
end;
A2: X[0] by Def8;
for n be Nat holds X[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
f is constant implies for x holds cdif(f,h).(n+1)/.x = 0.W
proof
defpred X[Nat] means for x holds cdif(f,h).($1+1)/.x = 0.W;
assume
A1: f is constant;
A2: for x holds f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h) = 0.W
proof
let x;
x-(2*1.F)"*h in the carrier of V;
then
A3: x-(2*1.F)"*h in dom f by FUNCT_2:def 1;
x+(2*1.F)"*h in the carrier of V;
then x+(2*1.F)"*h in dom f by FUNCT_2:def 1;
then f/.(x+(2*1.F)"*h) = f/.(x-(2*1.F)"*h) by A1,A3,FUNCT_1:def 10;
hence thesis by RLVECT_1:15;
end;
A4: X[0]
proof
let x;
thus cdif(f,h).(0+1)/.x = cD(cdif(f,h).0,h)/.x by Def8
.= cD(f,h)/.x by Def8
.= f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h) by Th5
.= 0.W by A2;
end;
A5: for k st X[k] holds X[k+1]
proof
let k;
assume
A6: for x holds cdif(f,h).(k+1)/.x = 0.W;
let x;
A8: cdif(f,h).(k+1) is Function of V,W by Th19;
(cdif(f,h).(k+2))/.x = (cdif(f,h).(k+1+1))/.x
.= cD(cdif(f,h).(k+1),h)/.x by Def8
.= cdif(f,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f,h).(k+1)/.(x-(2*1.F)"*h)
by A8,Th5
.= cdif(f,h).(k+1)/.(x+(2*1.F)"*h) - 0.W by A6
.= cdif(f,h).(k+1)/.(x+(2*1.F)"*h) by RLVECT_1:13
.= 0.W by A6;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem Th21:
cdif(r(#)f,h).(n+1)/.x = r * cdif(f,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds cdif(r(#)f,h).($1+1)/.x = r * cdif(f,h).($1+1)/.x;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds cdif(r(#)f,h).(k+1)/.x = r * cdif(f,h).(k+1)/.x;
let x;
A3: cdif(r(#)f,h).(k+1)/.(x-(2*1.F)"*h)
= r * cdif(f,h).(k+1)/.(x-(2*1.F)"*h) &
cdif(r(#)f,h).(k+1)/.(x+(2*1.F)"*h)
= r * cdif(f,h).(k+1)/.(x+(2*1.F)"*h) by A2;
A4: cdif(r(#)f,h).(k+1) is Function of V,W by Th19;
A5: cdif(f,h).(k+1) is Function of V,W by Th19;
cdif(r(#)f,h).(k+1+1)/.x = cD(cdif(r(#)f,h).(k+1),h)/.x by Def8
.= cdif(r(#)f,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(r(#)f,h).(k+1)/.(x-(2*1.F)"*h) by A4,Th5
.= r * (cdif(f,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f,h).(k+1)/.(x-(2*1.F)"*h)) by VECTSP_1:23,A3
.= r * cD(cdif(f,h).(k+1),h)/.x by A5,Th5
.= r * cdif(f,h).(k+1+1)/.x by Def8;
hence thesis;
end;
A6: X[0]
proof
let x;
x+(2*1.F)"*h in the carrier of V;
then
A7: x+(2*1.F)"*h in dom (r(#)f) by FUNCT_2:def 1;
x-(2*1.F)"*h in the carrier of V;
then
A8: x-(2*1.F)"*h in dom (r(#)f) by FUNCT_2:def 1;
cdif(r(#)f,h).(0+1)/.x = cD(cdif(r(#)f,h).0,h)/.x by Def8
.= cD(r(#)f,h)/.x by Def8
.=(r(#)f)/.(x+(2*1.F)"*h) - (r(#)f)/.(x-(2*1.F)"*h) by Th5
.= r * f/.(x+(2*1.F)"*h) - (r(#)f)/.(x-(2*1.F)"*h) by A7,Def4X
.= r * f/.(x+(2*1.F)"*h) - r * f/.(x-(2*1.F)"*h) by A8,Def4X
.= r * (f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h)) by VECTSP_1:23
.= r * cD(f,h)/.x by Th5
.= r * cD(cdif(f,h).0,h)/.x by Def8
.= r * cdif(f,h).(0+1)/.x by Def8;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
theorem Th22:
cdif(f1+f2,h).(n+1)/.x = cdif(f1,h).(n+1)/.x + cdif(f2,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds cdif(f1+f2,h).($1+1)/.x = cdif(f1,h).($1+1)/.x
+ cdif(f2,h).($1+1)/.x;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds
cdif(f1+f2,h).(k+1)/.x = cdif(f1,h).(k+1)/.x + cdif(f2,h).(k+1)/.x;
let x;
A4: cdif(f1+f2,h).(k+1) is Function of V,W by Th19;
A5: cdif(f2,h).(k+1) is Function of V,W by Th19;
A6: cdif(f1,h).(k+1) is Function of V,W by Th19;
cdif(f1+f2,h).(k+1+1)/.x = cD(cdif(f1+f2,h).(k+1),h)/.x by Def8
.= cdif(f1+f2,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f1+f2,h).(k+1)/.(x-(2*1.F)"*h) by A4,Th5
.=cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) + cdif(f2,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f1+f2,h).(k+1)/.(x-(2*1.F)"*h) by A2
.=(cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) + cdif(f2,h).(k+1)/.(x+(2*1.F)"*h))
- (cdif(f1,h).(k+1)/.(x-(2*1.F)"*h) + cdif(f2,h).(k+1)/.(x-(2*1.F)"*h))
by A2
.=((cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) + cdif(f2,h).(k+1)/.(x+(2*1.F)"*h))
- cdif(f2,h).(k+1)/.(x-(2*1.F)"*h)) - (cdif(f1,h).(k+1)/.(x-(2*1.F)"*h))
by RLVECT_1:27
.=(cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) + (cdif(f2,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f2,h).(k+1)/.(x-(2*1.F)"*h))) - (cdif(f1,h).(k+1)/.(x-(2*1.F)"*h))
by RLVECT_1:28
.=(cdif(f2,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f2,h).(k+1)/.(x-(2*1.F)"*h))
+ (cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - (cdif(f1,h).(k+1)/.(x-(2*1.F)"*h)))
by RLVECT_1:28
.= cD(cdif(f1,h).(k+1),h)/.x + (cdif(f2,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f2,h).(k+1)/.(x-(2*1.F)"*h)) by A6,Th5
.= cD(cdif(f1,h).(k+1),h)/.x + cD(cdif(f2,h).(k+1),h)/.x by A5,Th5
.= cdif(f1,h).(k+1+1)/.x + cD(cdif(f2,h).(k+1),h)/.x by Def8
.= cdif(f1,h).(k+1+1)/.x + cdif(f2,h).(k+1+1)/.x by Def8;
hence thesis;
end;
B1: dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1
.= (the carrier of V) /\ dom f2 by FUNCT_2:def 1
.= (the carrier of V) /\ (the carrier of V) by FUNCT_2:def 1
.= the carrier of V;
A7: X[0]
proof
let x;
reconsider xx = x, hp = (2*1.F)"*h as Element of V;
cdif(f1+f2,h).(0+1)/.x = cD(cdif(f1+f2,h).0,h)/.x by Def8
.= cD(f1+f2,h)/.x by Def8
.= (f1+f2)/.(x+(2*1.F)"*h) - (f1+f2)/.(x-(2*1.F)"*h) by Th5
.= f1/.(xx+(2*1.F)"*h) + f2/.(xx+hp) - (f1+f2)/.(xx-hp)
by B1,VFUNCT_1:def 1
.= f1/.(x+(2*1.F)"*h) + f2/.(x+hp) - (f1/.(x-(2*1.F)"*h) + f2/.(x-hp))
by B1,VFUNCT_1:def 1
.= f1/.(x+(2*1.F)"*h) + f2/.(x+hp) - f1/.(x-(2*1.F)"*h) - f2/.(x-hp)
by RLVECT_1:27
.= (f2/.(x+hp)+(f1/.(x+(2*1.F)"*h) - f1/.(x-(2*1.F)"*h)) - f2/.(x-hp))
by RLVECT_1:28
.= (f1/.(x+(2*1.F)"*h) - f1/.(x-(2*1.F)"*h)) + (f2/.(x+(2*1.F)"*h)
- f2/.(x-(2*1.F)"*h)) by RLVECT_1:28
.= cD(f1,h)/.x + (f2/.(x+(2*1.F)"*h) - f2/.(x-(2*1.F)"*h)) by Th5
.= cD(f1,h)/.x + cD(f2,h)/.x by Th5
.= cD(cdif(f1,h).0,h)/.x + cD(f2,h)/.x by Def8
.= cD(cdif(f1,h).0,h)/.x + cD(cdif(f2,h).0,h)/.x by Def8
.= cdif(f1,h).(0+1)/.x + cD(cdif(f2,h).0,h)/.x by Def8
.= cdif(f1,h).(0+1)/.x + cdif(f2,h).(0+1)/.x by Def8;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem
cdif(f1-f2,h).(n+1)/.x = cdif(f1,h).(n+1)/.x - cdif(f2,h).(n+1)/.x
proof
defpred X[Nat] means
for x holds cdif(f1-f2,h).($1+1)/.x = cdif(f1,h).($1+1)/.x
- cdif(f2,h).($1+1)/.x;
A1: X[0]
proof
let x;
x-(2*1.F)"*h in the carrier of V;
then x-(2*1.F)"*h in dom f1 & x-(2*1.F)"*h in dom f2 by FUNCT_2:def 1;
then x-(2*1.F)"*h in dom f1 /\ dom f2 by XBOOLE_0:def 4;
then
A2: x-(2*1.F)"*h in dom (f1-f2) by VFUNCT_1:def 2;
x+(2*1.F)"*h in the carrier of V;
then x+(2*1.F)"*h in dom f1 & x+(2*1.F)"*h in dom f2 by FUNCT_2:def 1;
then x+(2*1.F)"*h in dom f1 /\ dom f2 by XBOOLE_0:def 4;
then
A3: x+(2*1.F)"*h in dom (f1-f2) by VFUNCT_1:def 2;
cdif(f1-f2,h).(0+1)/.x = cD(cdif(f1-f2,h).0,h)/.x by Def8
.= cD(f1-f2,h)/.x by Def8
.= (f1-f2)/.(x+(2*1.F)"*h) - (f1-f2)/.(x-(2*1.F)"*h) by Th5
.= f1/.(x+(2*1.F)"*h) - f2/.(x+(2*1.F)"*h) - (f1-f2)/.(x-(2*1.F)"*h)
by A3,VFUNCT_1:def 2
.= (f1/.(x+(2*1.F)"*h) - f2/.(x+(2*1.F)"*h)) - (f1/.(x-(2*1.F)"*h)
- f2/.(x-(2*1.F)"*h)) by A2,VFUNCT_1:def 2
.= ((f1/.(x+(2*1.F)"*h) - f2/.(x+(2*1.F)"*h)) - f1/.(x-(2*1.F)"*h))
+ f2/.(x-(2*1.F)"*h) by RLVECT_1:29
.= (f1/.(x+(2*1.F)"*h) - (f1/.(x-(2*1.F)"*h) + f2/.(x+(2*1.F)"*h)))
+ f2/.(x-(2*1.F)"*h) by RLVECT_1:27
.= f1/.(x+(2*1.F)"*h) - ((f1/.(x-(2*1.F)"*h) + f2/.(x+(2*1.F)"*h))
- f2/.(x-(2*1.F)"*h)) by RLVECT_1:29
.= f1/.(x+(2*1.F)"*h) - (f1/.(x-(2*1.F)"*h) + (f2/.(x+(2*1.F)"*h)
- f2/.(x-(2*1.F)"*h))) by RLVECT_1:28
.= (f1/.(x+(2*1.F)"*h) - f1/.(x-(2*1.F)"*h)) - (f2/.(x+(2*1.F)"*h)
- f2/.(x-(2*1.F)"*h)) by RLVECT_1:27
.= cD(f1,h)/.x - (f2/.(x+(2*1.F)"*h) - f2/.(x-(2*1.F)"*h)) by Th5
.= cD(f1,h)/.x - cD(f2,h)/.x by Th5
.= cD(cdif(f1,h).0,h)/.x - cD(f2,h)/.x by Def8
.= cD(cdif(f1,h).0,h)/.x - cD(cdif(f2,h).0,h)/.x by Def8
.= cdif(f1,h).(0+1)/.x - cD(cdif(f2,h).0,h)/.x by Def8
.= cdif(f1,h).(0+1)/.x - cdif(f2,h).(0+1)/.x by Def8;
hence thesis;
end;
A4: for k st X[k] holds X[k+1]
proof
let k;
assume
A5: for x holds
cdif(f1-f2,h).(k+1)/.x = cdif(f1,h).(k+1)/.x - cdif(f2,h).(k+1)/.x;
let x;
A6: cdif(f1-f2,h).(k+1)/.(x-(2*1.F)"*h)
= cdif(f1,h).(k+1)/.(x-(2*1.F)"*h) - cdif(f2,h).(k+1)/.(x-(2*1.F)"*h) &
cdif(f1-f2,h).(k+1)/.(x+(2*1.F)"*h)
= cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f2,h).(k+1)/.(x+(2*1.F)"*h)
by A5;
A7: cdif(f1-f2,h).(k+1) is Function of (the carrier of V),(the carrier of W)
by Th19;
A8: cdif(f2,h).(k+1) is Function of (the carrier of V),(the carrier of W)
by Th19;
A9: cdif(f1,h).(k+1) is Function of (the carrier of V),(the carrier of W)
by Th19;
cdif(f1-f2,h).(k+1+1)/.x = cD(cdif(f1-f2,h).(k+1),h)/.x by Def8
.= cdif(f1-f2,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f1-f2,h).(k+1)/.(x-(2*1.F)"*h) by A7,Th5
.= ((cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f2,h).(k+1)/.(x+(2*1.F)"*h))
- cdif(f1,h).(k+1)/.(x-(2*1.F)"*h)) + cdif(f2,h).(k+1)/.(x-(2*1.F)"*h)
by RLVECT_1:29,A6
.= (cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - (cdif(f1,h).(k+1)/.(x-(2*1.F)"*h)
+ cdif(f2,h).(k+1)/.(x+(2*1.F)"*h))) + cdif(f2,h).(k+1)/.(x-(2*1.F)"*h)
by RLVECT_1:27
.= cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - ((cdif(f1,h).(k+1)/.(x-(2*1.F)"*h)
+ cdif(f2,h).(k+1)/.(x+(2*1.F)"*h)) - cdif(f2,h).(k+1)/.(x-(2*1.F)"*h))
by RLVECT_1:29
.= cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - (cdif(f1,h).(k+1)/.(x-(2*1.F)"*h)
+ (cdif(f2,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f2,h).(k+1)/.(x-(2*1.F)"*h)))
by RLVECT_1:28
.= (cdif(f1,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f1,h).(k+1)/.(x-(2*1.F)"*h))
- (cdif(f2,h).(k+1)/.(x+(2*1.F)"*h) - cdif(f2,h).(k+1)/.(x-(2*1.F)"*h))
by RLVECT_1:27
.= cD(cdif(f1,h).(k+1),h)/.x - (cdif(f2,h).(k+1)/.(x+(2*1.F)"*h)
- cdif(f2,h).(k+1)/.(x-(2*1.F)"*h)) by A9,Th5
.= cD(cdif(f1,h).(k+1),h)/.x - cD(cdif(f2,h).(k+1),h)/.x by A8,Th5
.= cdif(f1,h).(k+1+1)/.x - cD(cdif(f2,h).(k+1),h)/.x by Def8
.= cdif(f1,h).(k+1+1)/.x - cdif(f2,h).(k+1+1)/.x by Def8;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A1,A4);
hence thesis;
end;
theorem
cdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= r1 * cdif(f1,h).(n+1)/.x + r2 * cdif(f2,h).(n+1)/.x
proof
set g1 = r1(#)f1;
set g2 = r2(#)f2;
cdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= cdif(g1,h).(n+1)/.x + cdif(g2,h).(n+1)/.x by Th22
.= r1 * cdif(f1,h).(n+1)/.x + cdif(g2,h).(n+1)/.x by Th21
.= r1 * cdif(f1,h).(n+1)/.x + r2 * cdif(f2,h).(n+1)/.x by Th21;
hence thesis;
end;
theorem
(cdif(f,h).1)/.x = Shift(f,((2*1.F)"*h))/.x - Shift(f,-((2*1.F)"*h))/.x
proof
set f2 = Shift(f,-((2*1.F)"*h));
set f1 = Shift(f,((2*1.F)"*h));
(cdif(f,h).1)/.x = cdif(f,h).(0+1)/.x
.= cD(cdif(f,h).0,h)/.x by Def8
.= cD(f,h)/.x by Def8
.= f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h) by Th5
.= f1/.x - f/.(x+-((2*1.F)"*h)) by Def2
.= f1/.x - f2/.x by Def2;
hence thesis;
end;
theorem
(fdif(f,h).n)/.x = (bdif(f,h).n)/.(x+n*h)
proof
defpred X[Nat] means
for x holds (fdif(f,h).$1)/.x = (bdif(f,h).$1)/.(x+$1*h);
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds (fdif(f,h).k)/.x = (bdif(f,h).k)/.(x+k*h);
let x;
A3: (fdif(f,h).k)/.(x+h) = (bdif(f,h).k)/.(x+h+k*h) by A2;
reconsider fdk = fdif(f,h).k as Function of (the carrier of V),
(the carrier of W) by Th2;
N2: k*h + h = k*h + 1*h by BINOM:13
.= (k+1)*h by BINOM:15;
N3: k*h = k*h + 0.V by RLVECT_1:4
.=k*h + (h-h) by RLVECT_1:15
.= (k+1)*h - h by N2,RLVECT_1:28;
A5: bdif(f,h).k is Function of (the carrier of V),(the carrier of W)
by Th12;
(fdif(f,h).(k+1))/.x = fD(fdk,h)/.x by Def6
.= (fdk)/.(x+h) - (fdk)/.x by Th3
.= (bdif(f,h).k)/.(x+h+k*h) - (bdif(f,h).k)/.(x+k*h) by A2,A3
.= (bdif(f,h).k)/.(x+(h+k*h)) - (bdif(f,h).k)/.(x+k*h) by RLVECT_1:def 3
.= (bdif(f,h).k)/.(x+(k+1)*h) - (bdif(f,h).k)/.((x+(k+1)*h)-h)
by RLVECT_1:28,N3,N2
.= bD(bdif(f,h).k,h)/.(x+(k+1)*h) by A5,Th4
.= (bdif(f,h).(k+1))/.(x+(k+1)*h) by Def7;
hence thesis;
end;
A6: X[0]
proof
let x;
(fdif(f,h).0)/.x = f/.x by Def6
.= (bdif(f,h).0)/.x by Def7
.= (bdif(f,h).0)/.(x+0.V) by RLVECT_1:4
.= (bdif(f,h).0)/.(x+0*h) by BINOM:12;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
theorem LAST0:
1.F <> -1.F implies (fdif(f,h).(2*n))/.x = (cdif(f,h).(2*n))/.(x+n*h)
proof
assume
AS: 1.F <> -1.F;
defpred X[Nat] means
for x holds (fdif(f,h).(2*$1))/.x = (cdif(f,h).(2*$1))/.(x+$1*h);
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: for x holds (fdif(f,h).(2*k))/.x = cdif(f,h).(2*k)/.(x+k*h);
let x;
A31: h+h = 1*h+h by BINOM:13
.= 1*h + 1*h by BINOM:13
.= (1+1)*h by BINOM:15;
A32: 1.F + 1.F = 1*1.F + 1.F by BINOM:13
.= 1*1.F + 1*1.F by BINOM:13
.= (1+1)*1.F by BINOM:15
.= 2*1.F;
A33: h+h = 1.F*h + h
.= 1.F*h + 1.F*h
.= (2*1.F) * h by A32,VECTSP_1:def 15;
A30: 2*1.F <> 0.F
proof
assume
A301: 2*1.F = 0.F;
1.F + 1.F
= 1*1.F + 1.F by BINOM:13
.= 1*1.F + 1*1.F by BINOM:13
.= (1+1)*1.F by BINOM:15
.= 0.F by A301;
hence contradiction by AS,RLVECT_1:def 10;
end;
A34: (2*1.F)"*h + (2*1.F)"*h
= (2*1.F)"*(h+h) by VECTSP_1:def 14
.= ((2*1.F)"*(2*1.F))*h by VECTSP_1:def 16,A33
.= 1.F * h by A30,VECTSP_1:def 10
.= h;
A35: x+(k+1)*h - (2*1.F)"*h - (2*1.F)"*h
= x+ (k*h + 1*h) - (2*1.F)"*h - (2*1.F)"*h by BINOM:15
.= x + k*h + 1*h - (2*1.F)"*h - (2*1.F)"*h by RLVECT_1:def 3
.= x + k*h + h - (2*1.F)"*h - (2*1.F)"*h by BINOM:13
.= x + k*h + h - ((2*1.F)"*h + (2*1.F)"*h) by RLVECT_1:27
.= x + k*h + (h-h) by RLVECT_1:28,A34
.= x + k*h + 0.V by RLVECT_1:15
.= x + k*h by RLVECT_1:4;
A36: x+(k+1)*h + (2*1.F)"*h + (2*1.F)"*h
= x + (k+1)*h + ((2*1.F)"*h + (2*1.F)"*h) by RLVECT_1:def 3
.= x + ((k+1)*h + h) by RLVECT_1:def 3,A34
.= x + ((k+1)*h + 1*h) by BINOM:13
.= x + ((k+1+1)*h) by BINOM:15
.= x + (k+2)*h;
A3: fdif(f,h).(2*k)/.(x+h+h) = cdif(f,h).(2*k)/.(x+h+h+k*h) by A2
.= cdif(f,h).(2*k)/.(x+h+(h+k*h)) by RLVECT_1:def 3
.= cdif(f,h).(2*k)/.(x+(h+(h+k*h))) by RLVECT_1:def 3
.= cdif(f,h).(2*k)/.(x+(h+h+(k*h))) by RLVECT_1:def 3
.= cdif(f,h).(2*k)/.(x+(k+2)*h) by BINOM:15,A31;
A4: fdif(f,h).(2*k)/.(x+h) = cdif(f,h).(2*k)/.(x+h+k*h) by A2
.= cdif(f,h).(2*k)/.(x+1*h+k*h) by BINOM:13
.= cdif(f,h).(2*k)/.(x+(1*h+k*h)) by RLVECT_1:def 3
.= cdif(f,h).(2*k)/.(x+(k+1)*h) by BINOM:15;
set r3 = cdif(f,h).(2*k)/.(x+k*h);
set r2 = cdif(f,h).(2*k)/.(x+(k+1)*h);
set r1 = cdif(f,h).(2*k)/.(x+(k+2)*h);
A5: fdif(f,h).(2*k+1) is Function of V,W by Th2;
A6: cdif(f,h).(2*k) is Function of V,W by Th19;
A7: cdif(f,h).(2*k+1) is Function of V,W by Th19;
A8: fdif(f,h).(2*k) is Function of V,W by Th2;
A9: cdif(f,h).(2*k+1)/.(x+(k+1)*h-(2*1.F)"*h)
= cD(cdif(f,h).(2*k),h)/.(x+(k+1)*h-(2*1.F)"*h) by Def8
.= cdif(f,h).(2*k)/.(x+(k+1)*h-(2*1.F)"*h+(2*1.F)"*h)
- cdif(f,h).(2*k)/.(x+(k+1)*h-(2*1.F)"*h-(2*1.F)"*h) by A6,Th5
.= cdif(f,h).(2*k)/.(x+(k+1)*h-((2*1.F)"*h-(2*1.F)"*h))
- cdif(f,h).(2*k)/.(x+(k+1)*h-(2*1.F)"*h-(2*1.F)"*h) by RLVECT_1:29
.= cdif(f,h).(2*k)/.(x+(k+1)*h-0.V)
- cdif(f,h).(2*k)/.(x+(k+1)*h-(2*1.F)"*h-(2*1.F)"*h) by RLVECT_1:15
.= cdif(f,h).(2*k)/.(x+(k+1)*h) - cdif(f,h).(2*k)/.(x+k*h)
by A35,RLVECT_1:13;
A10: cdif(f,h).(2*k+1)/.(x+(k+1)*h+(2*1.F)"*h)
= cD(cdif(f,h).(2*k),h)/.(x+(k+1)*h+(2*1.F)"*h) by Def8
.= cdif(f,h).(2*k)/.(x+(k+1)*h+(2*1.F)"*h+(2*1.F)"*h)
- cdif(f,h).(2*k)/.(x+(k+1)*h+(2*1.F)"*h-(2*1.F)"*h) by A6,Th5
.= cdif(f,h).(2*k)/.(x+(k+1)*h+(2*1.F)"*h+(2*1.F)"*h)
- cdif(f,h).(2*k)/.(x+(k+1)*h+((2*1.F)"*h-(2*1.F)"*h)) by RLVECT_1:28
.= cdif(f,h).(2*k)/.(x+(k+1)*h+(2*1.F)"*h+(2*1.F)"*h)
- cdif(f,h).(2*k)/.(x+(k+1)*h+0.V) by RLVECT_1:15
.= cdif(f,h).(2*k)/.(x+(k+2)*h) - cdif(f,h).(2*k)/.(x+(k+1)*h)
by A36,RLVECT_1:4;
A11: cdif(f,h).(2*(k+1))/.(x+(k+1)*h) = cdif(f,h).(2*k+1+1)/.(x+(k+1)*h)
.= cD(cdif(f,h).(2*k+1),h)/.(x+(k+1)*h) by Def8
.= (r1-r2) - (r2-r3) by A7,A10,A9,Th5;
fdif(f,h).(2*(k+1))/.x = fdif(f,h).(2*k+1+1)/.x
.= fD(fdif(f,h).(2*k+1),h)/.x by Def6
.= (fdif(f,h).(2*k+1))/.(x+h) - (fdif(f,h).(2*k+1))/.x by A5,Th3
.= fD(fdif(f,h).(2*k),h)/.(x+h) - (fdif(f,h).(2*k+1))/.x by Def6
.= fD(fdif(f,h).(2*k),h)/.(x+h) - fD(fdif(f,h).(2*k),h)/.x by Def6
.= fdif(f,h).(2*k)/.(x+h+h) - fdif(f,h).(2*k)/.(x+h)
- fD(fdif(f,h).(2*k),h)/.x by A8,Th3
.= fdif(f,h).(2*k)/.(x+h+h) - fdif(f,h).(2*k)/.(x+h)
- (fdif(f,h).(2*k)/.(x+h) - fdif(f,h).(2*k)/.x) by A8,Th3
.= cdif(f,h).(2*k)/.(x+(k+2)*h) - cdif(f,h).(2*k)/.(x+(k+1)*h)
- (cdif(f,h).(2*k)/.(x+(k+1)*h) - cdif(f,h).(2*k)/.(x+k*h)) by A2,A3,A4;
hence thesis by A11;
end;
A12: X[0]
proof
let x;
(fdif(f,h).(2*0))/.x = f/.x by Def6
.= (cdif(f,h).(2*0))/.x by Def8
.= (cdif(f,h).(2*0))/.(x+0.V) by RLVECT_1:4
.= (cdif(f,h).(2*0))/.(x+0*h) by BINOM:12;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A12,A1);
hence thesis;
end;
theorem
1.F <> -1.F implies
(fdif(f,h).(2*n+1))/.x = (cdif(f,h).(2*n+1))/.(x+n*h+(2*1.F)"*h)
proof
assume
AS: 1.F <> -1.F;
A32: 1.F + 1.F = 1*1.F + 1.F by BINOM:13
.= 1*1.F + 1*1.F by BINOM:13
.= (1+1)*1.F by BINOM:15
.= 2*1.F;
A33: h+h = 1.F*h + h
.= 1.F*h + 1.F* h
.= (2*1.F) * h by A32,VECTSP_1:def 15;
A30: 2*1.F <> 0.F
proof
assume
A301: 2*1.F = 0.F;
1.F + 1.F
= 1*1.F + 1.F by BINOM:13
.= 1*1.F + 1*1.F by BINOM:13
.= (1+1)*1.F by BINOM:15
.= 0.F by A301;
hence contradiction by AS,RLVECT_1:def 10;
end;
A34: (2*1.F)"*h + (2*1.F)"*h
= (2*1.F)"*(h+h) by VECTSP_1:def 14
.=((2*1.F)"*(2*1.F))*h by VECTSP_1:def 16,A33
.= 1.F * h by A30,VECTSP_1:def 10
.= h;
A52: cdif(f,h).(2*n) is Function of V,W by Th19;
A35: x+n*h + (2*1.F)"*h - (2*1.F)"*h
= x+n*h + ((2*1.F)"*h-(2*1.F)"*h) by RLVECT_1:28
.=x+n*h + 0.V by RLVECT_1:15
.= x+n*h by RLVECT_1:4;
A36: x+n*h + (2*1.F)"*h + (2*1.F)"*h
= x+n*h + ((2*1.F)"*h+(2*1.F)"*h) by RLVECT_1:def 3
.= x + (n*h+h) by RLVECT_1:def 3,A34
.= x + (n*h+1*h) by BINOM:13
.= x + (n+1)*h by BINOM:15;
A51: fdif(f,h).(2*n) is Function of V,W by Th2;
A11: cdif(f,h).(2*n+1)/.(x+n*h+(2*1.F)"*h)
= cD(cdif(f,h).(2*n),h)/.(x+n*h+(2*1.F)"*h) by Def8
.= cdif(f,h).(2*n)/.(x+(n+1)*h)
- cdif(f,h).(2*n)/.(x+n*h+(2*1.F)"*h-(2*1.F)"*h) by A36,Th5,A52
.= cdif(f,h).(2*n)/.(x+(n*h+1*h)) - cdif(f,h).(2*n)/.(x+n*h) by BINOM:15,A35
.= cdif(f,h).(2*n)/.(x+(n*h+h)) - cdif(f,h).(2*n)/.(x+n*h) by BINOM:13
.= cdif(f,h).(2*n)/.(x+h+n*h) - cdif(f,h).(2*n)/.(x+n*h) by RLVECT_1:def 3
.= fdif(f,h).(2*n)/.(x+h) - cdif(f,h).(2*n)/.(x+n*h) by LAST0,AS
.= fdif(f,h).(2*n)/.(x+h) - fdif(f,h).(2*n)/.x by LAST0,AS;
fdif(f,h).(2*n+1)/.x = fD(fdif(f,h).(2*n),h)/.x by Def6
.= (fdif(f,h).(2*n))/.(x+h) - (fdif(f,h).(2*n))/.x by Th3,A51;
hence thesis by A11;
end;