:: Weak Convergence and Weak* Convergence :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received July 1, 2015 :: Copyright (c) 2015-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 RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, DUALSP02, DUALSP03, PBOOLE, INT_1, NFCONT_1, CFCONT_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, SEQ_1, FUNCOP_1, FCONT_1, SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, NORMSP_1, FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, VALUED_1, METRIC_1, ASYMPT_1, PARTFUN1, RCOMP_1, NORMSP_2, RLVECT_3, NORMSP_3, TOPS_1, TOPGEN_1, VALUED_0; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0, COMPLEX1, XXREAL_2, VALUED_1, SEQ_1, SEQ_2, SEQ_4, RINFSUP1, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLSUB_1, RLVECT_3, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, NORMSP_2, LOPBAN_5, DUALSP01, NORMSP_3, DUALSP02; constructors REAL_1, EUCLID, REALSET1, RSSPACE3, BINOP_2, SEQ_1, NFCONT_1, RELSET_1, SEQ_2, SEQ_4, HAHNBAN1, NORMSP_2, RLVECT_3, LOPBAN_5, COMSEQ_2, NORMSP_3, TOPS_1, DUALSP02, RINFSUP1, CARD_3; registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1, XXREAL_0, VALUED_0, FUNCT_2, VALUED_1, FUNCOP_1, SEQ_4, RELSET_1, FUNCT_1, NORMSP_3, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, SEQ_2, DUALSP01, XBOOLE_0, SEQM_3, INT_1, PRE_TOPC, NORMSP_4; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Some properties about Dual Spaces of Real Normed Spaces definition let X be non empty set; let F be sequence of Funcs(NAT,X); let k be Nat; redefine func F.k -> sequence of X; end; theorem :: DUALSP03:1 for X be strict RealNormSpace, A be non empty Subset of X holds (for f be Point of DualSp X st (for x be Point of X st x in A holds (Bound2Lipschitz(f,X)).x = 0) holds Bound2Lipschitz(f,X) = 0.(DualSp X)) implies ClNLin(A) = X; theorem :: DUALSP03:2 for X be strict RealNormSpace st DualSp X is separable holds X is separable; theorem :: DUALSP03:3 for x be Real, x1 be Point of RNS_Real st x=x1 holds -x = -x1; theorem :: DUALSP03:4 for x,y be Real, x1,y1 be Point of RNS_Real st x=x1 & y=y1 holds x-y = x1-y1; theorem :: DUALSP03:5 for seq be Real_Sequence, seq1 be sequence of RNS_Real st seq = seq1 holds seq is convergent iff seq1 is convergent; theorem :: DUALSP03:6 for seq be Real_Sequence, seq1 be sequence of RNS_Real st seq = seq1 & seq is convergent holds lim seq = lim seq1; theorem :: DUALSP03:7 for seq1 be sequence of RNS_Real st seq1 is Cauchy_sequence_by_Norm holds seq1 is convergent; registration cluster RNS_Real -> complete; end; definition let X be RealNormSpace, g be sequence of DualSp X, x be Point of X; func g#x -> Real_Sequence means :: DUALSP03:def 1 for i be Nat holds it.i = (g.i).x; end; begin :: Weak Convergence and Weak* Convergence definition let X be RealNormSpace, x be sequence of X; attr x is weakly-convergent means :: DUALSP03:def 2 ex x0 be Point of X st for f be Lipschitzian linear-Functional of X holds f*x is convergent & lim (f*x) = f.x0; end; theorem :: DUALSP03:8 for X be RealNormSpace, x be sequence of X st rng x c= {0.X} holds x is weakly-convergent; definition let X be RealNormSpace, x be sequence of X; assume x is weakly-convergent; func w-lim x -> Point of X means :: DUALSP03:def 3 for f be Lipschitzian linear-Functional of X holds f*x is convergent & lim (f*x) = f.it; end; theorem :: DUALSP03:9 for X be RealNormSpace, x be sequence of X st x is convergent holds x is weakly-convergent & w-lim x = lim x; theorem :: DUALSP03:10 for X be RealNormSpace, x be sequence of X st X is non trivial & x is weakly-convergent holds ||.x.|| is bounded & ||. w-lim x .|| <= lim_inf ||.x.|| & w-lim x in ClNLin(rng x); definition let X be RealNormSpace, g be sequence of DualSp X; attr g is weakly*-convergent means :: DUALSP03:def 4 ex g0 be Point of DualSp X st for x be Point of X holds g#x is convergent & lim (g#x) = g0.x; end; definition let X be RealNormSpace, g be sequence of DualSp X; assume g is weakly*-convergent; func w*-lim g -> Point of DualSp X means :: DUALSP03:def 5 for x be Point of X holds g#x is convergent & lim (g#x) = it.x; end; theorem :: DUALSP03:11 for X be RealNormSpace, g be sequence of DualSp X st g is convergent holds g is weakly*-convergent & w*-lim g = lim g; theorem :: DUALSP03:12 for X be RealNormSpace, f be sequence of DualSp X st f is weakly-convergent holds f is weakly*-convergent; theorem :: DUALSP03:13 for X be RealNormSpace, f be sequence of DualSp X st X is Reflexive holds f is weakly-convergent iff f is weakly*-convergent; theorem :: DUALSP03:14 for X be RealBanachSpace, T be Subset of DualSp X st ( for x be Point of X ex K be Real st 0 <= K & for f be Point of DualSp X st f in T holds |. f.x .| <= K ) holds ex L be Real st 0 <= L & for f be Point of DualSp X st f in T holds ||.f.|| <= L; theorem :: DUALSP03:15 for X be RealBanachSpace, f be sequence of DualSp X st f is weakly*-convergent holds ||.f.|| is bounded & ||. w*-lim f .|| <= lim_inf ||.f.||; theorem :: DUALSP03:16 for X be RealNormSpace, x be Point of X, vseq be sequence of DualSp X, vseq1 be sequence of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real) st vseq = vseq1 holds vseq#x = vseq1#x; theorem :: DUALSP03:17 for X be RealBanachSpace, X0 be Subset of X, vseq be sequence of DualSp X st ||.vseq.|| is bounded & X0 is dense & (for x be Point of X st x in X0 holds vseq#x is convergent) holds vseq is weakly*-convergent; theorem :: DUALSP03:18 for X be RealBanachSpace, f be sequence of DualSp X holds f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 be Subset of X st X0 is dense & (for x be Point of X st x in X0 holds f#x is convergent) ); begin :: Weak Sequential Compactness of Real Banach Spaces definition let X be RealNormSpace, X0 be non empty Subset of X; attr X0 is weakly-sequentially-compact means :: DUALSP03:def 6 for seq be sequence of X0 ex seq1 be sequence of X st seq1 is subsequence of seq & seq1 is weakly-convergent & w-lim seq1 in X; end; theorem :: DUALSP03:19 for X be RealNormSpace, x be sequence of X st X is Reflexive holds x is weakly-convergent iff (BidualFunc X)*x is weakly*-convergent; theorem :: DUALSP03:20 for X be RealNormSpace, f be sequence of DualSp X, x be Point of X st ||.f.|| is bounded holds ex f0 be sequence of DualSp X st f0 is subsequence of f & ||.f0.|| is bounded & f0#x is convergent; theorem :: DUALSP03:21 for X be RealNormSpace, f be sequence of DualSp X, x be Point of X st ||.f.|| is bounded holds ex f0 be sequence of DualSp X st f0 is subsequence of f & ||.f0.|| is bounded & f0#x is convergent & f0#x is subsequence of f#x; theorem :: DUALSP03:22 for X be RealNormSpace, f be sequence of DualSp X, x be Point of X st ||.f.|| is bounded holds ex f0 be sequence of DualSp X, N be increasing sequence of NAT st f0 is subsequence of f & ||.f0.|| is bounded & f0#x is convergent & f0#x is subsequence of f#x & f0 = f*N; theorem :: DUALSP03:23 for X be RealNormSpace, f be sequence of DualSp X, x be sequence of X st ||.f.|| is bounded holds ex F be sequence of Funcs(NAT,the carrier of DualSp X) st F.0 is subsequence of f & (F.0)#(x.0) is convergent & ( for k be Nat holds F.(k+1) is subsequence of F.k ) & ( for k be Nat holds (F.(k+1))#(x.(k+1)) is convergent); theorem :: DUALSP03:24 for X be RealNormSpace, f be sequence of DualSp X, x be sequence of X st ||.f.|| is bounded holds ex F be sequence of Funcs(NAT,the carrier of DualSp X), N be sequence of Funcs(NAT,NAT) st F.0 is subsequence of f & (F.0)#(x.0) is convergent & N.0 is increasing sequence of NAT & F.0 = f*N.0 & (for k be Nat holds F.(k+1) is subsequence of F.k) & (for k be Nat holds (F.(k+1))#(x.(k+1)) is convergent) & (for k be Nat holds (F.(k+1))#(x.(k+1)) is subsequence of (F.k)#(x.(k+1))) & (for k be Nat holds N.(k+1) is increasing sequence of NAT) & for k be Nat holds F.(k+1) = (F.k)*N.(k+1); theorem :: DUALSP03:25 for X be RealNormSpace, f be sequence of DualSp X, x be sequence of X st ||.f.|| is bounded holds ex M be sequence of DualSp X st M is subsequence of f & for k be Nat holds M#(x.k) is convergent; theorem :: DUALSP03:26 for X be RealBanachSpace, f be sequence of DualSp X st X is separable & ||.f.|| is bounded holds ex f0 be sequence of DualSp X st f0 is subsequence of f & f0 is weakly*-convergent; theorem :: DUALSP03:27 for X be RealBanachSpace, x be sequence of X st X is Reflexive & ||.x.|| is bounded holds ex x0 be sequence of X st x0 is subsequence of x & x0 is weakly-convergent; theorem :: DUALSP03:28 for X be RealBanachSpace, X0 be non empty Subset of X st X is non trivial Reflexive holds X0 is weakly-sequentially-compact iff ex S be non empty Subset of REAL st S = {||.x.|| where x is Point of X : x in X0} & S is bounded_above;