:: The Orthogonal Projection and {R}iesz Representation Theorem :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received July 1, 2015 :: Copyright (c) 2015 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; definitions ALGSTR_0, HAHNBAN, XXREAL_2, TARSKI; equalities RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0, SEQ_1, BHSP_1, DUALSP01; expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, SEQ_2, NORMSP_0, ORDINAL1, NORMSP_1, STRUCT_0, RLVECT_1, XXREAL_2, BHSP_1, MEMBERED, NFCONT_1, DUALSP01; theorems SEQ_4, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, HAHNBAN, RSSPACE, ORDINAL1, NAT_1, BHSP_1, BHSP_2, BHSP_3, SUBSET_1, NFCONT_1, XXREAL_2, DUALSP01, XCMPLX_1, RUSUB_5, SQUARE_1, RUSUB_1, BHSP_6; schemes FUNCT_2, XBOOLE_0; begin :: Preliminaries definition let X be RealUnitarySpace; func normRU X -> Function of the carrier of X,REAL means :Def1: for x be Point of X holds it.x = ||.x.||; existence proof deffunc F(Element of the carrier of X) = ||.$1.||; X0: for x be Element of the carrier of X holds F(x) in REAL by XREAL_0:def 1; consider f be Function of the carrier of X,REAL such that X1: for x be Element of the carrier of X holds f.x = F(x) from FUNCT_2:sch 8(X0); take f; thus thesis by X1; end; uniqueness proof let f1,f2 be Function of the carrier of X, REAL such that A1: for x be Point of X holds f1.x = ||.x.|| and A2: for x be Point of X holds f2.x = ||.x.||; now let x be Element of the carrier of X; thus f1.x = ||.x.|| by A1 .= f2.x by A2; end; hence f1=f2; end; end; Lm01: for X be RealUnitarySpace holds NORMSTR (# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, normRU X #) is non empty RealNormSpace proof let X be RealUnitarySpace; set T=NORMSTR (# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, normRU X #); reconsider T as non empty NORMSTR; now let v,w be Element of T; reconsider v1 = v, w1 = w as Element of X; thus v + w = v1 + w1 .= w1 + v1 .= w + v; end; then A1:T is Abelian; now let u,v,w be Element of T; reconsider u1 = u, v1 = v, w1 = w as Element of X; thus (u + v) + w = (u1 + v1) + w1 .= u1 + (v1 + w1) by RLVECT_1:def 3 .= u + (v + w); end; then A2:T is add-associative; now let v be Element of T; reconsider v1 = v as Element of X; thus v + 0.T = v1 + 0.X .= v; end; then A3:T is right_zeroed; A4:T is right_complementable proof let v be Element of T; reconsider v1 = v as Element of X; reconsider w1 = -v1 as Element of X; reconsider w = w1 as Element of T; take w; thus v + w = v1 + w1 .= 0.X by RLVECT_1:def 10 .= 0.T; end; now let a,b be Real, v be Element of T; reconsider v1=v as Element of X; thus (a + b) * v = (a + b) * v1 .= a * v1 + b * v1 by RLVECT_1:def 6 .= a * v + b * v; end; then A5:T is scalar-distributive; now let a be Real, v,w be Element of T; reconsider v1 = v, w1 = w as Element of X; thus a * (v + w) = a * (v1 + w1) .= a * v1 + a * w1 by RLVECT_1:def 5 .= a * v + a * w; end; then A6:T is vector-distributive; now let a,b be Real, v be Element of T; reconsider v1=v as Element of X; thus (a * b) * v = (a * b) * v1 .= a * (b * v1) by RLVECT_1:def 7 .= a * (b * v); end; then A7:T is scalar-associative; now let v be Element of T; reconsider v1=v as Element of X; thus 1 * v = 1 * v1 .= v by RLVECT_1:def 8; end; then A8:T is scalar-unital; ||.0.X.|| = 0 by SQUARE_1:17,BHSP_1:1; then A9:T is reflexive by Def1; now let v be Element of T; assume AS: ||.v.|| = 0; reconsider v1=v as Element of X; ||.v1.|| = 0 by AS,Def1; then v1 = 0.X by BHSP_1:26; hence v = 0.T; end; then A10: T is discerning; now let a be Real, v,w be Element of T; reconsider v1 = v, w1 = w as Element of X; thus ||.a*v.|| = ||.a*v1.|| by Def1 .= |.a.| * ||.v1.|| by BHSP_1:27 .= |.a.| * ||.v.|| by Def1; C3: ||.v + w.|| = ||.v1 + w1.|| by Def1; ||.v.|| + ||.w.|| = ||.v1.|| + (normRU X).w by Def1 .= ||.v1.|| + ||.w1.|| by Def1; hence ||.v + w.|| <= ||.v.|| + ||.w.|| by C3,BHSP_1:30; end; then T is RealNormSpace-like; hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10; end; definition let X be RealUnitarySpace; func RUSp2RNSp X -> RealNormSpace equals NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, normRU X #); correctness by Lm01; end; theorem RHS3: for X be RealUnitarySpace, x be Point of X, x1 be Point of RUSp2RNSp X st x=x1 holds -x = -x1 proof let X be RealUnitarySpace, x be Point of X, x1 be Point of RUSp2RNSp X; assume AS: x=x1; thus -x = (-1) * x by RLVECT_1:16 .= (-1) * x1 by AS .= -x1 by RLVECT_1:16; end; theorem RHS4: 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 by RHS3; theorem RHS6: for X be RealUnitarySpace, x be Point of X, x1 be Point of RUSp2RNSp X st x=x1 holds ||.x.|| = ||.x1.|| by Def1; theorem RHS8: 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 proof let X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of RUSp2RNSp X; assume AS: s1 = s2; hereby assume P1: s1 is convergent; reconsider g1=lim s1 as Point of RUSp2RNSp X; now let p be Real; assume 0 < p; then consider m be Nat such that P2: for n be Nat st m <= n holds ||.s1.n - lim s1.|| < p by P1,BHSP_2:19; take m; thus for n be Nat st m <= n holds ||.s2.n - g1.|| < p proof let n be Nat; assume m <= n; then P3: ||.s1.n - lim s1 .|| < p by P2; s1.n - lim s1 = s2.n - g1 by AS,RHS3; hence ||.s2.n - g1.|| < p by P3,Def1; end; end; hence s2 is convergent; end; assume P4: s2 is convergent; reconsider g2=lim s2 as Point of X; now let p be Real; assume 0 < p; then consider m be Nat such that P2: for n be Nat st m <= n holds ||.s2.n - lim s2 .|| < p by P4,NORMSP_1:def 7; take m; thus for n be Nat st m <= n holds ||.s1.n - g2.|| < p proof let n be Nat; assume m <= n; then P3: ||.s2.n - lim s2 .|| < p by P2; s2.n - lim s2 = s1.n - g2 by AS,RHS3; hence ||.s1.n - g2.|| < p by P3,Def1; end; end; hence s1 is convergent by BHSP_2:9; end; theorem RHS9: 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 proof let X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of RUSp2RNSp X; assume AS: s1 = s2; assume P1: s1 is convergent; then P5: s2 is convergent by AS,RHS8; reconsider g1=lim s1 as Point of RUSp2RNSp X; now let p be Real; assume 0 < p; then consider m be Nat such that P2: for n be Nat st m <= n holds ||.s1.n - lim s1.|| < p by P1,BHSP_2:19; take m; thus for n be Nat st m <= n holds ||.s2.n - g1.|| < p proof let n be Nat; assume m <= n; then P3: ||.s1.n - lim s1.|| < p by P2; s1.n - lim s1 = s2.n - g1 by AS,RHS3; hence ||.s2.n - g1.|| < p by P3,Def1; end; end; hence lim s2 = lim s1 by P5,NORMSP_1:def 7; end; theorem RHS11a: 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 proof let X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of RUSp2RNSp X; assume A0: s1 = s2; hereby assume AS: s2 is Cauchy_sequence_by_Norm; for r be Real st 0 < r ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.s1.n - s1.m.|| < r proof let r be Real; assume 0 < r; then consider k be Nat such that P1: for n, m be Nat st n >= k & m >= k holds ||.s2.n - s2.m.|| < r by AS,RSSPACE3:8; take k; thus for n, m be Nat st n >= k & m >= k holds ||.s1.n - s1.m.|| < r proof let n, m be Nat; assume n >= k & m >= k; then P2: ||.s2.n - s2.m.|| < r by P1; s2.n - s2.m = s1.n - s1.m by A0,RHS3; hence ||.s1.n - s1.m.|| < r by Def1,P2; end; end; hence s1 is Cauchy by BHSP_3:2; end; assume A1: s1 is Cauchy; for r be Real st r > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.s2.n - s2.m.|| < r proof let r be Real; assume r > 0; then consider k be Nat such that A2: for n, m be Nat st n >= k & m >= k holds ||.s1.n - s1.m.|| < r by A1,BHSP_3:2; take k; thus for n, m be Nat st n >= k & m >= k holds ||.s2.n - s2.m.|| < r proof let n, m be Nat; assume n >= k & m >= k; then A3: ||.s1.n - s1.m.|| < r by A2; s1.n - s1.m = s2.n - s2.m by A0,RHS3; hence ||.s2.n - s2.m.|| < r by Def1,A3; end; end; hence s2 is Cauchy_sequence_by_Norm by RSSPACE3:8; end; theorem RHS11b: for X be RealUnitarySpace holds X is complete iff RUSp2RNSp X is complete proof let X be RealUnitarySpace; set Y = RUSp2RNSp X; hereby assume AS1: X is complete; for s2 be sequence of Y holds s2 is Cauchy_sequence_by_Norm implies s2 is convergent proof let s2 be sequence of Y; reconsider s1=s2 as sequence of X; assume s2 is Cauchy_sequence_by_Norm; then s1 is Cauchy by RHS11a; then s1 is convergent by AS1,BHSP_3:def 4; hence s2 is convergent by RHS8; end; hence Y is complete by LOPBAN_1:def 15; end; assume AS2: Y is complete; for s1 be sequence of X holds s1 is Cauchy implies s1 is convergent proof let s1 be sequence of X; reconsider s2=s1 as sequence of Y; assume s1 is Cauchy; then s2 is Cauchy_sequence_by_Norm by RHS11a; then s2 is convergent by AS2,LOPBAN_1:def 15; hence s1 is convergent by RHS8; end; hence X is complete by BHSP_3:def 4; end; registration let X be RealHilbertSpace; cluster RUSp2RNSp X -> complete; correctness by RHS11b; end; definition let X be RealUnitarySpace, Y be Subset of X; attr Y is open means 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 ex Z be Subset of RUSp2RNSp X st Z = Y & Z is closed; end; theorem LM1: 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 proof let X be RealUnitarySpace, Y be Subset of X; hereby assume Y is closed; then consider Z be Subset of RUSp2RNSp X such that A1: Z = Y & Z is closed; thus for s be sequence of X st rng s c= Y & s is convergent holds lim s in Y proof let s be sequence of X; assume A3: rng s c= Y & s is convergent; reconsider s1=s as sequence of RUSp2RNSp X; rng s1 c= Z & s1 is convergent by A3,A1,RHS8; then lim s1 in Z by A1; hence lim s in Y by A1,A3,RHS9; end; end; assume A4: for s be sequence of X st rng s c= Y & s is convergent holds lim s in Y; reconsider Z=Y as Subset of RUSp2RNSp X; for s1 be sequence of RUSp2RNSp X st rng s1 c= Z & s1 is convergent holds lim s1 in Z proof let s1 be sequence of RUSp2RNSp X; assume A5: rng s1 c= Z & s1 is convergent; reconsider s=s1 as sequence of X; A6: rng s c= Y & s is convergent by A5,RHS8; then lim s in Y by A4; hence lim s1 in Z by A6,RHS9; end; then Z is closed; hence Y is closed; end; theorem for X be RealUnitarySpace, Y be Subset of X holds Y is open iff Y` is closed proof let X be RealUnitarySpace, Y be Subset of X; thus Y is open implies Y` is closed; assume Y` is closed; then consider Z be Subset of RUSp2RNSp X such that A2: Z = Y` & Z is closed; Z` is open by A2; hence Y is open by A2; end; 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 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 Y c= dom f & for x0 be Point of X st x0 in Y holds f|Y is_continuous_in x0; end; theorem LM3B: 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 proof let 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; assume AS: f=g & x0=y0; set Y=RUSp2RNSp X; hereby assume A11: f is_continuous_in x0; for s2 be sequence of Y st rng s2 c= dom g & s2 is convergent & lim s2 = y0 holds g/*s2 is convergent & g/.y0 = lim (g/*s2) proof let s2 be sequence of Y; assume AS1: rng s2 c= dom g & s2 is convergent & lim s2 = y0; reconsider s1=s2 as sequence of X; B2: s1 is convergent by AS1,RHS8; then lim s1 = x0 by AS1,AS,RHS9; hence g/*s2 is convergent & g/.y0 = lim (g/*s2) by AS,A11,AS1,B2; end; hence g is_continuous_in y0 by A11,AS; end; assume A31: g is_continuous_in y0; 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) proof let s1 be sequence of X; assume AS2: rng s1 c= dom f & s1 is convergent & lim s1 = x0; reconsider s2=s1 as sequence of Y; B2: s2 is convergent by AS2,RHS8; lim s2 = y0 by AS,AS2,RHS9; hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by AS,A31,AS2,B2; end; hence f is_continuous_in x0 by A31,AS; end; theorem LM3C: 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 proof let X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL; assume AS: f=g; set Y=RUSp2RNSp X; hereby assume A11: f is_continuous_on the carrier of X; for y0 be Point of Y st y0 in the carrier of Y holds g| (the carrier of Y) is_continuous_in y0 proof let y0 be Point of Y; assume y0 in the carrier of Y; reconsider x0=y0 as Point of X; f| (the carrier of X) is_continuous_in x0 by A11; hence thesis by LM3B,AS; end; hence g is_continuous_on the carrier of Y by A11,AS; end; assume A31: g is_continuous_on the carrier of Y; for x0 be Point of X st x0 in the carrier of X holds f| (the carrier of X) is_continuous_in x0 proof let x0 be Point of X; assume x0 in the carrier of X; reconsider y0=x0 as Point of Y; g| (the carrier of Y) is_continuous_in y0 by A31; hence thesis by LM3B,AS; end; hence thesis by A31,AS; end; theorem 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 proof let X be RealUnitarySpace, w be Point of X, f be Function of X, REAL; assume AS: for v be Point of X holds f.v = w .|. v; set Y=RUSp2RNSp X; reconsider g=f as Function of Y,REAL; A3: dom g = the carrier of Y by FUNCT_2:def 1; for y0 be Point of Y st y0 in the carrier of Y holds g| (the carrier of Y) is_continuous_in y0 proof let y0 be Point of Y; assume y0 in the carrier of Y; for r be Real st 0 < r ex s be Real st 0 < s & for y1 be Point of Y st y1 in dom g & ||. y1- y0 .|| < s holds |. g/.y1 - g/.y0 .| < r proof let r be Real; assume AS1: 0 < r; thus ex s be Real st 0 < s & for y1 be Point of Y st y1 in dom g & ||. y1 - y0 .|| < s holds |. g/.y1 - g/.y0 .| < r proof C1: 0 <= ||.w.|| by BHSP_1:28; reconsider s=r/(||.w.|| + 1) as Real; C41: ||.w.|| + 0 < ||.w.|| + 1 by XREAL_1:8; s*(||.w.|| + 1) = r by C1,XCMPLX_1:87; then C5: 0 < s & s*||.w.|| < r by C1,AS1,C41,XREAL_1:68; C6: for y1 be Point of Y st y1 in dom g & ||. y1 - y0 .|| < s holds |. g/.y1 - g/.y0 .| < r proof let y1 be Point of Y; assume AS2: y1 in dom g & ||. y1 - y0 .|| < s; reconsider x1=y1 as Point of X; reconsider x0=y0 as Point of X; X0: ||. y1 - y0 .|| = ||. x1 - x0 .|| by RHS4,RHS6; D1: |. g/.y1 - g/.y0 .| = |. w .|. x1 - g.y0 .| by AS .= |. w .|. x1 - w .|. x0 .| by AS .= |. w .|. (x1 - x0) .| by BHSP_1:12; D2: |. w .|. (x1 - x0) .| <= ||.w.||*||.x1 - x0.|| by BHSP_1:29; ||.w.||*||.x1 - x0.|| <= ||.w.||*s by X0,C1,AS2,XREAL_1:64; then |. g/.y1 - g/.y0 .| <= ||.w.||*s by D1,D2,XXREAL_0:2; hence |. g/.y1 - g/.y0 .| < r by C5,XXREAL_0:2; end; take s; thus thesis by C1,AS1,C6; end; end; hence g| (the carrier of Y) is_continuous_in y0 by A3,NFCONT_1:8; end; then g is_continuous_on the carrier of Y by FUNCT_2:def 1; hence thesis by LM3C; end; 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 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 LM4: 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 proof let X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL; assume AS: f=g; set Y=RUSp2RNSp X; thus f is_Lipschitzian_on the carrier of X implies g is_Lipschitzian_on the carrier of RUSp2RNSp X proof assume A11: f is_Lipschitzian_on the carrier of X; then consider r be Real such that A2: 0 < r & for x1, x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds |.f/.x1 - f/.x2.| <= r * ||.x1 - x2.||; for y1, y2 be Point of Y st y1 in the carrier of Y & y2 in the carrier of Y holds |.g/.y1 - g/.y2.| <= r * ||.y1 - y2.|| proof let y1, y2 be Point of Y; assume y1 in the carrier of Y & y2 in the carrier of Y; reconsider x1=y1,x2=y2 as Point of X; ||.y1 - y2.|| = ||.x1 - x2.|| by RHS4,RHS6; hence |.g/.y1 - g/.y2.| <= r * ||.y1 - y2.|| by A2,AS; end; hence g is_Lipschitzian_on the carrier of Y by A2,A11,AS; end; assume A11: g is_Lipschitzian_on the carrier of Y; then consider r be Real such that A2: 0 < r & for y1, y2 be Point of Y st y1 in the carrier of Y & y2 in the carrier of Y holds |.g/.y1 - g/.y2.| <= r * ||.y1 - y2.||; for x1, x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds |.f/.x1 - f/.x2.| <= r * ||.x1 - x2.|| proof let x1, x2 be Point of X; assume x1 in the carrier of X & x2 in the carrier of X; reconsider y1=x1,y2=x2 as Point of Y; ||.x1 - x2.|| = ||.y1 - y2.|| by RHS4,RHS6; hence |.f/.x1 - f/.x2.| <= r * ||.x1 - x2.|| by A2,AS; end; hence thesis by A2,A11,AS; end; theorem LM5: 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 proof let X be RealUnitarySpace, f be Function of X,REAL; assume AS: f is_Lipschitzian_on the carrier of X; reconsider g=f as Function of RUSp2RNSp X,REAL; set Y=RUSp2RNSp X; g is_Lipschitzian_on the carrier of Y by AS,LM4; then g is_continuous_on the carrier of Y by NFCONT_1:46; hence thesis by LM3C; end; Th16: for X be RealUnitarySpace, f be linear-Functional of X st (for x be VECTOR of X holds f.x = 0) holds f is Lipschitzian proof let X be RealUnitarySpace; let f be linear-Functional of X; assume A1: for x be VECTOR of X holds f.x = 0; for x be VECTOR of X holds |.f.x.| <= 1*||.x.|| proof let x be VECTOR of X; 0 <= ||.x.|| by BHSP_1:28; hence thesis by A1,COMPLEX1:44; end; hence thesis by BHSP_6:def 4; end; theorem Th21X: for X be RealUnitarySpace, F be linear-Functional of X st F = (the carrier of X) --> 0 holds F is Lipschitzian proof let X be RealUnitarySpace, F be linear-Functional of X; assume F = (the carrier of X) --> 0; then for x be VECTOR of X holds F.x = 0 by FUNCOP_1:7; hence thesis by Th16; end; registration let X be RealUnitarySpace; cluster Lipschitzian for linear-Functional of X; correctness proof set f = (the carrier of X) --> 0; reconsider f as linear-Functional of X by DUALSP01:9; f is Lipschitzian by Th21X; hence thesis; end; end; definition let X be RealUnitarySpace; func BoundedLinearFunctionals X -> Subset of X*' means :Def10: for x be set holds x in it iff x is Lipschitzian linear-Functional of X; existence proof defpred P[object] means $1 is Lipschitzian linear-Functional of X; consider IT be set such that A1: for x be object holds x in IT iff x in LinearFunctionals X & P[x] from XBOOLE_0:sch 1; take IT; for x be object st x in IT holds x in LinearFunctionals X by A1; hence IT is Subset of X*' by TARSKI:def 3; let x be set; thus x in IT implies x is Lipschitzian linear-Functional of X by A1; assume A2: x is Lipschitzian linear-Functional of X; then x in LinearFunctionals X by DUALSP01:def 6; hence thesis by A1,A2; end; uniqueness proof let X1,X2 be Subset of X*'; assume that A3: for x be set holds x in X1 iff x is Lipschitzian linear-Functional of X and A4: for x be set holds x in X2 iff x is Lipschitzian linear-Functional of X; now let x be object; assume x in X2; then x is Lipschitzian linear-Functional of X by A4; hence x in X1 by A3; end; then A5: X2 c= X1; now let x be object; assume x in X1; then x is Lipschitzian linear-Functional of X by A3; hence x in X2 by A4; end; then X1 c= X2; hence thesis by A5; end; end; Th17: for X be RealUnitarySpace holds BoundedLinearFunctionals X is linearly-closed proof let X be RealUnitarySpace; set W = BoundedLinearFunctionals X; A1: for v,u be VECTOR of X*' st v in W & u in W holds v + u in W proof let v,u be VECTOR of X*' such that A2: v in W & u in W; reconsider f=v+u as linear-Functional of X by DUALSP01:def 6; f is Lipschitzian proof reconsider v1=v, u1=u as Lipschitzian linear-Functional of X by A2,Def10; consider K2 be Real such that A4: 0 < K2 and A5: for x be Point of X holds |. v1.x .| <= K2*||. x .|| by BHSP_6:def 4; consider K1 be Real such that A6: 0 < K1 and A7: for x be Point of X holds |. u1.x .| <= K1*||. x .|| by BHSP_6:def 4; reconsider K3=K1+K2 as Real; now let x be VECTOR of X; A8: |. u1.x+v1.x .| <= |. u1.x .|+ |. v1.x .| by COMPLEX1:56; A9: |. v1.x .| <= K2*||. x .|| by A5; |. u1.x .| <= K1*||. x .|| by A7; then A10: |. u1.x .| + |. v1.x .| <= K1*||. x .|| +K2*||. x .|| by A9,XREAL_1:7; |. f.x .| =|. u1.x+v1.x .| by DUALSP01:12; hence |. f.x .| <= K3*||. x .|| by A8,A10,XXREAL_0:2; end; hence thesis by A4,A6,BHSP_6:def 4; end; hence thesis by Def10; end; for a be Real, v be VECTOR of X*' st v in W holds a * v in W proof let a be Real; let v be VECTOR of X*' such that A11: v in W; reconsider f=a*v as linear-Functional of X by DUALSP01:def 6; f is Lipschitzian proof reconsider v1=v as Lipschitzian linear-Functional of X by A11,Def10; consider K be Real such that A12: 0 < K and A13: for x be Point of X holds |. v1.x .| <= K*||. x .|| by BHSP_6:def 4; B12: 0 <=|.a.| by COMPLEX1:46; |.a.| + 0 < |.a.| + 1 by XREAL_1:8; then B2: |.a.|*K <= (|.a.|+1)*K by A12,XREAL_1:64; now let x be VECTOR of X; 0 <=|.a.| by COMPLEX1:46; then A15: |.a.|* |. v1.x .| <= |.a.|* (K*||. x .||) by A13,XREAL_1:64; |. a*v1.x .| = |.a.|* |. v1.x .| by COMPLEX1:65; then A16: |. f.x .| <= |.a.|* (K*||. x .||) by A15,DUALSP01:13; 0 <= ||.x.|| by BHSP_1:28; then (|.a.|*K)*||.x.|| <= ((|.a.|+1)*K)*||.x.|| by B2,XREAL_1:64; hence |. f.x .| <= ((|.a.|+1)*K)*||.x.|| by A16,XXREAL_0:2; end; hence thesis by B12,A12,BHSP_6:def 4; end; hence thesis by Def10; end; hence thesis by A1; end; registration let X be RealUnitarySpace; cluster BoundedLinearFunctionals X -> non empty linearly-closed; coherence proof set f = the Lipschitzian linear-Functional of X; f in BoundedLinearFunctionals X by Def10; hence thesis by Th17; end; end; definition let X be RealUnitarySpace; let f be object; func Bound2Lipschitz(f,X) -> Lipschitzian linear-Functional of X equals In(f,BoundedLinearFunctionals X); coherence by Def10; end; definition let X be RealUnitarySpace; let u be linear-Functional of X; func PreNorms u -> non empty Subset of REAL equals {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 }; coherence proof A1: now let x be object; now assume x in {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 }; then ex t be VECTOR of X st x=|.u.t.| & ||.t.|| <= 1; hence x in REAL by XREAL_0:def 1; end; hence x in {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 } implies x in REAL; end; ||.0.X.|| = 0 by SQUARE_1:17,BHSP_1:1; then |.u.(0.X).| in {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 }; hence thesis by A1,TARSKI:def 3; end; end; Th27X: for X be RealUnitarySpace, g be Lipschitzian linear-Functional of X holds PreNorms g is bounded_above proof let X be RealUnitarySpace; let g be Lipschitzian linear-Functional of X; consider K be Real such that A1: 0 < K & for x be VECTOR of X holds |. g.x .| <= K*||. x .|| by BHSP_6:def 4; take K; let r be ExtReal; assume r in PreNorms g; then consider t be VECTOR of X such that A3: r=|.g.t.| & ||.t.|| <= 1; A5: |.g.t.| <= K*||. t .|| by A1; K*||. t .|| <= K *1 by A1,A3,XREAL_1:64; hence r <= K by A3,A5,XXREAL_0:2; end; registration let X be RealUnitarySpace, g be Lipschitzian linear-Functional of X; cluster PreNorms g -> bounded_above; coherence by Th27X; end; definition let X be RealUnitarySpace; func BoundedLinearFunctionalsNorm X -> Function of BoundedLinearFunctionals X,REAL means :Def14: for x be object st x in BoundedLinearFunctionals X holds it.x = upper_bound PreNorms(Bound2Lipschitz(x,X)); existence proof deffunc F(object) = upper_bound PreNorms(Bound2Lipschitz($1,X)); A1: for z be object st z in BoundedLinearFunctionals X holds F(z) in REAL by XREAL_0:def 1; thus ex f be Function of BoundedLinearFunctionals X,REAL st for x be object st x in BoundedLinearFunctionals X holds f.x = F(x) from FUNCT_2:sch 2(A1); end; uniqueness proof let NORM1,NORM2 be Function of BoundedLinearFunctionals X,REAL such that A2: for x be object st x in BoundedLinearFunctionals X holds NORM1.x = upper_bound PreNorms(Bound2Lipschitz(x,X)) and A3: for x be object st x in BoundedLinearFunctionals X holds NORM2.x = upper_bound PreNorms(Bound2Lipschitz(x,X)); for z be object st z in BoundedLinearFunctionals X holds NORM1.z = NORM2.z proof let z be object such that A5: z in BoundedLinearFunctionals X; NORM1.z = upper_bound PreNorms(Bound2Lipschitz(z,X)) by A2,A5; hence thesis by A3,A5; end; hence thesis; end; end; Th23: for X be RealUnitarySpace, f be Lipschitzian linear-Functional of X holds Bound2Lipschitz(f,X) = f proof let X be RealUnitarySpace; let f be Lipschitzian linear-Functional of X; f in BoundedLinearFunctionals X by Def10; hence thesis by SUBSET_1:def 8; end; registration let X be RealUnitarySpace; let f be Lipschitzian linear-Functional of X; reduce Bound2Lipschitz(f,X) to f; reducibility by Th23; end; theorem Th24: for X be RealUnitarySpace, f be Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms f proof let X be RealUnitarySpace; let f be Lipschitzian linear-Functional of X; reconsider f9=f as set; thus (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms(Bound2Lipschitz(f9,X)) by Def14 .= upper_bound PreNorms f; end; definition let X be RealUnitarySpace; func DualSp X -> non empty NORMSTR equals NORMSTR (# BoundedLinearFunctionals X, Zero_(BoundedLinearFunctionals X, X*'), Add_(BoundedLinearFunctionals X, X*'), Mult_(BoundedLinearFunctionals X, X*'), BoundedLinearFunctionalsNorm X #); coherence; end; theorem Th26: 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.|| proof let X be RealUnitarySpace; let f be Point of DualSp X; let g be Lipschitzian linear-Functional of X such that A1: g=f; let t be VECTOR of X; per cases; suppose A3: t = 0.X; then A4: ||.t.|| = 0 by BHSP_1:26; g.t = g.(0 * 0.X) by A3 .= 0 * g.(0.X) by HAHNBAN:def 3 .= 0; hence |.g.t.| <= ||.f.||*||.t.|| by A4,COMPLEX1:44; end; suppose A5: t <> 0.X; reconsider t1 = ( ||.t.||")*t as VECTOR of X; A6: ||.t.|| <> 0 by A5,BHSP_1:26; then B61: 0 < ||.t.|| by BHSP_1:28; A7: |. ||.t.||".| = |. 1*||.t.||".| .= |. 1/||.t.||.| by XCMPLX_0:def 9 .= 1/||.t.|| by B61,ABSVALUE:def 1 .= 1*||.t.||" by XCMPLX_0:def 9 .= ||.t.||"; A8: |.g.t.|/||.t.|| = |.g.t.|*||.t.||" by XCMPLX_0:def 9 .=|. ||.t.||"*g.t.| by A7,COMPLEX1:65 .=|.g.t1.| by HAHNBAN:def 3; ||.t1.|| =|. ||.t.||".|*||.t.|| by BHSP_1:27 .=1 by A6,A7,XCMPLX_0:def 7; then |.g.t.|/||.t.|| in {|.g.s.| where s is VECTOR of X : ||.s.|| <= 1 } by A8; then |.g.t.|/||.t.|| <= upper_bound PreNorms g by SEQ_4:def 1; then A9: |.g.t.|/||.t.|| <= ||.f.|| by A1,Th24; A10: |.g.t.|/||.t.||*||.t.|| = |.g.t.|*||.t.||"*||.t.|| by XCMPLX_0:def 9 .=|.g.t.|*(||.t.||"*||.t.||) .=|.g.t.|*1 by A6,XCMPLX_0:def 7 .=|.g.t.|; 0 <= ||.t.|| by BHSP_1:28; hence |.g.t.| <= ||.f.||*||.t.|| by A9,A10,XREAL_1:64; end; end; theorem Th27: for X be RealUnitarySpace, f be Point of DualSp X holds 0 <= ||.f.|| proof let X be RealUnitarySpace; let f be Point of DualSp X; reconsider g=f as Lipschitzian linear-Functional of X by Def10; consider r0 be object such that A1: r0 in PreNorms g by XBOOLE_0:def 1; reconsider r0 as Real by A1; A3: (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms g by Th24; now let r be Real; assume r in PreNorms g; then ex t be VECTOR of X st r=|.g.t.| & ||.t.|| <= 1; hence 0 <= r by COMPLEX1:46; end; then 0 <= r0 by A1; hence thesis by A1,SEQ_4:def 1,A3; end; theorem LM6A: 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 proof let X be RealUnitarySpace, f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL; assume AS: f=g; set Y=RUSp2RNSp X; hereby assume AS1: f is additive homogeneous; A1: g is additive proof let x,y be Point of Y; reconsider x1=x,y1=y as Point of X; thus g.(x+y) = f.(x1+y1) by AS .= g.x + g.y by AS,AS1,HAHNBAN:def 2; end; g is homogeneous proof let x be Point of Y, r be Real; reconsider x1=x as Point of X; thus g.(r*x) = f.(r*x1) by AS .= r*g.x by AS,AS1,HAHNBAN:def 3; end; hence g is additive homogeneous by A1; end; assume AS2: g is additive homogeneous; A2: f is additive proof let x,y be Point of X; reconsider x1=x,y1=y as Point of Y; thus f.(x+y) = g.(x1+y1) by AS .= f.x + f.y by AS,AS2,HAHNBAN:def 2; end; f is homogeneous proof let x be Point of X, r be Real; reconsider x1=x as Point of Y; thus f.(r*x) = g.(r*x1) by AS .= r*f.x by AS,AS2,HAHNBAN:def 3; end; hence f is additive homogeneous by A2; end; theorem LM6B: 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 proof let X be RealUnitarySpace, f be linear-Functional of X, g be linear-Functional of RUSp2RNSp X; assume AS: f=g; set Y=RUSp2RNSp X; hereby assume f is Lipschitzian; then consider K be Real such that A1: 0 < K & for x be Point of X holds |.f.x.| <= K * ||.x.|| by BHSP_6:def 4; for y be Point of Y holds |.g.y.| <= K * ||.y.|| proof let y be Point of Y; reconsider x=y as Point of X; ||.y.|| = ||.x.|| by Def1; hence |.g.y.| <= K * ||.y.|| by A1,AS; end; hence g is Lipschitzian by A1; end; assume g is Lipschitzian; then consider K be Real such that A2: 0 <= K & for y be Point of Y holds |.g.y.| <= K * ||.y.||; A4: K + 0 < K + 1 by XREAL_1:8; for x be Point of X holds |.f.x.| <= (K+1) * ||.x.|| proof let x be Point of X; reconsider y=x as Point of Y; ||.x.|| = ||.y.|| by Def1; then B3: |.f.x.| <= K * ||.x.|| by A2,AS; 0 <= ||.x.|| by BHSP_1:28; then K * ||.x.|| <= (K+1) * ||.x.|| by A4,XREAL_1:64; hence |.f.x.| <= (K+1) * ||.x.|| by B3,XXREAL_0:2; end; hence f is Lipschitzian by A2,BHSP_6:def 4; end; theorem LM6: for X be RealUnitarySpace holds BoundedLinearFunctionals X = BoundedLinearFunctionals (RUSp2RNSp X) proof let X be RealUnitarySpace; set Y = RUSp2RNSp X; now let x be object; assume x in BoundedLinearFunctionals X; then A1: x is Lipschitzian linear-Functional of X by Def10; then x is linear-Functional of Y by LM6A; then x is Lipschitzian linear-Functional of Y by A1,LM6B; hence x in BoundedLinearFunctionals Y by DUALSP01:def 10; end; then A2: BoundedLinearFunctionals X c= BoundedLinearFunctionals Y; now let x be object; assume x in BoundedLinearFunctionals Y; then x is Lipschitzian linear-Functional of Y by DUALSP01:def 10; then x is Lipschitzian linear-Functional of X by LM6B,LM6A; hence x in BoundedLinearFunctionals X by Def10; end; then BoundedLinearFunctionals Y c= BoundedLinearFunctionals X; hence thesis by A2; end; theorem LM8: 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 proof let X be RealUnitarySpace, u be linear-Functional of X, v be linear-Functional of (RUSp2RNSp X); assume AS: u=v; set Y = RUSp2RNSp X; A11: now let x be object; assume AS1: x in PreNorms u; then reconsider y=x as Real; consider t be VECTOR of X such that B1: y = |.u.t.| & ||.t.|| <= 1 by AS1; reconsider t1=t as VECTOR of Y; ||.t1.|| <= 1 by B1,Def1; hence x in PreNorms v by AS,B1; end; now let x be object; assume AS2: x in PreNorms v; then reconsider y=x as Real; consider t be VECTOR of Y such that B1: y = |.v.t.| & ||.t.|| <= 1 by AS2; reconsider t1=t as VECTOR of X; ||.t1.|| <= 1 by B1,Def1; hence x in PreNorms u by AS,B1; end; hence PreNorms u = PreNorms v by A11; end; theorem LM9: for X be RealUnitarySpace holds BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X) proof let X be RealUnitarySpace; set Y = RUSp2RNSp X; set f = BoundedLinearFunctionalsNorm X; set g = BoundedLinearFunctionalsNorm Y; A1: dom f = BoundedLinearFunctionals X by FUNCT_2:def 1 .= BoundedLinearFunctionals Y by LM6 .= dom g by FUNCT_2:def 1; now let x be object; assume B11: x in dom f; then B1: x in BoundedLinearFunctionals X; B2: f.x = upper_bound PreNorms(Bound2Lipschitz(x,X)) by B11,Def14; B31: x in BoundedLinearFunctionals Y by B1,LM6; Bound2Lipschitz(x,X) = Bound2Lipschitz(x,RUSp2RNSp X) by LM6; then upper_bound PreNorms(Bound2Lipschitz(x,X)) = upper_bound PreNorms(Bound2Lipschitz(x,Y)) by LM8; hence f.x = g.x by B2,B31,DUALSP01:def 14; end; hence thesis by A1; end; theorem LM10A: for X be RealUnitarySpace holds LinearFunctionals X = LinearFunctionals (RUSp2RNSp X) proof let X be RealUnitarySpace; set Y = RUSp2RNSp X; now let x be object; assume x in LinearFunctionals X; then x is linear-Functional of X by DUALSP01:def 6; then x is linear-Functional of Y by LM6A; hence x in LinearFunctionals Y by DUALSP01:def 6; end; then A1: LinearFunctionals X c= LinearFunctionals Y; now let x be object; assume x in LinearFunctionals Y; then x is linear-Functional of Y by DUALSP01:def 6; then x is linear-Functional of X by LM6A; hence x in LinearFunctionals X by DUALSP01:def 6; end; then LinearFunctionals Y c= LinearFunctionals X; hence thesis by A1; end; theorem LM10B: for X be RealUnitarySpace holds X*' = (RUSp2RNSp X)*' proof let X be RealUnitarySpace; set Y = RUSp2RNSp X; the carrier of X*' = the carrier of Y*'by LM10A; hence X*' = (RUSp2RNSp X)*'; end; theorem for X be RealUnitarySpace holds DualSp X = DualSp (RUSp2RNSp X) proof let X be RealUnitarySpace; set Y = RUSp2RNSp X; set X1 = BoundedLinearFunctionals X; set Y1 = BoundedLinearFunctionals Y; A0: the carrier of X*' = the carrier of Y*' by LM10B; A2: the ZeroF of DualSp X = 0.(X*') by RSSPACE:def 10 .= 0.(Y*') by LM10B .= the ZeroF of DualSp Y by DUALSP01:17,RSSPACE:def 10; A3: the addF of DualSp X = (the addF of X*') ||X1 by RSSPACE:def 8 .= (the addF of Y*') ||Y1 by LM6,A0 .= the addF of DualSp Y by DUALSP01:17,RSSPACE:def 8; A4: the Mult of DualSp X = (the Mult of X*') | [:REAL,X1:] by RSSPACE:def 9 .= (the Mult of Y*') | [:REAL,Y1:] by LM6,A0 .= the Mult of DualSp Y by DUALSP01:17,RSSPACE:def 9; the normF of DualSp X = the normF of DualSp Y by LM9; hence DualSp X = DualSp (RUSp2RNSp X) by A2,A3,A4; end; begin :: The Orthogonal Projection theorem 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 proof let X be RealUnitarySpace; let M,N be Subspace of X; assume A1: the carrier of M c= the carrier of N; let x be object; assume x in the carrier of Ort_Comp N; then x in {v where v is VECTOR of X : for w being VECTOR of X st w in N holds w, v are_orthogonal} by RUSUB_5:def 3; then A2: ex v1 being VECTOR of X st x = v1 & for w being VECTOR of X st w in N holds w,v1 are_orthogonal; then reconsider x as VECTOR of X; for y being VECTOR of X st y in M holds y,x are_orthogonal proof let y being VECTOR of X; assume y in M; then y in N by A1; hence y,x are_orthogonal by A2; end; then x in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w,v are_orthogonal}; hence thesis by RUSUB_5:def 3; end; theorem for X be RealUnitarySpace, M be Subspace of X holds the carrier of M c= the carrier of Ort_Comp (Ort_Comp M) proof let X be RealUnitarySpace; let M be Subspace of X; let x be object; assume AS: x in the carrier of M; then A1: x in M; the carrier of M c= the carrier of X by RUSUB_1:def 1; then reconsider x as VECTOR of X by AS; for y being VECTOR of X st y in Ort_Comp M holds x,y are_orthogonal proof let y be VECTOR of X; assume y in Ort_Comp M; then y in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w, v are_orthogonal} by RUSUB_5:def 3; then ex v being VECTOR of X st y = v & for w being VECTOR of X st w in M holds w, v are_orthogonal; hence thesis by A1; end; then x in {v where v is VECTOR of X : for w being VECTOR of X st w in Ort_Comp M holds w, v are_orthogonal}; hence thesis by RUSUB_5:def 3; end; theorem Lm814: 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 proof let X be RealUnitarySpace, M be Subspace of X, x be Point of X; assume x in (the carrier of M) /\ the carrier of (Ort_Comp M); then A1: x in M & x in Ort_Comp M by XBOOLE_0:def 4; then x in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w, v are_orthogonal} by RUSUB_5:def 3; then consider v be VECTOR of X such that A2: x = v & for w being VECTOR of X st w in M holds w, v are_orthogonal; x, x are_orthogonal by A1,A2; hence thesis by BHSP_1:def 2; end; theorem 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 proof let X be RealUnitarySpace, M be Subspace of X, N be non empty Subset of X; assume AS1: N = the carrier of (Ort_Comp M); hence N is linearly-closed by RUSUB_1:28; for s be sequence of X st rng s c= N & s is convergent holds lim s in N proof let s be sequence of X; assume AS2: rng s c= N & s is convergent; A1: now let i be Nat; s.i in rng s by FUNCT_2:4,ORDINAL1:def 12; then s.i in N by AS2; then s.i in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w,v are_orthogonal} by AS1,RUSUB_5:def 3; then consider v be VECTOR of X such that B1: v=s.i & for w being VECTOR of X st w in M holds w,v are_orthogonal; thus for w being VECTOR of X st w in M holds w .|. (s.i) = 0 by B1,BHSP_1:def 3; end; for w being VECTOR of X st w in M holds w .|. (lim s) = 0 proof let w be VECTOR of X; assume AS3: w in M; reconsider g=w .|. (lim s) as Real; for p be Real st 0 < p ex m be Nat st for n be Nat st m <= n holds |. (seq_const 0).n - w .|. (lim s) .| < p proof let p be Real; assume B0: 0 < p; B1: 0 <= ||.w.|| by BHSP_1:28; reconsider r=p/(||.w.|| + 1) as Real; B41: ||.w.|| + 0 < ||.w.|| + 1 by XREAL_1:8; r*(||.w.|| + 1) = p by B1,XCMPLX_1:87; then B5: 0 < r & r*||.w.|| < p by B0,B1,B41,XREAL_1:68; consider m be Nat such that B6: for n be Nat st m <= n holds ||.s.n - lim s.|| < r by B1,B0,AS2,BHSP_2:19; B7: for n be Nat st m <= n holds |. (seq_const 0).n - w .|. (lim s) .| < p proof let n be Nat; assume m <= n; then C1: ||.s.n - lim s.|| < r by B6; C2: |. w .|. (s.n) - w .|. (lim s) .| = |. w .|. (s.n - lim s) .| by BHSP_1:12; C3: |. w .|. (s.n - lim s) .| <= ||.w.|| * ||.s.n - lim s.|| by BHSP_1:29; ||.w.|| * ||.s.n - lim s.|| <= ||.w.||*r by B1,C1,XREAL_1:64; then C41: |. w .|. (s.n) - w .|. (lim s) .| <= ||.w.||*r by C2,C3,XXREAL_0:2; w .|. (s.n) = 0 by A1,AS3 .= (seq_const 0).n by SEQ_1:57; hence thesis by C41,B5,XXREAL_0:2; end; take m; thus thesis by B7; end; then lim (seq_const 0) = w .|. (lim s) by SEQ_2:def 7; then (seq_const 0).0 = w .|. (lim s) by SEQ_4:26; hence w .|. (lim s) = 0 by SEQ_1:57; end; then A3: for w being VECTOR of X st w in M holds w,lim s are_orthogonal; reconsider v=lim s as VECTOR of X; lim s in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w,v are_orthogonal} by A3; hence lim s in N by AS1,RUSUB_5:def 3; end; hence N is closed by LM1; end; Lm88A: for X be RealUnitarySpace, x,y be Point of X holds ||.x + y.||*||.x + y.|| + ||.x - y.||*||.x - y.|| = 2*(||.x.||*||.x.||) + 2*(||.y.||*||.y.||) proof let X be RealUnitarySpace, x,y be Point of X; ||.x + y.||^2 = ||.x + y.||*||.x + y.|| & ||.x - y.||^2 = ||.x - y.||*||.x - y.|| & ||.x.||^2 = ||.x.||*||.x.|| & ||.y.||^2 = ||.y.||*||.y.|| by SQUARE_1:def 1; hence thesis by RUSUB_5:31; end; theorem Lm88: 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 proof let X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X, d be Real; assume that A1: N = the carrier of M & N is closed and A2: 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; consider Y be non empty Subset of REAL such that A3: Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0 by A2; reconsider r0=0 as Real; for r be ExtReal st r in Y holds r0 <= r proof let r be ExtReal; assume r in Y; then ex y be Point of X st r = ||.x-y.|| & y in M by A3; hence r0 <= r by BHSP_1:28; end; then r0 is LowerBound of Y by XXREAL_2:def 2; then A4:Y is bounded_below; defpred P[Nat,Real] means $2 in Y & $2 < d + (1/($1+1)); F1: for n being Element of NAT ex r being Element of REAL st P[n,r] proof let n be Element of NAT; reconsider n1=n as Nat; consider r1 be Real such that F11: r1 in Y & r1 < d + (1/(n1+1)) by A4,A3,SEQ_4:def 2; reconsider r=r1 as Element of REAL by XREAL_0:def 1; take r; thus thesis by F11; end; consider S being Function of NAT,REAL such that B3: for n being Element of NAT holds P[n,S.n] from FUNCT_2:sch 3(F1); B4: for n be Nat holds |. S.n - d .| <= 1/(n+1) proof let n be Nat; C11: n in NAT by ORDINAL1:def 12; then S.n in Y & S.n < d + (1/(n+1)) by B3; then C21: d <= S.n by A4,A3,SEQ_4:def 2; S.n - d < d + 1/(n+1) - d by C11,B3,XREAL_1:9; hence |. S.n - d .| <= 1/(n+1) by C21,ABSVALUE:def 1,XREAL_1:48; end; B5: for p be Real st 0
= k & m >= k holds |. (SA.m + SB.n) - 4*(d*d) .| < e proof let e be Real; assume B01: 0 < e; then consider k1 be Nat such that B1: for n be Nat st n >= k1 holds |.SA.n - 2*(d*d).| < e/2 by A5,C5,SEQ_2:def 7; consider k2 be Nat such that B2: for m be Nat st m >= k2 holds |.SB.m - 2*(d*d).| < e/2 by B01,A5,C6,SEQ_2:def 7; max(k1,k2) is natural; then reconsider k=max(k1,k2) as Nat; B3: for n,m be Nat st n >= k & m >= k holds |.(SA.m + SB.n) - 4*(d*d).| < e proof let n,m be Nat; assume AS: n >= k & m >= k; k >= k1 & k >= k2 by XXREAL_0:25; then C0: n >= k1 & m >= k2 by AS,XXREAL_0:2; then C1: |.SA.n - 2*(d*d).| < e/2 by B1; C2: |.SB.m - 2*(d*d).| < e/2 by C0,B2; C4: |.(SA.n - 2*(d*d)) + (SB.m - 2*(d*d)).| <= |.SA.n - 2*(d*d).| + |.SB.m - 2*(d*d).| by COMPLEX1:56; |.SA.n - 2*(d*d).| + |.SB.m - 2*(d*d).| < e/2 + e/2 by C1,C2,XREAL_1:8; hence thesis by C4,XXREAL_0:2; end; take k; thus thesis by B3; end; for p be Real st p > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.z.n - z.m.|| < p proof let p be Real; assume AS1: p > 0; then consider k be Nat such that D1: for n,m be Nat st n >= k & m >= k holds |. (SA.m + SB.n) - 4*(d*d) .| < p*p by A12; D2: for n, m be Nat st n >= k & m >= k holds ||.z.n - z.m.|| < p proof let n, m be Nat; assume n >= k & m >= k; then B0: |. (SA.m + SB.n) - 4*(d*d) .| < p*p by D1; set C=||.(x-z.n).||; set D=||.(x-z.m).||; B2: (x-z.n) + (x-z.m) = ((-z.n + x) + x) + -z.m by RLVECT_1:def 3 .= ((x + x) + -z.n) + -z.m by RLVECT_1:def 3 .= (x + x) +(-z.n + -z.m) by RLVECT_1:def 3 .= (x + x) + (-(z.n + z.m)) by RLVECT_1:31 .= (1*x + x) + (-(z.n + z.m)) by RLVECT_1:def 8 .= (1*x + 1*x) + (-(z.n + z.m)) by RLVECT_1:def 8 .= ((1+1)*x) + (-(z.n + z.m)) by RLVECT_1:def 6 .= 2*x - (z.n + z.m); B3: (x-z.n) - (x-z.m) = (x + -z.n) + (z.m + -x) by RLVECT_1:33 .= -x + ((x + -z.n) + z.m) by RLVECT_1:def 3 .= -x + (x + (-z.n + z.m)) by RLVECT_1:def 3 .= (-x + x) + (-z.n + z.m) by RLVECT_1:def 3 .= 0.X + (-z.n + z.m) by RLVECT_1:5 .= z.m - z.n; set E=||.2*x - (z.n + z.m).||; set F=||.z.m - z.n.||; B6: F*F = (E*E + F*F) + -E*E .= (2*(C*C) + 2*(D*D)) + -E*E by Lm88A,B2,B3; 2*x - (z.n + z.m) = 2*x + (-1)*(z.n + z.m) by RLVECT_1:16 .= 2*x + 2*(1/2)*(-(z.n + z.m)) by RLVECT_1:24 .= 2*x + 2*((1/2)*(-(z.n + z.m))) by RLVECT_1:def 7 .= 2*(x + (1/2)*(-(z.n + z.m))) by RLVECT_1:def 5 .= 2*(x - (1/2)*(z.n + z.m)) by RLVECT_1:25; then B7: ||.2*x - (z.n + z.m).|| = |.2.|*||.x - (1/2)*(z.n + z.m).|| by BHSP_1:27 .= 2*||.x - (1/2)*(z.n + z.m).|| by ABSVALUE:def 1; reconsider znm=z.n+z.m as Point of X; reconsider p0=||.x - (1/2)*(z.n+z.m).|| as Real; z.n in M & z.m in M by A8; then znm in M by RUSUB_1:14; then (1/2)*znm in M by RUSUB_1:15; then p0 in Y by A3; then d <= p0 by A3,A4,SEQ_4:def 2; then 2*d <= ||.2*x - (z.n + z.m).|| by B7,XREAL_1:64; then (2*d)*(2*d) <= ||.2*x - (z.n + z.m).||*||.2*x - (z.n + z.m).|| by A3,XREAL_1:66; then -(E*E) <= -(4*(d*d)) by XREAL_1:24; then B81: F*F <= (2*(C*C) + 2*(D*D)) + -(4*(d*d)) by B6,XREAL_1:6; E2: SA.n = 2*S1.n by SEQ_1:9 .= 2*((S.n)*(S.n)) by SEQ_1:8; E3: SB.m = 2*S2.m by SEQ_1:9 .= 2*((S.m)*(S.m)) by SEQ_1:8; B91: C = S.n & D = S.m by A8; (SA.n + SB.m) - 4*(d*d) <= |.(SA.n + SB.m) - 4*(d*d).| by ABSVALUE:4; then F*F <= |.(SA.n + SB.m) - 4*(d*d).| by B91,B81,E2,E3,XXREAL_0:2; then F*F < p*p by B0,XXREAL_0:2; then F^2 < p*p by SQUARE_1:def 1; then B10: F^2 < p^2 by SQUARE_1:def 1; 0 <= F*F by XREAL_1:63; then 0 <= F^2 by SQUARE_1:def 1; then B11: sqrt F^2 < sqrt p^2 by B10,SQUARE_1:27; B12: F < sqrt p^2 by B11,SQUARE_1:22,BHSP_1:28; ||.z.n - z.m.|| = ||.-(z.m - z.n).|| by RLVECT_1:33 .= F by BHSP_1:31; hence thesis by B12,SQUARE_1:22,AS1; end; take k; thus thesis by D2; end; then A13: z is convergent by BHSP_3:def 4,BHSP_3:2; then consider x0 be Point of X such that A14: for r be Real st r > 0 ex m be Nat st for n be Nat st n >= m holds ||.z.n - x0.|| < r by BHSP_2:9; lim z = x0 by A13,A14,BHSP_2:19; then A16: lim ||.z - x.|| = ||.x0-x.|| by A13,BHSP_2:34 .= ||.-(x0-x).|| by BHSP_1:31 .= ||.x-x0.|| by RLVECT_1:33; for y be object st y in rng z holds y in N proof let y be object; assume y in rng z; then ex n being object st n in NAT & z.n = y by FUNCT_2:11; then y in M by A8; hence thesis by A1; end; then rng z c= N; then BX: lim z in N by A1,A13,LM1; ex k0 be Nat st for n be Nat st k0 <= n holds S.n = ||.z - x.||.n proof set k0 = the Nat; B1: for n be Nat st k0 <= n holds S.n = ||.z - x.||.n proof let n be Nat; assume k0 <= n; thus S.n = ||.x - z.n.|| by A8 .= ||.-(z.n - x).|| by RLVECT_1:33 .= ||.z.n + -x.|| by BHSP_1:31 .= ||.(z + -x).n.|| by BHSP_1:def 6 .= ||.(z - x).n.|| by BHSP_1:56 .= ||.z - x.||.n by BHSP_2:def 3; end; take k0; thus thesis by B1; end; then BY: lim S = lim ||.z - x.|| by A5,SEQ_4:19; take x0; thus thesis by BX,A1,A13,A14,BHSP_2:19,BY,SEQ_2:def 7,B5,A16,A5; end; theorem Lm87A: 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 proof let X be RealHilbertSpace, M be Subspace of X, x,x0 be Point of X, d be Real; assume that A2: x0 in M and A3: 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; consider Y be non empty Subset of REAL such that A4: Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0 by A3; reconsider r0=0 as Real; for r be ExtReal st r in Y holds r0 <= r proof let r be ExtReal; assume r in Y; then ex y be Point of X st r = ||.x-y.|| & y in M by A4; hence r0 <= r by BHSP_1:28; end; then r0 is LowerBound of Y by XXREAL_2:def 2; then A51: Y is bounded_below; A6: for y0 be Point of X st y0 in M holds d <= ||.x-y0.|| proof let y0 be Point of X; assume y0 in M; then ||.x-y0.|| in Y by A4; hence thesis by A51,A4,SEQ_4:def 2; end; hereby assume AS1: d = ||.x-x0.||; assume not (for w be Point of X st w in M holds w, x-x0 are_orthogonal); then consider w be Point of X such that B1: w in M & w .|. (x-x0) <> 0; set e = w .|. (x-x0); set r = e/||.w.||^2; set s = ||.w.||^2; reconsider w0 = x0 + r*w as Point of X; B21: r*w in M by B1,RUSUB_1:15; per cases; suppose C11: s = 0; ||.w.|| = 0 by C11,SQUARE_1:17,SQUARE_1:22,BHSP_1:28; then w = 0.X by BHSP_1:26; hence contradiction by B1,BHSP_1:14; end; suppose CS2: s <> 0; C2: ||.x-w0.||^2 = ||.(x-x0) - r*w.||^2 by RLVECT_1:27 .= ||.x-x0.||^2 - 2*((x-x0) .|. (r*w)) + ||.r*w.||^2 by RUSUB_5:29; C3: (x-x0) .|. (r*w) = (e/s)*e by BHSP_1:3 .= (e*e)/s by XCMPLX_1:74 .= e^2/s by SQUARE_1:def 1; C4: ||.r*w.||^2 = (|.r.|*||.w.||)^2 by BHSP_1:27 .= |.r.|^2*s by SQUARE_1:9 .= (e/s)^2*s by COMPLEX1:75 .= (e*(1/s))^2*s by XCMPLX_1:99 .= e^2*(1/s)^2*s by SQUARE_1:9 .= e^2*((1/s)^2*s) .= e^2*((1/s)*(1/s)*s) by SQUARE_1:def 1 .= e^2*((1/s)*((1/s)*s)) .= e^2*((1/s)*1) by CS2,XCMPLX_1:106 .= e^2/s by XCMPLX_1:99; C5: ||.x-w0.||^2 = ||.x-x0.||^2 - e^2/s by C3,C4,C2; C6: 0 < e^2 by B1,SQUARE_1:12; 0 <= ||.w.|| by BHSP_1:28; then 0 <= ||.w.||*||.w.||; then 0 < s by CS2,SQUARE_1:def 1; then C7: ||.x-w0.||^2 < ||.x-x0.||^2 by C5,XREAL_1:44,C6; 0 <= ||.x-w0.||*||.x-w0.|| by XREAL_1:63; then 0 <= ||.x-w0.||^2 by SQUARE_1:def 1; then sqrt ||.x-w0.||^2 < sqrt ||.x-x0.||^2 by C7,SQUARE_1:27; then C91: ||.x-w0.|| < sqrt ||.x-x0.||^2 by BHSP_1:28,SQUARE_1:22; d <= ||.x-w0.|| by A6,B21,A2,RUSUB_1:14; hence contradiction by C91,AS1,BHSP_1:28,SQUARE_1:22; end; end; assume AS2: for w be Point of X st w in M holds w, x-x0 are_orthogonal; B1: for y be Point of X st y in M holds ||.x-x0.|| <= ||.x-y.|| proof let y be Point of X; assume y in M; then C1: x0-y,x-x0 are_orthogonal by AS2,A2,RUSUB_1:17; x - y = (x - y) + 0.X .= (x + -y) + (-x0 + x0) by RLVECT_1:5 .= ((x + -y) + -x0) + x0 by RLVECT_1:def 3 .= ((x + -x0) + -y) + x0 by RLVECT_1:def 3 .= (x - x0) + (x0 - y) by RLVECT_1:def 3; then ||.x-y.||^2 = ||.x-x0.||^2 + ||.x0-y.||^2 by C1,RUSUB_5:30; then C2: ||.x-y.||^2 - ||.x0-y.||^2 = ||.x-x0.||^2; 0 <= ||.x0-y.||*||.x0-y.|| by XREAL_1:63; then C31: 0 <= ||.x0-y.||^2 by SQUARE_1:def 1; 0 <= ||.x-x0.||*||.x-x0.|| by XREAL_1:63; then 0 <= ||.x-x0.||^2 by SQUARE_1:def 1; then sqrt ||.x-x0.||^2 <= sqrt ||.x-y.||^2 by C31,C2,XREAL_1:43,SQUARE_1:26; then ||.x-x0.|| <= sqrt ||.x-y.||^2 by BHSP_1:28,SQUARE_1:22; hence ||.x-x0.|| <= ||.x-y.|| by BHSP_1:28,SQUARE_1:22; end; for s be Real st s in Y holds ||.x-x0.|| <= s proof let s be Real; assume s in Y; then consider y0 be Point of X such that C1: s = ||.x-y0.|| & y0 in M by A4; thus ||.x-x0.|| <= s by B1,C1; end; then B2: ||.x-x0.|| <= d by A4,SEQ_4:43; d <= ||.x-x0.|| by A2,A6; hence d = ||.x-x0.|| by B2,XXREAL_0:1; end; theorem Th87A: 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 proof let X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X; assume AS: N = the carrier of M & N is closed; set Y = {||.x-y.|| where y is Point of X: y in M}; Y c= REAL proof let z be object; assume z in Y; then consider y be Point of X such that B1: z = ||.x-y.|| & y in M; thus z in REAL by B1,XREAL_0:def 1; end; then reconsider Y as Subset of REAL; 0.X in M by RUSUB_1:11; then ||.x-0.X.|| in Y; then reconsider Y as non empty Subset of REAL; set d = lower_bound Y; A11: for r be Real st r in Y holds 0 <= r proof let r be Real; assume r in Y; then consider y be Point of X such that B2: r = ||.x-y.|| & y in M; thus 0 <= r by B2,BHSP_1:28; end; then A1: 0 <= d by SEQ_4:43; consider x0 be Point of X such that A2: d = ||.x-x0.|| & x0 in M by AS,Lm88,A11,SEQ_4:43; reconsider y=x0 as Point of X; reconsider z=x-x0 as Point of X; for w be Point of X st w in M holds w, x-x0 are_orthogonal by A1,A2,Lm87A; then B21: x-x0 in {v where v is VECTOR of X : for w be Point of X st w in M holds w, v are_orthogonal}; B3: y + z = (x0 + -x0) + x by RLVECT_1:def 3 .= x + 0.X by RLVECT_1:5 .= x; take y,z; thus thesis by A2,B21,RUSUB_5:def 3,B3; end; theorem 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 proof let X be RealUnitarySpace, M be Subspace of X, x be Point of X; let y1,y2,z1,z2 be Point of X; assume that A1: y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M and A2: x = y1 + z1 & x = y2 + z2; y1 + (z1 + -y2) = (y2 + z2) + -y2 by RLVECT_1:def 3,A2; then y1 + (-y2 + z1) = y2 + (-y2 + z2) by RLVECT_1:def 3; then (y1 + -y2) + z1 = y2 + (-y2 + z2) by RLVECT_1:def 3; then (y1 - y2) + z1 = (y2 + -y2) + z2 by RLVECT_1:def 3; then (y1 - y2) + z1 = z2 + 0.X by RLVECT_1:def 10; then (y1 - y2) + (z1 + -z1) = z2 + -z1 by RLVECT_1:def 3; then A31: (y1 - y2) + 0.X = z2 + -z1 by RLVECT_1:def 10; A4: y1 - y2 in M & z2 - z1 in Ort_Comp M by A1,RUSUB_1:17; then y1 - y2 in (the carrier of M) /\ the carrier of (Ort_Comp M) by XBOOLE_0:def 4,A31; then y1 - y2 = 0.X by Lm814; hence y1 = y2 by RLVECT_1:21; z2 - z1 in (the carrier of M) /\ the carrier of (Ort_Comp M) by A4,A31,XBOOLE_0:def 4; then z2 - z1 = 0.X by Lm814; hence z1 = z2 by RLVECT_1:21; end; begin :: F. Riesz Representation Theorem theorem 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 proof let X be RealUnitarySpace, f be linear-Functional of X, y be Point of X; assume AS: for x be Point of X holds f.x = x .|. y; reconsider K=||.y.|| + 1 as Real; A11: 0 <= ||.y.|| by BHSP_1:28; for x be Point of X holds |.f.x.| <= K * ||.x.|| proof let x be Point of X; B1: |.x .|. y.| <= ||.x.||*||.y.|| by BHSP_1:29; B2: ||.y.|| < ||.y.|| + 1 by XREAL_1:145; 0 <= ||.x.|| by BHSP_1:28; then ||.y.|| * ||.x.|| <= (||.y.|| + 1) * ||.x.|| by B2,XREAL_1:64; then |.x .|. y.| <= (||.y.|| + 1) * ||.x.|| by B1,XXREAL_0:2; hence thesis by AS; end; hence thesis by A11,BHSP_6:def 4; end; KERX1: for X be RealUnitarySpace, f be Function of X,REAL st f is homogeneous holds f"{0} is non empty proof let X be RealUnitarySpace, f be Function of X,REAL; assume A1: f is homogeneous; f.(0.X) = f.(0 * 0.X) .= 0 * f.(0.X) by A1,HAHNBAN:def 3 .= 0; then f.(0.X) in {0} by TARSKI:def 1; hence thesis by FUNCT_2:38; end; registration let X be RealUnitarySpace, f be linear-Functional of X; cluster f"{0} -> non empty; correctness by KERX1; end; theorem KLXY1: for X be RealUnitarySpace, f be Function of X,REAL st f is additive homogeneous holds f"{0} is linearly-closed proof let X be RealUnitarySpace, f be Function of X,REAL; assume A1: f is additive homogeneous; set X1 = f"{0}; A2: for v,u be Point of X st v in X1 & u in X1 holds v+u in X1 proof let v,u be Point of X; assume AS1: v in X1 & u in X1; then v in the carrier of X & f.v in {0} by FUNCT_2:38; then A3: f.v = 0 by TARSKI:def 1; A4: u in the carrier of X & f.u in {0} by AS1,FUNCT_2:38; f.(v+u) = f.v + f.u by A1,HAHNBAN:def 2 .= 0 + 0 by A3,A4,TARSKI:def 1; then f.(v+u) in {0} by TARSKI:def 1; hence thesis by FUNCT_2:38; end; for r be Real, v be Point of X st v in X1 holds r*v in X1 proof let r be Real, v be Point of X; assume v in X1; then A5: v in the carrier of X & f.v in {0} by FUNCT_2:38; f.(r*v) = r * (f.v) by A1,HAHNBAN:def 3 .= r * 0 by A5,TARSKI:def 1; then f.(r*v) in {0} by TARSKI:def 1; hence thesis by FUNCT_2:38; end; hence thesis by A2; end; definition let X be RealUnitarySpace, f be linear-Functional of X; func UKer(f) -> strict Subspace of X means :defuker: the carrier of it = f"{0}; existence by KLXY1,RUSUB_1:29; uniqueness by RUSUB_1:24; end; theorem Lm89A: for X be RealUnitarySpace, f be linear-Functional of X st f is Lipschitzian holds f"{0} is closed proof let X be RealUnitarySpace, f be linear-Functional of X; assume AS: f is Lipschitzian; set Y=f"{0}; for s be sequence of X st rng s c= Y & s is convergent holds lim s in Y proof let s be sequence of X; assume B0: rng s c= Y & s is convergent; reconsider x0=lim s as Point of X; B1: dom f = the carrier of X by FUNCT_2:def 1; consider K be Real such that B3: 0 < K & for x be Point of X holds |. f.x .| <= K * ||. x .|| by AS,BHSP_6:def 4; for x1, x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds |.f/.x1 - f/.x2.| <= K * ||.x1 - x2.|| proof let x1,x2 be Point of X; assume x1 in the carrier of X & x2 in the carrier of X; C1: |.f/.x1 - f/.x2.| = |.f.(x1 - x2).| by HAHNBAN:19; thus thesis by C1,B3; end; then f is_Lipschitzian_on (the carrier of X) by FUNCT_2:def 1,B3; then B41: f is_continuous_on (the carrier of X) by LM5; B5: rng s c= the carrier of X; B71: f is_continuous_in x0 by B41; B91: f/*s = f*s by B1,B5,FUNCT_2:def 11; ex k be Nat st for n be Nat st k <= n holds (f*s).n = (seq_const 0).n proof set k = the Nat; C0: for n be Nat st k <= n holds (f*s).n = (seq_const 0).n proof let n be Nat; assume k <= n; s.n in rng s by FUNCT_2:4,ORDINAL1:def 12; then D2: s.n in X & f.(s.n) in {0} by FUNCT_2:38,B0; dom s = NAT by FUNCT_2:def 1; then (f*s).n in {0} by ORDINAL1:def 12,D2,FUNCT_1:13; then (f*s).n = 0 by TARSKI:def 1; hence (f*s).n = (seq_const 0).n by SEQ_1:57; end; take k; thus thesis by C0; end; then lim (f*s) = lim (seq_const 0) by SEQ_4:19 .= (seq_const 0).0 by SEQ_4:26 .= 0 by SEQ_1:57; then f.x0 = 0 by B71,B0,B1,B91; then x0 in X & f.x0 in {0} by TARSKI:def 1; hence lim s in Y by FUNCT_2:38; end; hence f"{0} is closed by LM1; end; theorem Lm89B: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; assume A1: v <> 0.V; v in Ort_Comp W implies not v in W proof assume A2: v in Ort_Comp W; assume A3: v in W; v in {v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds w,v1 are_orthogonal} by A2,RUSUB_5:def 3; then ex v1 being VECTOR of V st v = v1 & for w being VECTOR of V st w in W holds w,v1 are_orthogonal; then v,v are_orthogonal by A3; hence contradiction by A1,BHSP_1:def 2; end; hence thesis; end; theorem Th89A: 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 proof let X be RealHilbertSpace, f be linear-Functional of X; assume AS: f is Lipschitzian; set M = UKer(f); A1: the carrier of M = f"{0} by defuker; per cases; suppose AS1: the carrier of X = the carrier of M; reconsider y=0.X as Point of X; B1: for x be Point of X holds f.x = x .|. y proof let x be Point of X; C11: x in X & f.x in {0} by FUNCT_2:38,AS1,A1; x .|. y = 0 by BHSP_1:15; hence thesis by C11,TARSKI:def 1; end; take y; thus thesis by B1; end; suppose the carrier of X <> the carrier of M; then not the carrier of X c= the carrier of M by RUSUB_1:def 1; then consider z be object such that B1: z in the carrier of X & not z in the carrier of M; reconsider y=z as Point of X by B1; reconsider N=the carrier of M as non empty Subset of X by A1; consider y1,z1 be Point of X such that C0: y1 in M & z1 in Ort_Comp M & y = y1 + z1 by Th87A,A1,AS,Lm89A; C1: z1 <> 0.X by C0,B1; then ||.z1.|| <> 0 by BHSP_1:26; then C2: ||.z1.||^2 > 0 by SQUARE_1:12; not z1 in M by C0,C1,Lm89B; then not z1 in f"{0} by defuker; then not f.z1 in {0} by FUNCT_2:38; then C3: f.z1 <> 0 by TARSKI:def 1; set r=f.z1/||.z1.||^2; reconsider y=r*z1 as Point of X; C4: y in Ort_Comp M by C0,RUSUB_1:15; C5: for x be Point of X holds f.x = x .|. y proof let x be Point of X; set s=f.x/f.z1; reconsider y0=x - s*z1 as Point of X; D1: -s*z1 = (-1)*(s*z1) by RLVECT_1:16 .= ((-1)*s)*z1 by RLVECT_1:def 7; f.y0 = f.x + f.(((-1)*s)*z1) by D1,HAHNBAN:def 2 .= f.x + ((-1)*s)*f.z1 by HAHNBAN:def 3 .= f.x - (f.x/f.z1)*f.z1 .= f.x - f.x by C3,XCMPLX_1:87 .= 0; then y0 in X & f.y0 in {0} by TARSKI:def 1; then y0 in f"{0} by FUNCT_2:38; then D2: y0 in M by defuker; y in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w, v are_orthogonal} by RUSUB_5:def 3,C4; then consider v be VECTOR of X such that D3: y = v & for w being VECTOR of X st w in M holds w, v are_orthogonal; D41: y0,y are_orthogonal by D2,D3; D6: (x - s*z1) .|. (r*z1) = x .|. (r*z1) - (s*z1) .|. (r*z1) by BHSP_1:11 .= r * x .|. z1 - (s*z1) .|. (r*z1) by BHSP_1:3 .= r * x .|. z1 - s * (z1 .|. (r*z1)) by BHSP_1:def 2; D7: s*r = f.x/||.z1.||^2 by C3,XCMPLX_1:98; D8: 0 <= z1 .|. z1 by BHSP_1:def 2; z1 .|. (r*z1) = r * (z1 .|. z1) by BHSP_1:3 .= r * ||.z1.||^2 by D8,SQUARE_1:def 2; then s * (z1 .|. (r*z1)) = (f.x/||.z1.||^2) * ||.z1.||^2 by D7 .= f.x by C2,XCMPLX_1:87; hence f.x = x .|. y by BHSP_1:3,D6,D41; end; take y; thus thesis by C5; end; end; theorem 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 proof let X be RealUnitarySpace, f be linear-Functional of X; let y1,y2 be Point of X; assume AS: for x be Point of X holds f.x = x .|. y1 & f.x = x .|. y2; now let x be Point of X; f.x = x .|. y1 & f.x = x .|. y2 by AS; then x .|. y1 - x .|. y2 = 0; hence x .|. (y1 - y2) = 0 by BHSP_1:12; end; then (y1 - y2) .|. (y1 - y2) = 0; then y1 - y2 = 0.X by BHSP_1:def 2; hence y1 = y2 by RLVECT_1:21; end; theorem 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.|| proof let X be RealHilbertSpace, f be Point of DualSp X, g be Lipschitzian linear-Functional of X; assume AS: g=f; consider y be Point of X such that A1: for x be Point of X holds g.x = x .|. y by Th89A; now let s be Real; assume s in PreNorms g; then consider t be VECTOR of X such that B1: s = |.g.t.| & ||.t.|| <= 1; B3: |.t .|. y.| <= ||.t.|| * ||.y.|| by BHSP_1:29; 0 <= ||.y.|| by BHSP_1:28; then ||.t.|| * ||.y.|| <= 1 * ||.y.|| by B1,XREAL_1:64; then |.t .|. y.| <= ||.y.|| by B3,XXREAL_0:2; hence s <= ||.y.|| by B1,A1; end; then upper_bound PreNorms g <= ||.y.|| by SEQ_4:45; then A2: ||.f.|| <= ||.y.|| by AS,Th24; A31: ||.y.|| <= ||.f.|| proof per cases; suppose ||.y.|| = 0; hence ||.y.|| <= ||.f.|| by Th27; end; suppose AS2: ||.y.|| <> 0; B1: 0 <= y .|. y by BHSP_1:def 2; B2: g.y = y .|. y by A1 .= ||.y.||^2 by B1,SQUARE_1:def 2 .= ||.y.|| * ||.y.|| by SQUARE_1:def 1; B3: g.y <= |.g.y.| by ABSVALUE:4; |.g.y.| <= ||.f.|| * ||.y.|| by AS,Th26; then B4: ||.y.|| * ||.y.|| <= ||.f.|| * ||.y.|| by B2,B3,XXREAL_0:2; B51: 0 <= ||.y.|| by BHSP_1:28; ||.y.|| * ||.y.||/||.y.|| = ||.y.|| & ||.f.|| * ||.y.||/||.y.|| = ||.f.|| by AS2,XCMPLX_1:89; hence ||.y.|| <= ||.f.|| by B51,B4,XREAL_1:72; end; end; take y; thus thesis by A1,A2,XXREAL_0:1,A31; end;