:: Functional Sequence in Norm Space :: by Hiroshi Yamazaki :: :: Received October 25, 2020 :: Copyright (c) 2020-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, ARYTM_1, COMPLEX1, ARYTM_3, CARD_1, PBOOLE, XXREAL_0, SEQ_2, ORDINAL2, FCONT_1, SEQFUNC, FUNCT_7, NORMSP_1, PRE_TOPC, STRUCT_0, CFCONT_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQFUNC, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, NFCONT_1; constructors COMPLEX1, SEQ_2, FCONT_1, VALUED_1, RELSET_1, COMSEQ_2, SEQFUNC, POWER, VFUNCT_1, NFCONT_1; registrations XBOOLE_0, RELSET_1, XREAL_0, MEMBERED, PARTFUN1, NAT_1, ORDINAL1, STRUCT_0, NORMSP_1; requirements SUBSET, BOOLE, NUMERALS, ARITHM; begin :: 1. Preliminaries reserve D for non empty set, D1, D2, x, y, Z for set, n, k for Nat, p, x1, r for Real, f for Function, Y for RealNormSpace, G, H, H1, H2, J for Functional_Sequence of D,the carrier of Y; theorem :: SEQFUNC2:1 f is Functional_Sequence of D1, D2 iff (dom f = NAT & for x st x in NAT holds f.x is PartFunc of D1, D2); definition let D; let Y be non empty NORMSTR; let H be Functional_Sequence of D,the carrier of Y; let r be Real; func r(#)H -> Functional_Sequence of D, the carrier of Y means :: SEQFUNC2:def 1 for n being Nat holds it.n = r(#)(H.n); end; definition let D; let Y be RealNormSpace; let H be Functional_Sequence of D,the carrier of Y; func - H -> Functional_Sequence of D,the carrier of Y means :: SEQFUNC2:def 2 for n being Nat holds it.n = -H.n; involutiveness; end; definition let D; let Y be non empty NORMSTR; let H be Functional_Sequence of D,the carrier of Y; func ||.H.|| -> Functional_Sequence of D,REAL means :: SEQFUNC2:def 3 for n being Nat holds it.n = ||.(H.n) .||; end; definition let D; let Y be non empty NORMSTR; let G, H be Functional_Sequence of D,the carrier of Y; func G + H -> Functional_Sequence of D,the carrier of Y means :: SEQFUNC2:def 4 for n being Nat holds it.n = G.n + H.n; end; definition let D; let Y be RealNormSpace; let G, H be Functional_Sequence of D,the carrier of Y; func G - H -> Functional_Sequence of D, the carrier of Y equals :: SEQFUNC2:def 5 G + -H; end; theorem :: SEQFUNC2:2 H1 = G - H iff for n holds H1.n = G.n - H.n; theorem :: SEQFUNC2:3 G + H = H + G & (G + H) + J = G + (H + J); theorem :: SEQFUNC2:4 -H = (-1)(#)H; theorem :: SEQFUNC2:5 r(#)(G + H) = r(#)G + r(#)H & r(#)(G - H) = r(#)G - r(#)H; theorem :: SEQFUNC2:6 (r*p)(#)H = r(#)(p(#)H); theorem :: SEQFUNC2:7 1 (#) H = H; theorem :: SEQFUNC2:8 ||.r(#)H.|| = |.r.| (#) ||.H.||; begin :: 2. Pointwise convergence reserve x for Element of D, X for set, S1, S2 for sequence of Y, f for PartFunc of D,the carrier of Y; definition let D; let Y be non empty NORMSTR; let H be Functional_Sequence of D,the carrier of Y; let x; func H#x -> sequence of the carrier of Y means :: SEQFUNC2:def 6 for n holds it.n = (H.n)/.x; end; definition let D, Y, H, X; pred H is_point_conv_on X means :: SEQFUNC2:def 7 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 :: SEQFUNC2:9 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 :: SEQFUNC2:10 H is_point_conv_on X iff X common_on_dom H & for x st x in X holds (H#x) is convergent; begin :: 3. Uniform convergence and limit of functional sequence definition let D, Y, H, X; pred H is_unif_conv_on X means :: SEQFUNC2:def 8 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, Y, H, X; assume H is_point_conv_on X; func lim(H, X) -> PartFunc of D,the carrier of Y means :: SEQFUNC2:def 9 dom it = X & for x st x in dom it holds it.x = lim(H#x); end; theorem :: SEQFUNC2:11 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 :: SEQFUNC2:12 H is_unif_conv_on X implies H is_point_conv_on X; theorem :: SEQFUNC2:13 Z c= X & Z<>{} & X common_on_dom H implies Z common_on_dom H; theorem :: SEQFUNC2:14 Z c= X & Z<>{} & H is_point_conv_on X implies H is_point_conv_on Z & lim(H, X)|Z = lim(H,Z); theorem :: SEQFUNC2:15 Z c= X & Z <> {} & H is_unif_conv_on X implies H is_unif_conv_on Z; theorem :: SEQFUNC2:16 X common_on_dom H implies for x be set st x in X holds {x} common_on_dom H; theorem :: SEQFUNC2:17 :: LM01: H is_point_conv_on X implies for x be set st x in X holds {x} common_on_dom H; theorem :: SEQFUNC2:18 {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; reserve x for Element of D; theorem :: SEQFUNC2:19 {x} common_on_dom H implies (||.H.||)#x = ||.H#x .|| & (-H)#x = (-1)*(H#x); theorem :: SEQFUNC2:20 {x} common_on_dom H implies (r(#)H)#x = r*(H#x); theorem :: SEQFUNC2:21 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; theorem :: SEQFUNC2:22 :: Th31: {x} common_on_dom H implies ||.H.||#x = ||.(H#x).|| & (-H)#x = (-1)*(H#x); theorem :: SEQFUNC2:23 X common_on_dom H implies for x st x in X holds (r(#)H)#x = r*(H#x); theorem :: SEQFUNC2:24 :: Th33: 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; theorem :: SEQFUNC2:25 {x} common_on_dom H implies ||.H.||#x = ||.(H#x).|| & (-H)#x = (-1)*(H#x); theorem :: SEQFUNC2:26 H is_point_conv_on X implies for x st x in X holds (r(#)H)#x = r*(H# x); theorem :: SEQFUNC2:27 X common_on_dom H1 & X common_on_dom H2 implies X common_on_dom H1 + H2 & X common_on_dom H1-H2; theorem :: SEQFUNC2:28 X common_on_dom H implies X common_on_dom ||.H.|| & X common_on_dom (-H); theorem :: SEQFUNC2:29 X common_on_dom H implies X common_on_dom r(#)H; theorem :: SEQFUNC2:30 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); theorem :: SEQFUNC2:31 H is_point_conv_on X implies ||.H.|| is_point_conv_on X & lim (||.H.||, X) = ||. lim (H, X) .|| & -H is_point_conv_on X & lim (-H, X) = - lim(H, X); theorem :: SEQFUNC2:32 H is_point_conv_on X implies r(#)H is_point_conv_on X & lim (r(#)H, X) = r(#)(lim(H, X)); theorem :: SEQFUNC2:33 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.|| < r; reserve V, W for RealNormSpace, H for Functional_Sequence of the carrier of V,the carrier of W; theorem :: SEQFUNC2:34 H is_unif_conv_on X & (for n holds (H.n)|X is_continuous_on X) implies lim(H, X) is_continuous_on X;