:: Functional Sequence from a Domain to a Domain :: by Beata Perkowska :: :: Received May 22, 1992 :: Copyright (c) 1992-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, SUBSET_1, NUMBERS, REAL_1, FUNCT_1, NAT_1, PARTFUN1, RELAT_1, TARSKI, VALUED_1, ORDINAL4, ARYTM_1, COMPLEX1, ARYTM_3, CARD_1, SEQ_1, PBOOLE, XXREAL_0, SEQ_2, ORDINAL2, FCONT_1, SEQFUNC, FUNCT_7, ORDINAL1, ZFMISC_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, FCONT_1; constructors PARTFUN1, FUNCOP_1, REAL_1, COMPLEX1, SEQ_2, RFUNCT_1, FCONT_1, LIMFUNC1, VALUED_1, RELSET_1, COMSEQ_2; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, PARTFUN1, NAT_1; requirements NUMERALS, SUBSET, ARITHM; begin reserve D for non empty set, D1,D2,x,y for set, n,k for Nat, p,x1 ,r for Real, f for Function; definition let D1,D2; mode Functional_Sequence of D1,D2 is sequence of PFuncs(D1,D2); end; reserve F for Functional_Sequence of D1,D2; definition let D1,D2,F; let n be natural Number; redefine func F.n -> PartFunc of D1,D2; end; reserve G,H,H1,H2,J for Functional_Sequence of D,REAL; theorem :: SEQFUNC:1 f is Functional_Sequence of D1,D2 iff dom f = NAT & for n holds f.n is PartFunc of D1,D2; scheme :: SEQFUNC:sch 1 ExFuncSeq{D1() -> set, D2() -> set, F(object)->PartFunc of D1(),D2()}: ex G being Functional_Sequence of D1(), D2() st for n being Nat holds G.n = F(n); definition let D,H; let r be Real; func r(#)H ->Functional_Sequence of D,REAL means :: SEQFUNC:def 1 for n being Nat holds it.n = r(#)(H.n); end; definition let D,H; func H" -> Functional_Sequence of D,REAL means :: SEQFUNC:def 2 for n being Nat holds it.n=(H.n)^; func - H -> Functional_Sequence of D,REAL means :: SEQFUNC:def 3 for n being Nat holds it.n = -H.n; involutiveness; func abs(H)->Functional_Sequence of D,REAL means :: SEQFUNC:def 4 for n being Nat holds it.n=abs(H.n); projectivity; end; definition let D,G,H; func G + H -> Functional_Sequence of D,REAL means :: SEQFUNC:def 5 for n being Nat holds it.n = G.n + H.n; end; definition let D,G,H; func G - H -> Functional_Sequence of D,REAL equals :: SEQFUNC:def 6 G + -H; end; definition let D,G,H; func G (#) H -> Functional_Sequence of D,REAL means :: SEQFUNC:def 7 for n being Nat holds it.n =G.n (#) H.n; end; definition let D,H,G; func G / H ->Functional_Sequence of D,REAL equals :: SEQFUNC:def 8 G (#) (H"); end; theorem :: SEQFUNC:2 H1 = G/H iff for n holds H1.n = G.n / H.n; theorem :: SEQFUNC:3 H1 = G - H iff for n holds H1.n = G.n - H.n; theorem :: SEQFUNC:4 G + H = H + G & (G + H) + J = G + (H + J); theorem :: SEQFUNC:5 G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J); theorem :: SEQFUNC:6 (G + H) (#) J = G(#)J + H(#)J & J (#) (G + H) = J(#)G + J(#)H; theorem :: SEQFUNC:7 -H = (-1)(#)H; theorem :: SEQFUNC:8 (G - H) (#) J = G(#)J - H(#)J & J(#)G - J(#)H = J (#) (G - H); theorem :: SEQFUNC:9 r(#)(G + H) = r(#)G + r(#)H & r(#)(G - H) = r(#)G - r(#)H; theorem :: SEQFUNC:10 (r*p)(#)H = r(#)(p(#)H); theorem :: SEQFUNC:11 1 (#) H = H; ::$CT theorem :: SEQFUNC:13 G" (#) H" = (G(#)H)"; theorem :: SEQFUNC:14 r<>0 implies (r(#)H)" = r" (#) H"; theorem :: SEQFUNC:15 abs(H)"=abs(H"); theorem :: SEQFUNC:16 abs(G(#)H) = abs(G) (#) abs(H); theorem :: SEQFUNC:17 abs(G/H) = abs(G) / abs(H); theorem :: SEQFUNC:18 abs(r(#)H) = |.r.| (#) abs(H); reserve x for Element of D, X,Y for set, S1,S2 for Real_Sequence, f for PartFunc of D,REAL; definition let D1,D2,F,X; pred X common_on_dom F means :: SEQFUNC:def 9 X <> {} & for n holds X c= dom (F.n); end; definition let D,H,x; func H#x ->Real_Sequence means :: SEQFUNC:def 10 for n holds it.n = (H.n).x; end; definition let D,H,X; pred H is_point_conv_on X means :: SEQFUNC:def 11 X common_on_dom H & ex f st X = dom f & for x st x in X holds for p st p>0 ex k st for n st n>=k holds |.(H.n).x - f.x.| < p; end; theorem :: SEQFUNC:19 H is_point_conv_on X iff X common_on_dom H & ex f st X = dom f & for x st x in X holds (H#x) is convergent & lim(H#x) = f.x; theorem :: SEQFUNC:20 H is_point_conv_on X iff X common_on_dom H & for x st x in X holds (H#x) is convergent; definition let D,H,X; pred H is_unif_conv_on X means :: SEQFUNC:def 12 X common_on_dom H & ex f st X = dom f & for p st p>0 ex k st for n,x st n>=k & x in X holds |.(H.n).x - f.x.| < p; end; definition let D,H,X; assume H is_point_conv_on X; func lim(H,X) -> PartFunc of D,REAL means :: SEQFUNC:def 13 dom it = X & for x st x in dom it holds it.x = lim(H#x); end; theorem :: SEQFUNC:21 H is_point_conv_on X implies (f = lim(H,X) iff dom f = X & for x st x in X holds for p st p>0 ex k st for n st n>=k holds |.(H.n).x - f.x.| < p ); theorem :: SEQFUNC:22 H is_unif_conv_on X implies H is_point_conv_on X; theorem :: SEQFUNC:23 Y c= X & Y<>{} & X common_on_dom H implies Y common_on_dom H; theorem :: SEQFUNC:24 Y c= X & Y<>{} & H is_point_conv_on X implies H is_point_conv_on Y & lim(H,X)|Y = lim(H,Y); theorem :: SEQFUNC:25 Y c= X & Y<>{} & H is_unif_conv_on X implies H is_unif_conv_on Y; theorem :: SEQFUNC:26 X common_on_dom H implies for x st x in X holds {x} common_on_dom H; theorem :: SEQFUNC:27 H is_point_conv_on X implies for x st x in X holds {x} common_on_dom H; theorem :: SEQFUNC:28 {x} common_on_dom H1 & {x} common_on_dom H2 implies H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x & (H1#x) (#) (H2#x) = (H1(#)H2)#x; theorem :: SEQFUNC:29 (abs(H))#x = abs(H#x) & (-H)#x = -(H#x); theorem :: SEQFUNC:30 {x} common_on_dom H implies (r(#)H)#x = r(#)(H#x); theorem :: SEQFUNC:31 X common_on_dom H1 & X common_on_dom H2 implies for x st x in X holds H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x & (H1#x) (#) (H2#x) = ( H1(#)H2)#x; theorem :: SEQFUNC:32 abs(H)#x = abs(H#x) & (-H)#x = -(H#x); theorem :: SEQFUNC:33 X common_on_dom H implies for x st x in X holds (r(#)H)#x = r(#) (H#x); theorem :: SEQFUNC:34 H1 is_point_conv_on X & H2 is_point_conv_on X implies for x st x in X holds H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x & (H1#x) (#) (H2#x ) = (H1(#)H2)#x; theorem :: SEQFUNC:35 abs(H)#x = abs(H#x) & (-H)#x = -(H#x); theorem :: SEQFUNC:36 H is_point_conv_on X implies for x st x in X holds (r(#)H)#x = r(#)(H# x); theorem :: SEQFUNC:37 X common_on_dom H1 & X common_on_dom H2 implies X common_on_dom H1+H2 & X common_on_dom H1-H2 & X common_on_dom H1(#)H2; theorem :: SEQFUNC:38 X common_on_dom H implies X common_on_dom abs(H) & X common_on_dom (-H); theorem :: SEQFUNC:39 X common_on_dom H implies X common_on_dom r(#)H; theorem :: SEQFUNC:40 H1 is_point_conv_on X & H2 is_point_conv_on X implies H1+H2 is_point_conv_on X & lim(H1+H2,X) = lim(H1,X) + lim(H2,X) & H1-H2 is_point_conv_on X & lim(H1-H2,X) = lim(H1,X) - lim(H2,X) & H1(#)H2 is_point_conv_on X & lim(H1(#)H2,X) = lim(H1,X) (#) lim(H2,X); theorem :: SEQFUNC:41 H is_point_conv_on X implies abs(H) is_point_conv_on X & lim (abs(H),X ) = |. lim (H,X) .| & -H is_point_conv_on X & lim (-H,X) = - lim(H,X); theorem :: SEQFUNC:42 H is_point_conv_on X implies r(#)H is_point_conv_on X & lim (r(#)H,X) = r(#)(lim(H,X)); theorem :: SEQFUNC:43 H is_unif_conv_on X iff X common_on_dom H & H is_point_conv_on X & for r st 0=k & x in X holds |.(H.n).x-(lim(H,X)).x.|