let X be RealHilbertSpace; :: thesis: for M being Subspace of X
for N being Subset of X
for x being Point of X
for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )
let M be Subspace of X; :: thesis: for N being Subset of X
for x being Point of X
for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )
let N be Subset of X; :: thesis: for x being Point of X
for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )
let x be Point of X; :: thesis: for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )
let d be Real; :: thesis: ( N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) implies ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M ) )
assume that
A1: ( N = the carrier of M & N is closed ) and
A2: ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) ; :: thesis: ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )
consider Y being non empty Subset of REAL such that
A3: ( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) by A2;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in Y holds
r0 <= r
proof
let r be ExtReal; :: thesis: ( r in Y implies r0 <= r )
assume r in Y ; :: thesis: r0 <= r
then ex y being Point of X st
( r = ||.(x - y).|| & y in M ) by A3;
hence r0 <= r by BHSP_1:28; :: thesis: verum
end;
then r0 is LowerBound of Y by XXREAL_2:def 2;
then A4: Y is bounded_below ;
defpred S1[ 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 S1[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S1[n,r]
reconsider n1 = n as Nat ;
consider r1 being 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 ; :: thesis: S1[n,r]
thus S1[n,r] by F11; :: thesis: verum
end;
consider S being Function of NAT,REAL such that
B3: for n being Element of NAT holds S1[n,S . n] from FUNCT_2:sch 3(F1);
 B4: for n being Nat holds |.((S . n) - d).| <= 1 / (n + 1)
proof
let n be Nat; :: thesis: |.((S . n) - d).| <= 1 / (n + 1)
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; :: thesis: verum
end;
B5: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - d).| < p
proof
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - d).| < p )
assume D0: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - d).| < p
reconsider r = 1 / p as Real ;
consider n being Nat such that
E1: r < n by SEQ_4:3;
r * p = 1 by D0, XCMPLX_1:106;
then E3: 1 < n * p by D0, E1, XREAL_1:68;
n * p < (n + 1) * p by D0, XREAL_1:68, NAT_1:16;
then E4: 1 < (n + 1) * p by E3, XXREAL_0:2;
D1: 1 / (n + 1) < p by E4, XREAL_1:83;
take n ; :: thesis: for m being Nat st n <= m holds
|.((S . m) - d).| < p
let m be Nat; :: thesis: ( n <= m implies |.((S . m) - d).| < p )
assume n <= m ; :: thesis: |.((S . m) - d).| < p
then D21: n + 1 <= m + 1 by XREAL_1:6;
( (m + 1) " = 1 / (m + 1) & (n + 1) " = 1 / (n + 1) ) by XCMPLX_1:215;
then 1 / (m + 1) <= 1 / (n + 1) by D21, XREAL_1:85;
then D3: 1 / (m + 1) < p by XXREAL_0:2, D1;
|.((S . m) - d).| <= 1 / (m + 1) by B4;
hence |.((S . m) - d).| < p by D3, XXREAL_0:2; :: thesis: verum
end;
then A5: S is convergent ;
then A6: lim S = d by SEQ_2:def 7, B5;
defpred S2[ Nat, Point of X] means ( $2 in M & S . $1 = ||.(x - $2).|| );
F2: for n being Element of NAT ex v being Point of X st S2[n,v]
proof
let n be Element of NAT ; :: thesis: ex v being Point of X st S2[n,v]
( S . n in Y & S . n < d + (1 / (n + 1)) ) by B3;
then consider y being Point of X such that
F21: ( S . n = ||.(x - y).|| & y in M ) by A3;
take y ; :: thesis: S2[n,y]
thus S2[n,y] by F21; :: thesis: verum
end;
consider z being Function of NAT, the carrier of X such that
A7: for n being Element of NAT holds S2[n,z . n] from FUNCT_2:sch 3(F2);
 for n being Nat holds
