:: Difference of Function on Vector Space over $\mathbbF$
:: by Kenichi Arai , Ken Wakabayashi and Hiroyuki Okazaki
::
:: Received September 26, 2014
:: Copyright (c) 2014-2021 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;
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;
func r(#)f -> PartFunc of C,V means
:: VSDIFF_1:def 1
dom it = dom f &
for c being Element of C st c in dom it holds it/.c = r * (f/.c);
end;
registration
let C,GF,V;
let f be Function of C,V;
let r be Element of GF;
cluster r(#)f -> total;
end;
definition
let GF,V,v,W;
func v ++ W -> Subset of V equals
:: VSDIFF_1:def 2
{v + u : u in W};
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
:: VSDIFF_1:def 3
dom it = (-h) ++ (dom f) &
(for x being Element of V st x in (-h) ++ (dom f) holds it.x = f.(x+h));
end;
theorem :: VSDIFF_1:1
for x being Element of V, A being Subset of V st A = the carrier of V
holds x ++ A = A;
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
:: VSDIFF_1:def 4
for x be Element of V holds it.x = f.(x+h);
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
:: VSDIFF_1:def 5
Shift(f,h) - f;
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;
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
:: VSDIFF_1:def 6
f - Shift(f,-h);
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;
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
:: VSDIFF_1:def 7
Shift(f,(2*1.F)"*h) - Shift(f,-(2*1.F)"*h);
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;
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
:: VSDIFF_1:def 8
it.0 = f & for n being Nat holds it.(n+1) = fD(it.n,h);
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 :: VSDIFF_1:2
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;
theorem :: VSDIFF_1:3
for n be Nat holds
fdif(f,h).n is Function of V, W;
theorem :: VSDIFF_1:4
fD(f,h)/.x = f/.(x+h) - f/.x;
theorem :: VSDIFF_1:5
bD(f,h)/.x = f/.x - f/.(x-h);
theorem :: VSDIFF_1:6
cD(f,h)/.x = f/.(x+(2*1.F)"*h) - f/.(x-(2*1.F)"*h);
reserve n,m,k for Nat;
theorem :: VSDIFF_1:7
f is constant implies for x holds fdif(f,h).(n+1)/.x = 0.W;
theorem :: VSDIFF_1:8
fdif(r(#)f,h).(n+1)/.x = r* fdif(f,h).(n+1)/.x;
theorem :: VSDIFF_1:9
fdif(f1+f2,h).(n+1)/.x = fdif(f1,h).(n+1)/.x + fdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:10
fdif(f1-f2,h).(n+1)/.x = fdif(f1,h).(n+1)/.x - fdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:11
fdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= r1 * (fdif(f1,h).(n+1)/.x) + r2 * (fdif(f2,h).(n+1)/.x);
theorem :: VSDIFF_1:12
(fdif(f,h).1)/.x = Shift(f,h)/.x - f/.x;
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
:: VSDIFF_1:def 9
it.0 = f & for n being Nat holds it.(n+1) = bD(it.n,h);
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
:: VSDIFF_1:def 10
it.0 = f & for n being Nat holds it.(n+1) = bD(it.n,h);
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 :: VSDIFF_1:13
for n be Nat holds
bdif(f,h).n is Function of V,W;
theorem :: VSDIFF_1:14
f is constant implies for x holds bdif(f,h).(n+1)/.x = 0.W;
theorem :: VSDIFF_1:15
bdif(r(#)f,h).(n+1)/.x = r * bdif(f,h).(n+1)/.x;
theorem :: VSDIFF_1:16
bdif(f1+f2,h).(n+1)/.x = bdif(f1,h).(n+1)/.x + bdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:17
bdif(f1-f2,h).(n+1)/.x = bdif(f1,h).(n+1)/.x - bdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:18
bdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= r1 * bdif(f1,h).(n+1)/.x + r2 * bdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:19
(bdif(f,h).1)/.x = f/.x - Shift(f,-h)/.x;
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
:: VSDIFF_1:def 11
it.0 = f & for n be Nat holds it.(n+1) = cD(it.n,h);
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 :: VSDIFF_1:20
for n being Nat holds
cdif(f,h).n is Function of V,W;
theorem :: VSDIFF_1:21
f is constant implies for x holds cdif(f,h).(n+1)/.x = 0.W;
theorem :: VSDIFF_1:22
cdif(r(#)f,h).(n+1)/.x = r * cdif(f,h).(n+1)/.x;
theorem :: VSDIFF_1:23
cdif(f1+f2,h).(n+1)/.x = cdif(f1,h).(n+1)/.x + cdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:24
cdif(f1-f2,h).(n+1)/.x = cdif(f1,h).(n+1)/.x - cdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:25
cdif(r1(#)f1+r2(#)f2,h).(n+1)/.x
= r1 * cdif(f1,h).(n+1)/.x + r2 * cdif(f2,h).(n+1)/.x;
theorem :: VSDIFF_1:26
(cdif(f,h).1)/.x = Shift(f,((2*1.F)"*h))/.x - Shift(f,-((2*1.F)"*h))/.x;
theorem :: VSDIFF_1:27
(fdif(f,h).n)/.x = (bdif(f,h).n)/.(x+n*h);
theorem :: VSDIFF_1:28
1.F <> -1.F implies (fdif(f,h).(2*n))/.x = (cdif(f,h).(2*n))/.(x+n*h);
theorem :: VSDIFF_1:29
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);