:: The Orthogonal Projection and {R}iesz Representation Theorem :: 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, PROB_2, NFCONT_1, CFCONT_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, REALSET1, SEQ_1, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, VALUED_1, METRIC_1, RELAT_2, ASYMPT_1, FUNCT_7, PARTFUN1, RCOMP_1, BHSP_1, RSSPACE2, DUALSP04, RUSUB_5, SQUARE_1, RVSUM_1, BHSP_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, REALSET1, NUMBERS, XCMPLX_0, SQUARE_1, XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, RLSUB_1, RUSUB_1, RUSUB_5, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, RSSPACE2, BHSP_6, RSSPACE3, LOPBAN_1, NFCONT_1, DUALSP01; constructors REAL_1, REALSET1, RSSPACE3, LOPBAN_2, SEQ_1, NFCONT_1, DUALSP01, RELSET_1, SEQ_2, SEQ_4, HAHNBAN1, COMSEQ_2, BHSP_2, BHSP_3, RUSUB_5, SQUARE_1, BHSP_6; registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1, XXREAL_0, VALUED_0, RLVECT_1, FUNCT_2, VALUED_1, FUNCOP_1, RELSET_1, NORMSP_3, XCMPLX_0, NAT_1, NORMSP_1, SEQ_2, DUALSP01, XBOOLE_0, SQUARE_1, RUSUB_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Preliminaries definition let X be RealUnitarySpace; func normRU X -> Function of the carrier of X,REAL means :: DUALSP04:def 1 for x be Point of X holds it.x = ||.x.||; end; definition let X be RealUnitarySpace; func RUSp2RNSp X -> RealNormSpace equals :: DUALSP04:def 2 NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, normRU X #); end; theorem :: DUALSP04:1 for X be RealUnitarySpace, x be Point of X, x1 be Point of RUSp2RNSp X st x=x1 holds -x = -x1; theorem :: DUALSP04:2 for X be RealUnitarySpace, x,y be Point of X, x1,y1 be Point of RUSp2RNSp X st x=x1 & y=y1 holds x - y = x1 - y1; theorem :: DUALSP04:3 for X be RealUnitarySpace, x be Point of X, x1 be Point of RUSp2RNSp X st x=x1 holds ||.x.|| = ||.x1.||; theorem :: DUALSP04:4 for X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of RUSp2RNSp X st s1 = s2 holds s1 is convergent iff s2 is convergent; theorem :: DUALSP04:5 for X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of RUSp2RNSp X st s1 = s2 & s1 is convergent holds lim s1 = lim s2; theorem :: DUALSP04:6 for X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of RUSp2RNSp X st s1 = s2 holds s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy; theorem :: DUALSP04:7 for X be RealUnitarySpace holds X is complete iff RUSp2RNSp X is complete; registration let X be RealHilbertSpace; cluster RUSp2RNSp X -> complete; end; definition let X be RealUnitarySpace, Y be Subset of X; attr Y is open means :: DUALSP04:def 3 ex Z be Subset of RUSp2RNSp X st Z = Y & Z is open; end; definition let X be RealUnitarySpace, Y be Subset of X; attr Y is closed means :: DUALSP04:def 4 ex Z be Subset of RUSp2RNSp X st Z = Y & Z is closed; end; theorem :: DUALSP04:8 for X be RealUnitarySpace, Y be Subset of X holds Y is closed iff for s be sequence of X st rng s c= Y & s is convergent holds lim s in Y; theorem :: DUALSP04:9 for X be RealUnitarySpace, Y be Subset of X holds Y is open iff Y` is closed; definition let X be RealUnitarySpace; let f be PartFunc of the carrier of X,REAL; let x0 be Point of X; pred f is_continuous_in x0 means :: DUALSP04:def 5 x0 in dom f & for s1 be sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds f/*s1 is convergent & f/.x0 = lim (f/*s1); end; definition let X be RealUnitarySpace; let f be PartFunc of the carrier of X,REAL; let Y be set; pred f is_continuous_on Y means :: DUALSP04:def 6 Y c= dom f & for x0 be Point of X st x0 in Y holds f|Y is_continuous_in x0; end; theorem :: DUALSP04:10 for X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL, x0 be Point of X, y0 be Point of RUSp2RNSp X st f=g & x0=y0 holds f is_continuous_in x0 iff g is_continuous_in y0; theorem :: DUALSP04:11 for X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL st f=g holds f is_continuous_on the carrier of X iff g is_continuous_on the carrier of RUSp2RNSp X; theorem :: DUALSP04:12 for X be RealUnitarySpace, w be Point of X, f be Function of X,REAL st for v be Point of X holds f.v = w .|. v holds f is_continuous_on the carrier of X; definition let X be RealUnitarySpace; let Y be set; let f be PartFunc of the carrier of X,REAL; pred f is_Lipschitzian_on Y means :: DUALSP04:def 7 Y c= dom f & ex r be Real st 0 < r & for x1, x2 be Point of X st x1 in Y & x2 in Y holds |.f/.x1 - f/.x2.| <= r * ||.x1 - x2.||; end; theorem :: DUALSP04:13 for X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL st f=g holds f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of RUSp2RNSp X; theorem :: DUALSP04:14 for X be RealUnitarySpace, f be Function of X,REAL st f is_Lipschitzian_on the carrier of X holds f is_continuous_on the carrier of X; theorem :: DUALSP04:15 for X be RealUnitarySpace, F be linear-Functional of X st F = (the carrier of X) --> 0 holds F is Lipschitzian; registration let X be RealUnitarySpace; cluster Lipschitzian for linear-Functional of X; end; definition let X be RealUnitarySpace; func BoundedLinearFunctionals X -> Subset of X*' means :: DUALSP04:def 8 for x be set holds x in it iff x is Lipschitzian linear-Functional of X; end; registration let X be RealUnitarySpace; cluster BoundedLinearFunctionals X -> non empty linearly-closed; end; definition let X be RealUnitarySpace; let f be object; func Bound2Lipschitz(f,X) -> Lipschitzian linear-Functional of X equals :: DUALSP04:def 9 In(f,BoundedLinearFunctionals X); end; definition let X be RealUnitarySpace; let u be linear-Functional of X; func PreNorms u -> non empty Subset of REAL equals :: DUALSP04:def 10 {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 }; end; registration let X be RealUnitarySpace, g be Lipschitzian linear-Functional of X; cluster PreNorms g -> bounded_above; end; definition let X be RealUnitarySpace; func BoundedLinearFunctionalsNorm X -> Function of BoundedLinearFunctionals X,REAL means :: DUALSP04:def 11 for x be object st x in BoundedLinearFunctionals X holds it.x = upper_bound PreNorms(Bound2Lipschitz(x,X)); end; registration let X be RealUnitarySpace; let f be Lipschitzian linear-Functional of X; reduce Bound2Lipschitz(f,X) to f; end; theorem :: DUALSP04:16 for X be RealUnitarySpace, f be Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms f; definition let X be RealUnitarySpace; func DualSp X -> non empty NORMSTR equals :: DUALSP04:def 12 NORMSTR (# BoundedLinearFunctionals X, Zero_(BoundedLinearFunctionals X, X*'), Add_(BoundedLinearFunctionals X, X*'), Mult_(BoundedLinearFunctionals X, X*'), BoundedLinearFunctionalsNorm X #); end; theorem :: DUALSP04:17 for X be RealUnitarySpace, f be Point of DualSp X, g be Lipschitzian linear-Functional of X st g=f holds for t be VECTOR of X holds |.g.t.| <= ||.f.|| * ||.t.||; theorem :: DUALSP04:18 for X be RealUnitarySpace, f be Point of DualSp X holds 0 <= ||.f.||; theorem :: DUALSP04:19 for X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL st f=g holds f is additive homogeneous iff g is additive homogeneous; theorem :: DUALSP04:20 for X be RealUnitarySpace, f be linear-Functional of X, g be linear-Functional of RUSp2RNSp X st f=g holds f is Lipschitzian iff g is Lipschitzian; theorem :: DUALSP04:21 for X be RealUnitarySpace holds BoundedLinearFunctionals X = BoundedLinearFunctionals (RUSp2RNSp X); theorem :: DUALSP04:22 for X be RealUnitarySpace, u be linear-Functional of X, v be linear-Functional of (RUSp2RNSp X) st u=v holds PreNorms u = PreNorms v; theorem :: DUALSP04:23 for X be RealUnitarySpace holds BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X); theorem :: DUALSP04:24 for X be RealUnitarySpace holds LinearFunctionals X = LinearFunctionals (RUSp2RNSp X); theorem :: DUALSP04:25 for X be RealUnitarySpace holds X*' = (RUSp2RNSp X)*'; theorem :: DUALSP04:26 for X be RealUnitarySpace holds DualSp X = DualSp (RUSp2RNSp X); begin :: The Orthogonal Projection theorem :: DUALSP04:27 for X be RealUnitarySpace, M,N be Subspace of X st the carrier of M c= the carrier of N holds the carrier of Ort_Comp N c= the carrier of Ort_Comp M; theorem :: DUALSP04:28 for X be RealUnitarySpace, M be Subspace of X holds the carrier of M c= the carrier of Ort_Comp (Ort_Comp M); theorem :: DUALSP04:29 for X be RealUnitarySpace, M be Subspace of X, x be Point of X st x in (the carrier of M) /\ the carrier of (Ort_Comp M) holds x = 0.X; theorem :: DUALSP04:30 for X be RealUnitarySpace, M be Subspace of X, N be non empty Subset of X st N = the carrier of (Ort_Comp M) holds N is linearly-closed & N is closed; theorem :: DUALSP04:31 for X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X, d be Real st N = the carrier of M & N is closed & ( ex Y be non empty Subset of REAL st Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0) holds ex x0 be Point of X st d = ||.x-x0.|| & x0 in M; theorem :: DUALSP04:32 for X be RealHilbertSpace, M be Subspace of X, x,x0 be Point of X, d be Real st x0 in M & (ex Y be non empty Subset of REAL st Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0) holds d = ||.x-x0.|| iff for w be Point of X st w in M holds w, x-x0 are_orthogonal; theorem :: DUALSP04:33 for X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X st N = the carrier of M & N is closed holds ex y,z be Point of X st y in M & z in Ort_Comp M & x = y + z; theorem :: DUALSP04:34 for X be RealUnitarySpace, M be Subspace of X, x be Point of X, y1,y2,z1,z2 be Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds y1 = y2 & z1 = z2; begin :: F. Riesz Representation Theorem theorem :: DUALSP04:35 for X be RealUnitarySpace, f be linear-Functional of X, y be Point of X st for x be Point of X holds f.x = x .|. y holds f is Lipschitzian; registration let X be RealUnitarySpace, f be linear-Functional of X; cluster f"{0} -> non empty; end; theorem :: DUALSP04:36 for X be RealUnitarySpace, f be Function of X,REAL st f is additive homogeneous holds f"{0} is linearly-closed; definition let X be RealUnitarySpace, f be linear-Functional of X; func UKer(f) -> strict Subspace of X means :: DUALSP04:def 13 the carrier of it = f"{0}; end; theorem :: DUALSP04:37 for X be RealUnitarySpace, f be linear-Functional of X st f is Lipschitzian holds f"{0} is closed; theorem :: DUALSP04:38 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V st v <> 0.V holds v in Ort_Comp W implies not v in W; theorem :: DUALSP04:39 for X be RealHilbertSpace, f be linear-Functional of X st f is Lipschitzian holds ex y be Point of X st for x be Point of X holds f.x = x .|. y; theorem :: DUALSP04:40 for X be RealUnitarySpace, f be linear-Functional of X holds for y1,y2 be Point of X st for x be Point of X holds f.x = x .|. y1 & f.x = x .|. y2 holds y1 = y2; theorem :: DUALSP04:41 for X be RealHilbertSpace, f be Point of DualSp X, g be Lipschitzian linear-Functional of X st g=f holds ex y be Point of X st (for x be Point of X holds g.x = x .|. y) & ||.f.|| = ||.y.||;