( z . n in M & S . n = ||.(x - (z . n)).|| )
proof
let n be Nat; :: thesis: ( z . n in M & S . n = ||.(x - (z . n)).|| )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
( z . n1 in M & S . n1 = ||.(x - (z . n1)).|| ) by A7;
hence ( z . n in M & S . n = ||.(x - (z . n)).|| ) ; :: thesis: verum
end;
then consider z being sequence of X such that
A8: for n being Nat holds
( z . n in M & S . n = ||.(x - (z . n)).|| ) ;
reconsider S1 = S (#) S, S2 = S (#) S as Real_Sequence ;
reconsider SA = 2 (#) S1, SB = 2 (#) S2 as Real_Sequence ;
C3: lim S1 = d * d by A6, A5, SEQ_2:15;
C4: lim S2 = d * d by A6, A5, SEQ_2:15;
C5: lim SA = 2 * (d * d) by C3, A5, SEQ_2:8;
C6: lim SB = 2 * (d * d) by C4, A5, SEQ_2:8;
A12: for e being Real st 0 < e holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e
proof
let e be Real; :: thesis: ( 0 < e implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e )
assume B01: 0 < e ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e
then consider k1 being Nat such that
B1: for n being Nat st n >= k1 holds
|.((SA . n) - (2 * (d * d))).| < e / 2 by A5, C5, SEQ_2:def 7;
consider k2 being Nat such that
B2: for m being 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 being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e
proof
let n, m be Nat; :: thesis: ( n >= k & m >= k implies |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e )
assume AS: ( n >= k & m >= k ) ; :: thesis: |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e
( 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 |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e by C4, XXREAL_0:2; :: thesis: verum
end;
take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e
thus for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e by B3; :: thesis: verum
end;
for p being Real st p > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p
proof
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p )
assume AS1: p > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p
then consider k being Nat such that
D1: for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < p * p by A12;
D2: for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p
proof
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((z . n) - (z . m)).|| < p )
assume ( n >= k & m >= k ) ; :: thesis: ||.((z . n) - (z . m)).|| < p
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: ||.((z . m) - (z . n)).|| * ||.((z . m) - (z . n)).|| = ((||.((2 * x) - ((z . n) + (z . m))).|| * ||.((2 * x) - ((z . n) + (z . m))).||) + (||.((z . m) - (z . n)).|| * ||.((z . m) - (z . n)).||)) + (- (||.((2 * x) - ((z . n) + (z . m))).|| * ||.((2 * x) - ((z . n) + (z . m))).||))
.= ((2 * (||.(x - (z . n)).|| * ||.(x - (z . n)).||)) + (2 * (||.(x - (z . m)).|| * ||.(x - (z . m)).||))) + (- (||.((2 * x) - ((z . n) + (z . m))).|| * ||.((2 * x) - ((z . n) + (z . m))).||)) 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 - (||.((2 * x) - ((z . n) + (z . m))).|| * ||.((2 * x) - ((z . n) + (z . m))).||) <= - (4 * (d * d)) by XREAL_1:24;
then B81: ||.((z . m) - (z . n)).|| * ||.((z . m) - (z . n)).|| <= ((2 * (||.(x - (z . n)).|| * ||.(x - (z . n)).||)) + (2 * (||.(x - (z . m)).|| * ||.(x - (z . m)).||))) + (- (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: ( ||.(x - (z . n)).|| = S . n & ||.(x - (z . m)).|| = S . m ) by A8;
((SA . n) + (SB . m)) - (4 * (d * d)) <= |.(((SA . n) + (SB . m)) - (4 * (d * d))).| by ABSVALUE:4;
then ||.((z . m) - (z . n)).|| * ||.((z . m) - (z . n)).|| <= |.(((SA . n) + (SB . m)) - (4 * (d * d))).| by B91, B81, E2, E3, XXREAL_0:2;
then ||.((z . m) - (z . n)).|| * ||.((z . m) - (z . n)).|| < p * p by B0, XXREAL_0:2;
then ||.((z . m) - (z . n)).|| ^2 < p * p by SQUARE_1:def 1;
then B10: ||.((z . m) - (z . n)).|| ^2 < p ^2 by SQUARE_1:def 1;
0 <= ||.((z . m) - (z . n)).|| * ||.((z . m) - (z . n)).|| by XREAL_1:63;
then 0 <= ||.((z . m) - (z . n)).|| ^2 by SQUARE_1:def 1;
then B11: sqrt (||.((z . m) - (z . n)).|| ^2) < sqrt (p ^2) by B10, SQUARE_1:27;
B12: ||.((z . m) - (z . n)).|| < sqrt (p ^2) by B11, SQUARE_1:22, BHSP_1:28;
||.((z . n) - (z . m)).|| = ||.(- ((z . m) - (z . n))).|| by RLVECT_1:33
.= ||.((z . m) - (z . n)).|| by BHSP_1:31 ;
hence ||.((z . n) - (z . m)).|| < p by B12, SQUARE_1:22, AS1; :: thesis: verum
end;
take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p
thus for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p by D2; :: thesis: verum
end;
then A13: z is convergent by BHSP_3:def 4, BHSP_3:2;
then consider x0 being Point of X such that
A14: for r being Real st r > 0 holds
ex m being Nat st
for n being 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 being object st y in rng z holds
y in N
proof
let y be object ; :: thesis: ( y in rng z implies y in N )
assume y in rng z ; :: thesis: y in N
then ex n being object st
( n in NAT & z . n = y ) by FUNCT_2:11;
then y in M by A8;
hence y in N by A1; :: thesis: verum
end;
then rng z c= N ;
then BX: lim z in N by A1, A13, LM1;
ex k0 being Nat st
for n being Nat st k0 <= n holds
S . n = ||.(z - x).|| . n
proof
set k0 = the Nat;
B1: for n being Nat st the Nat <= n holds
S . n = ||.(z - x).|| . n
proof
let n be Nat; :: thesis: ( the Nat <= n implies S . n = ||.(z - x).|| . n )
assume the Nat <= n ; :: thesis: S . n = ||.(z - x).|| . 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 ; :: thesis: verum
end;
take the Nat ; :: thesis: for n being Nat st the Nat <= n holds
S . n = ||.(z - x).|| . n
thus for n being Nat st the Nat <= n holds
S . n = ||.(z - x).|| . n by B1; :: thesis: verum
end;
then BY: lim S = lim ||.(z - x).|| by A5, SEQ_4:19;
take x0 ; :: thesis: ( d = ||.(x - x0).|| & x0 in M )
thus ( d = ||.(x - x0).|| & x0 in M ) by BX, A1, A13, A14, BHSP_2:19, BY, SEQ_2:def 7, B5, A16, A5; :: thesis: verum