:: The Orthogonal Projection and {R}iesz Representation Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 1, 2015
:: Copyright (c) 2015-2026 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;
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;
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<p ex n be Nat
st for m be Nat st n<=m holds |.S.m - d.| < p
proof
let p be Real;
assume D0: 0 < p;
reconsider r=1/p as Real;
consider n be 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;
let m be Nat;
assume n <= m; 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;
end; then
A5: S is convergent; then
A6: lim S = d by SEQ_2:def 7,B5;
defpred P1[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 P1[n,v]
proof
let n be Element of NAT;
S.n in Y & S.n < d + (1/(n+1)) by B3; then
consider y be Point of X such that
F21: S.n = ||.x-y.|| & y in M by A3;
take y;
thus thesis by F21;
end;
consider z being Function of NAT,the carrier of X such that
A7: for n being Element of NAT holds P1[n,z.n]
from FUNCT_2:sch 3(F2);
for n be Nat holds z.n in M & S.n = ||.x - z.n.||
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
z.n1 in M & S.n1 = ||.x - z.n1.|| by A7;
hence thesis;
end; then
consider z be sequence of X such that
A8: for n be 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 be Real st 0 < e holds
ex k be Nat st for n,m be Nat st
n >= 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; 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;
::$N Riesz representation theorem
::$L https://en.wikipedia.org/wiki/Riesz_representation_theorem Riesz representation theorem
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;