:: The Orthogonal Projection and {R}iesz Representation Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 1, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, PROB_2, NFCONT_1, CFCONT_1,
RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI,
MSSUBFAM, STRUCT_0, REALSET1, SEQ_1, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2,
LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC,
SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2,
COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, VALUED_1, METRIC_1,
RELAT_2, ASYMPT_1, FUNCT_7, PARTFUN1, RCOMP_1, BHSP_1, RSSPACE2,
DUALSP04, RUSUB_5, SQUARE_1, RVSUM_1, BHSP_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, REALSET1, NUMBERS, XCMPLX_0, SQUARE_1,
XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, VALUED_1, SEQ_1, SEQ_2, SEQ_4,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, RLSUB_1,
RUSUB_1, RUSUB_5, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, RSSPACE2, BHSP_6,
RSSPACE3, LOPBAN_1, NFCONT_1, DUALSP01;
constructors REAL_1, REALSET1, RSSPACE3, LOPBAN_2, SEQ_1, NFCONT_1, DUALSP01,
RELSET_1, SEQ_2, SEQ_4, HAHNBAN1, COMSEQ_2, BHSP_2, BHSP_3, RUSUB_5,
SQUARE_1, BHSP_6;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1,
XXREAL_0, VALUED_0, RLVECT_1, FUNCT_2, VALUED_1, FUNCOP_1, RELSET_1,
NORMSP_3, XCMPLX_0, NAT_1, NORMSP_1, SEQ_2, DUALSP01, XBOOLE_0, SQUARE_1,
RUSUB_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin :: Preliminaries
definition
let X be RealUnitarySpace;
func normRU X -> Function of the carrier of X,REAL means
:: DUALSP04:def 1
for x be Point of X holds it.x = ||.x.||;
end;
definition
let X be RealUnitarySpace;
func RUSp2RNSp X -> RealNormSpace equals
:: DUALSP04:def 2
NORMSTR(# the carrier of X, the ZeroF of X, the addF of X,
the Mult of X, normRU X #);
end;
theorem :: DUALSP04:1
for X be RealUnitarySpace,
x be Point of X, x1 be Point of RUSp2RNSp X
st x=x1 holds -x = -x1;
theorem :: DUALSP04:2
for X be RealUnitarySpace,
x,y be Point of X, x1,y1 be Point of RUSp2RNSp X
st x=x1 & y=y1 holds x - y = x1 - y1;
theorem :: DUALSP04:3
for X be RealUnitarySpace,
x be Point of X, x1 be Point of RUSp2RNSp X
st x=x1 holds ||.x.|| = ||.x1.||;
theorem :: DUALSP04:4
for X be RealUnitarySpace,
s1 be sequence of X, s2 be sequence of RUSp2RNSp X
st s1 = s2 holds s1 is convergent iff s2 is convergent;
theorem :: DUALSP04:5
for X be RealUnitarySpace,
s1 be sequence of X, s2 be sequence of RUSp2RNSp X
st s1 = s2 & s1 is convergent holds
lim s1 = lim s2;
theorem :: DUALSP04:6
for X be RealUnitarySpace, s1 be sequence of X,
s2 be sequence of RUSp2RNSp X
st s1 = s2 holds s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy;
theorem :: DUALSP04:7
for X be RealUnitarySpace holds
X is complete iff RUSp2RNSp X is complete;
registration
let X be RealHilbertSpace;
cluster RUSp2RNSp X -> complete;
end;
definition
let X be RealUnitarySpace, Y be Subset of X;
attr Y is open means
:: DUALSP04:def 3
ex Z be Subset of RUSp2RNSp X st Z = Y & Z is open;
end;
definition
let X be RealUnitarySpace, Y be Subset of X;
attr Y is closed means
:: DUALSP04:def 4
ex Z be Subset of RUSp2RNSp X st Z = Y & Z is closed;
end;
theorem :: DUALSP04:8
for X be RealUnitarySpace, Y be Subset of X holds
Y is closed iff
for s be sequence of X st rng s c= Y & s is convergent
holds lim s in Y;
theorem :: DUALSP04:9
for X be RealUnitarySpace, Y be Subset of X
holds Y is open iff Y` is closed;
definition
let X be RealUnitarySpace;
let f be PartFunc of the carrier of X,REAL;
let x0 be Point of X;
pred f is_continuous_in x0 means
:: DUALSP04:def 5
x0 in dom f &
for s1 be sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0
holds f/*s1 is convergent & f/.x0 = lim (f/*s1);
end;
definition
let X be RealUnitarySpace;
let f be PartFunc of the carrier of X,REAL;
let Y be set;
pred f is_continuous_on Y means
:: DUALSP04:def 6
Y c= dom f &
for x0 be Point of X st x0 in Y holds f|Y is_continuous_in x0;
end;
theorem :: DUALSP04:10
for X be RealUnitarySpace,
f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL,
x0 be Point of X, y0 be Point of RUSp2RNSp X
st f=g & x0=y0 holds
f is_continuous_in x0 iff g is_continuous_in y0;
theorem :: DUALSP04:11
for X be RealUnitarySpace,
f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL
st f=g holds
f is_continuous_on the carrier of X
iff
g is_continuous_on the carrier of RUSp2RNSp X;
theorem :: DUALSP04:12
for X be RealUnitarySpace, w be Point of X,
f be Function of X,REAL
st for v be Point of X holds f.v = w .|. v
holds f is_continuous_on the carrier of X;
definition
let X be RealUnitarySpace;
let Y be set;
let f be PartFunc of the carrier of X,REAL;
pred f is_Lipschitzian_on Y means
:: DUALSP04:def 7
Y c= dom f & ex r be Real st 0 < r &
for x1, x2 be Point of X st x1 in Y & x2 in Y
holds |.f/.x1 - f/.x2.| <= r * ||.x1 - x2.||;
end;
theorem :: DUALSP04:13
for X be RealUnitarySpace,
f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL
st f=g holds
f is_Lipschitzian_on the carrier of X
iff
g is_Lipschitzian_on the carrier of RUSp2RNSp X;
theorem :: DUALSP04:14
for X be RealUnitarySpace, f be Function of X,REAL
st f is_Lipschitzian_on the carrier of X
holds f is_continuous_on the carrier of X;
theorem :: DUALSP04:15
for X be RealUnitarySpace, F be linear-Functional of X
st F = (the carrier of X) --> 0
holds F is Lipschitzian;
registration
let X be RealUnitarySpace;
cluster Lipschitzian for linear-Functional of X;
end;
definition
let X be RealUnitarySpace;
func BoundedLinearFunctionals X -> Subset of X*' means
:: DUALSP04:def 8
for x be set holds x in it
iff x is Lipschitzian linear-Functional of X;
end;
registration
let X be RealUnitarySpace;
cluster BoundedLinearFunctionals X -> non empty linearly-closed;
end;
definition
let X be RealUnitarySpace;
let f be object;
func Bound2Lipschitz(f,X) -> Lipschitzian linear-Functional of X equals
:: DUALSP04:def 9
In(f,BoundedLinearFunctionals X);
end;
definition
let X be RealUnitarySpace;
let u be linear-Functional of X;
func PreNorms u -> non empty Subset of REAL equals
:: DUALSP04:def 10
{|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 };
end;
registration
let X be RealUnitarySpace,
g be Lipschitzian linear-Functional of X;
cluster PreNorms g -> bounded_above;
end;
definition
let X be RealUnitarySpace;
func BoundedLinearFunctionalsNorm X
-> Function of BoundedLinearFunctionals X,REAL means
:: DUALSP04:def 11
for x be object st x in BoundedLinearFunctionals X holds
it.x = upper_bound PreNorms(Bound2Lipschitz(x,X));
end;
registration
let X be RealUnitarySpace;
let f be Lipschitzian linear-Functional of X;
reduce Bound2Lipschitz(f,X) to f;
end;
theorem :: DUALSP04:16
for X be RealUnitarySpace, f be Lipschitzian linear-Functional of X
holds (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms f;
definition
let X be RealUnitarySpace;
func DualSp X -> non empty NORMSTR equals
:: DUALSP04:def 12
NORMSTR (# BoundedLinearFunctionals X,
Zero_(BoundedLinearFunctionals X, X*'),
Add_(BoundedLinearFunctionals X, X*'),
Mult_(BoundedLinearFunctionals X, X*'),
BoundedLinearFunctionalsNorm X #);
end;
theorem :: DUALSP04:17
for X be RealUnitarySpace, f be Point of DualSp X,
g be Lipschitzian linear-Functional of X
st g=f
holds for t be VECTOR of X holds |.g.t.| <= ||.f.|| * ||.t.||;
theorem :: DUALSP04:18
for X be RealUnitarySpace, f be Point of DualSp X holds 0 <= ||.f.||;
theorem :: DUALSP04:19
for X be RealUnitarySpace,
f be Function of X,REAL, g be Function of RUSp2RNSp X,REAL
st f=g holds
f is additive homogeneous iff g is additive homogeneous;
theorem :: DUALSP04:20
for X be RealUnitarySpace,
f be linear-Functional of X,
g be linear-Functional of RUSp2RNSp X
st f=g holds
f is Lipschitzian iff g is Lipschitzian;
theorem :: DUALSP04:21
for X be RealUnitarySpace holds
BoundedLinearFunctionals X = BoundedLinearFunctionals (RUSp2RNSp X);
theorem :: DUALSP04:22
for X be RealUnitarySpace,
u be linear-Functional of X,
v be linear-Functional of (RUSp2RNSp X)
st u=v holds
PreNorms u = PreNorms v;
theorem :: DUALSP04:23
for X be RealUnitarySpace holds
BoundedLinearFunctionalsNorm X
= BoundedLinearFunctionalsNorm (RUSp2RNSp X);
theorem :: DUALSP04:24
for X be RealUnitarySpace holds
LinearFunctionals X = LinearFunctionals (RUSp2RNSp X);
theorem :: DUALSP04:25
for X be RealUnitarySpace holds
X*' = (RUSp2RNSp X)*';
theorem :: DUALSP04:26
for X be RealUnitarySpace holds
DualSp X = DualSp (RUSp2RNSp X);
begin :: The Orthogonal Projection
theorem :: DUALSP04:27
for X be RealUnitarySpace, M,N be Subspace of X
st the carrier of M c= the carrier of N
holds the carrier of Ort_Comp N c= the carrier of Ort_Comp M;
theorem :: DUALSP04:28
for X be RealUnitarySpace, M be Subspace of X
holds the carrier of M c= the carrier of Ort_Comp (Ort_Comp M);
theorem :: DUALSP04:29
for X be RealUnitarySpace, M be Subspace of X,
x be Point of X
st x in (the carrier of M) /\ the carrier of (Ort_Comp M)
holds x = 0.X;
theorem :: DUALSP04:30
for X be RealUnitarySpace, M be Subspace of X,
N be non empty Subset of X
st N = the carrier of (Ort_Comp M) holds
N is linearly-closed & N is closed;
theorem :: DUALSP04:31
for X be RealHilbertSpace, M be Subspace of X,
N be Subset of X,
x be Point of X, d be Real
st N = the carrier of M & N is closed &
( ex Y be non empty Subset of REAL st
Y = {||.x-y.|| where y is Point of X: y in M}
& d = lower_bound Y >= 0) holds
ex x0 be Point of X st d = ||.x-x0.|| & x0 in M;
theorem :: DUALSP04:32
for X be RealHilbertSpace, M be Subspace of X,
x,x0 be Point of X, d be Real
st x0 in M &
(ex Y be non empty Subset of REAL st
Y = {||.x-y.|| where y is Point of X: y in M}
& d = lower_bound Y >= 0) holds
d = ||.x-x0.|| iff
for w be Point of X st w in M holds w, x-x0 are_orthogonal;
theorem :: DUALSP04:33
for X be RealHilbertSpace, M be Subspace of X,
N be Subset of X, x be Point of X
st N = the carrier of M & N is closed holds
ex y,z be Point of X st
y in M & z in Ort_Comp M & x = y + z;
theorem :: DUALSP04:34
for X be RealUnitarySpace, M be Subspace of X,
x be Point of X,
y1,y2,z1,z2 be Point of X st
y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M &
x = y1 + z1 & x = y2 + z2
holds y1 = y2 & z1 = z2;
begin :: F. Riesz Representation Theorem
theorem :: DUALSP04:35
for X be RealUnitarySpace, f be linear-Functional of X,
y be Point of X
st for x be Point of X holds f.x = x .|. y holds
f is Lipschitzian;
registration
let X be RealUnitarySpace,
f be linear-Functional of X;
cluster f"{0} -> non empty;
end;
theorem :: DUALSP04:36
for X be RealUnitarySpace,
f be Function of X,REAL
st f is additive homogeneous
holds f"{0} is linearly-closed;
definition
let X be RealUnitarySpace,
f be linear-Functional of X;
func UKer(f) -> strict Subspace of X means
:: DUALSP04:def 13
the carrier of it = f"{0};
end;
theorem :: DUALSP04:37
for X be RealUnitarySpace, f be linear-Functional of X
st f is Lipschitzian
holds f"{0} is closed;
theorem :: DUALSP04:38
for V being RealUnitarySpace, W being Subspace of V,
v being VECTOR of V st v <> 0.V holds
v in Ort_Comp W implies not v in W;
theorem :: DUALSP04:39
for X be RealHilbertSpace, f be linear-Functional of X
st f is Lipschitzian holds
ex y be Point of X st
for x be Point of X holds f.x = x .|. y;
theorem :: DUALSP04:40
for X be RealUnitarySpace, f be linear-Functional of X holds
for y1,y2 be Point of X st
for x be Point of X holds f.x = x .|. y1 & f.x = x .|. y2
holds y1 = y2;
theorem :: DUALSP04:41
for X be RealHilbertSpace, f be Point of DualSp X,
g be Lipschitzian linear-Functional of X
st g=f holds
ex y be Point of X st
(for x be Point of X holds g.x = x .|. y)
& ||.f.|| = ||.y.||;