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