:: The Orthogonal Projection and {R}iesz Representation Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2015-2019 Association of Mizar Users

definition
let X be RealUnitarySpace;
func normRU X -> Function of the carrier of X,REAL means :Def1: :: DUALSP04:def 1
for x being Point of X holds it . x = ;
existence
ex b1 being Function of the carrier of X,REAL st
for x being Point of X holds b1 . x =
proof end;
uniqueness
for b1, b2 being Function of the carrier of X,REAL st ( for x being Point of X holds b1 . x = ) & ( for x being Point of X holds b2 . x = ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines normRU DUALSP04:def 1 :
for X being RealUnitarySpace
for b2 being Function of the carrier of X,REAL holds
( b2 = normRU X iff for x being Point of X holds b2 . x = );

Lm01: for X being RealUnitarySpace holds NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,() #) is RealNormSpace
proof 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,() #);
correctness
coherence
NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,() #) is RealNormSpace
;
by Lm01;
end;

:: deftheorem defines RUSp2RNSp DUALSP04:def 2 :
for X being RealUnitarySpace holds RUSp2RNSp X = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,() #);

theorem RHS3: :: DUALSP04:1
for X being RealUnitarySpace
for x being Point of X
for x1 being Point of () st x = x1 holds
- x = - x1
proof end;

theorem RHS4: :: DUALSP04:2
for X being RealUnitarySpace
for x, y being Point of X
for x1, y1 being Point of () st x = x1 & y = y1 holds
x - y = x1 - y1 by RHS3;

theorem RHS6: :: DUALSP04:3
for X being RealUnitarySpace
for x being Point of X
for x1 being Point of () st x = x1 holds
= ||.x1.|| by Def1;

theorem RHS8: :: DUALSP04:4
for X being RealUnitarySpace
for s1 being sequence of X
for s2 being sequence of () st s1 = s2 holds
( s1 is convergent iff s2 is convergent )
proof end;

theorem RHS9: :: DUALSP04:5
for X being RealUnitarySpace
for s1 being sequence of X
for s2 being sequence of () st s1 = s2 & s1 is convergent holds
lim s1 = lim s2
proof end;

theorem RHS11a: :: DUALSP04:6
for X being RealUnitarySpace
for s1 being sequence of X
for s2 being sequence of () st s1 = s2 holds
( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy )
proof end;

theorem RHS11b: :: DUALSP04:7
for X being RealUnitarySpace holds
( X is complete iff RUSp2RNSp X is complete )
proof end;

registration
let X be RealHilbertSpace;
correctness
coherence ;
by RHS11b;
end;

definition
let X be RealUnitarySpace;
let Y be Subset of X;
attr Y is open means :: DUALSP04:def 3
ex Z being Subset of () st
( Z = Y & Z is open );
end;

:: deftheorem defines open DUALSP04:def 3 :
for X being RealUnitarySpace
for Y being Subset of X holds
( Y is open iff ex Z being Subset of () st
( Z = Y & Z is open ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
attr Y is closed means :: DUALSP04:def 4
ex Z being Subset of () st
( Z = Y & Z is closed );
end;

:: deftheorem defines closed DUALSP04:def 4 :
for X being RealUnitarySpace
for Y being Subset of X holds
( Y is closed iff ex Z being Subset of () st
( Z = Y & Z is closed ) );

theorem LM1: :: DUALSP04:8
for X being RealUnitarySpace
for Y being Subset of X holds
( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y )
proof end;

theorem :: DUALSP04:9
for X being RealUnitarySpace
for Y being Subset of X holds
( Y is open iff Y ` is closed )
proof 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 :: DUALSP04:def 5
( x0 in dom f & ( for s1 being 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;

:: deftheorem defines is_continuous_in DUALSP04:def 5 :
for X being RealUnitarySpace
for f being PartFunc of the carrier of X,REAL
for x0 being Point of X holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being 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) ) ) ) );

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 being Point of X st x0 in Y holds
f | Y is_continuous_in x0 ) );
end;

:: deftheorem defines is_continuous_on DUALSP04:def 6 :
for X being RealUnitarySpace
for f being PartFunc of the carrier of X,REAL
for Y being set holds
( f is_continuous_on Y iff ( Y c= dom f & ( for x0 being Point of X st x0 in Y holds
f | Y is_continuous_in x0 ) ) );

theorem LM3B: :: DUALSP04:10
for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (),REAL
for x0 being Point of X
for y0 being Point of () st f = g & x0 = y0 holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
proof end;

theorem LM3C: :: DUALSP04:11
for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (),REAL st f = g holds
( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of () )
proof end;

theorem :: DUALSP04:12
for X being RealUnitarySpace
for w being Point of X
for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds
f is_continuous_on the carrier of X
proof 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 :: DUALSP04:def 7
( Y c= dom f & ex r being Real st
( 0 < r & ( for x1, x2 being Point of X st x1 in Y & x2 in Y holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem defines is_Lipschitzian_on DUALSP04:def 7 :
for X being RealUnitarySpace
for Y being set
for f being PartFunc of the carrier of X,REAL holds
( f is_Lipschitzian_on Y iff ( Y c= dom f & ex r being Real st
( 0 < r & ( for x1, x2 being Point of X st x1 in Y & x2 in Y holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ) );

theorem LM4: :: DUALSP04:13
for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (),REAL st f = g holds
( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of () )
proof end;

theorem LM5: :: DUALSP04:14
for X being RealUnitarySpace
for f being Function of X,REAL st f is_Lipschitzian_on the carrier of X holds
f is_continuous_on the carrier of X
proof end;

Th16: for X being RealUnitarySpace
for f being linear-Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian

proof end;

theorem Th21X: :: DUALSP04:15
for X being RealUnitarySpace
for F being linear-Functional of X st F = the carrier of X --> 0 holds
F is Lipschitzian
proof end;

registration
let X be RealUnitarySpace;
cluster V1() V4( the carrier of X) V5( REAL ) non empty Function-like total quasi_total additive homogeneous V166() V167() V168() Lipschitzian for Element of bool [: the carrier of X,REAL:];
correctness
existence
ex b1 being linear-Functional of X st b1 is Lipschitzian
;
proof end;
end;

definition
let X be RealUnitarySpace;
func BoundedLinearFunctionals X -> Subset of (X *') means :Def10: :: DUALSP04:def 8
for x being set holds
( x in it iff x is Lipschitzian linear-Functional of X );
existence
ex b1 being Subset of (X *') st
for x being set holds
( x in b1 iff x is Lipschitzian linear-Functional of X )
proof end;
uniqueness
for b1, b2 being Subset of (X *') st ( for x being set holds
( x in b1 iff x is Lipschitzian linear-Functional of X ) ) & ( for x being set holds
( x in b2 iff x is Lipschitzian linear-Functional of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines BoundedLinearFunctionals DUALSP04:def 8 :
for X being RealUnitarySpace
for b2 being Subset of (X *') holds
( b2 = BoundedLinearFunctionals X iff for x being set holds
( x in b2 iff x is Lipschitzian linear-Functional of X ) );

Th17: for X being RealUnitarySpace holds BoundedLinearFunctionals X is linearly-closed
proof end;

registration
let X be RealUnitarySpace;
coherence
proof end;
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,);
coherence
In (f,) is Lipschitzian linear-Functional of X
by Def10;
end;

:: deftheorem defines Bound2Lipschitz DUALSP04:def 9 :
for X being RealUnitarySpace
for f being object holds Bound2Lipschitz (f,X) = In (f,);

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 : <= 1 } ;
coherence
{ |.(u . t).| where t is VECTOR of X : <= 1 } is non empty Subset of REAL
proof end;
end;

:: deftheorem defines PreNorms DUALSP04:def 10 :
for X being RealUnitarySpace
for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : <= 1 } ;

Th27X: for X being RealUnitarySpace
for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above

proof end;

registration
let X be RealUnitarySpace;
let g be Lipschitzian linear-Functional of X;
coherence by Th27X;
end;

definition
let X be RealUnitarySpace;
func BoundedLinearFunctionalsNorm X -> Function of ,REAL means :Def14: :: DUALSP04:def 11
for x being object st x in BoundedLinearFunctionals X holds
it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));
existence
ex b1 being Function of ,REAL st
for x being object st x in BoundedLinearFunctionals X holds
b1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)))
proof end;
uniqueness
for b1, b2 being Function of ,REAL st ( for x being object st x in BoundedLinearFunctionals X holds
b1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) & ( for x being object st x in BoundedLinearFunctionals X holds
b2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines BoundedLinearFunctionalsNorm DUALSP04:def 11 :
for X being RealUnitarySpace
for b2 being Function of ,REAL holds
( b2 = BoundedLinearFunctionalsNorm X iff for x being object st x in BoundedLinearFunctionals X holds
b2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) );

Th23: for X being RealUnitarySpace
for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f

proof end;

registration
let X be RealUnitarySpace;
let f be Lipschitzian linear-Functional of X;
reduce Bound2Lipschitz (f,X) to f;
reducibility
Bound2Lipschitz (f,X) = f
by Th23;
end;

theorem Th24: :: DUALSP04:16
for X being RealUnitarySpace
for f being Lipschitzian linear-Functional of X holds . f = upper_bound ()
proof end;

definition
let X be RealUnitarySpace;
func DualSp X -> non empty NORMSTR equals :: DUALSP04:def 12
NORMSTR(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))), #);
coherence
NORMSTR(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))), #) is non empty NORMSTR
;
end;

:: deftheorem defines DualSp DUALSP04:def 12 :
for X being RealUnitarySpace holds DualSp X = NORMSTR(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))), #);

theorem Th26: :: DUALSP04:17
for X being RealUnitarySpace
for f being Point of ()
for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= *
proof end;

theorem Th27: :: DUALSP04:18
for X being RealUnitarySpace
for f being Point of () holds 0 <=
proof end;

theorem LM6A: :: DUALSP04:19
for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (),REAL st f = g holds
( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )
proof end;

theorem LM6B: :: DUALSP04:20
for X being RealUnitarySpace
for f being linear-Functional of X
for g being linear-Functional of () st f = g holds
( f is Lipschitzian iff g is Lipschitzian )
proof end;

theorem LM6: :: DUALSP04:21
for X being RealUnitarySpace holds BoundedLinearFunctionals X = BoundedLinearFunctionals ()
proof end;

theorem LM8: :: DUALSP04:22
for X being RealUnitarySpace
for u being linear-Functional of X
for v being linear-Functional of () st u = v holds
PreNorms u = PreNorms v
proof end;

theorem LM9: :: DUALSP04:23
proof end;

theorem LM10A: :: DUALSP04:24
for X being RealUnitarySpace holds LinearFunctionals X = LinearFunctionals ()
proof end;

theorem LM10B: :: DUALSP04:25
for X being RealUnitarySpace holds X *' = () *'
proof end;

theorem :: DUALSP04:26
for X being RealUnitarySpace holds DualSp X = DualSp ()
proof end;

theorem :: DUALSP04:27
for X being RealUnitarySpace
for M, N being Subspace of X st the carrier of M c= the carrier of N holds
the carrier of () c= the carrier of ()
proof end;

theorem :: DUALSP04:28
for X being RealUnitarySpace
for M being Subspace of X holds the carrier of M c= the carrier of (Ort_Comp ())
proof end;

theorem Lm814: :: DUALSP04:29
for X being RealUnitarySpace
for M being Subspace of X
for x being Point of X st x in the carrier of M /\ the carrier of () holds
x = 0. X
proof end;

theorem :: DUALSP04:30
for X being RealUnitarySpace
for M being Subspace of X
for N being non empty Subset of X st N = the carrier of () holds
( N is linearly-closed & N is closed )
proof end;

Lm88A: for X being RealUnitarySpace
for x, y being Point of X holds (||.(x + y).|| * ||.(x + y).||) + (||.(x - y).|| * ||.(x - y).||) = (2 * ()) + (2 * ())

proof end;

theorem Lm88: :: DUALSP04:31
for X being RealHilbertSpace
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 )
proof end;

theorem Lm87A: :: DUALSP04:32
for X being RealHilbertSpace
for M being Subspace of X
for x, x0 being Point of X
for d being Real st x0 in M & 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
( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal )
proof end;

theorem Th87A: :: DUALSP04:33
for X being RealHilbertSpace
for M being Subspace of X
for N being Subset of X
for x being Point of X st N = the carrier of M & N is closed holds
ex y, z being Point of X st
( y in M & z in Ort_Comp M & x = y + z )
proof end;

theorem :: DUALSP04:34
for X being RealUnitarySpace
for M being Subspace of X
for x, y1, y2, z1, z2 being 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 end;

theorem :: DUALSP04:35
for X being RealUnitarySpace
for f being linear-Functional of X
for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds
f is Lipschitzian
proof end;

KERX1: for X being RealUnitarySpace
for f being Function of X,REAL st f is homogeneous holds
not f " is empty

proof end;

registration
let X be RealUnitarySpace;
let f be linear-Functional of X;
cluster f " -> non empty ;
correctness
coherence
not f " is empty
;
by KERX1;
end;

theorem KLXY1: :: DUALSP04:36
for X being RealUnitarySpace
for f being Function of X,REAL st f is additive & f is homogeneous holds
f " is linearly-closed
proof end;

definition
let X be RealUnitarySpace;
let f be linear-Functional of X;
func UKer f -> strict Subspace of X means :defuker: :: DUALSP04:def 13
the carrier of it = f " ;
existence
ex b1 being strict Subspace of X st the carrier of b1 = f "
by ;
uniqueness
for b1, b2 being strict Subspace of X st the carrier of b1 = f " & the carrier of b2 = f " holds
b1 = b2
by RUSUB_1:24;
end;

:: deftheorem defuker defines UKer DUALSP04:def 13 :
for X being RealUnitarySpace
for f being linear-Functional of X
for b3 being strict Subspace of X holds
( b3 = UKer f iff the carrier of b3 = f " );

theorem Lm89A: :: DUALSP04:37
for X being RealUnitarySpace
for f being linear-Functional of X st f is Lipschitzian holds
f " is closed
proof end;

theorem Lm89B: :: DUALSP04:38
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds
not v in W
proof end;

theorem Th89A: :: DUALSP04:39
for X being RealHilbertSpace
for f being linear-Functional of X st f is Lipschitzian holds
ex y being Point of X st
for x being Point of X holds f . x = x .|. y
proof end;

theorem :: DUALSP04:40
for X being RealUnitarySpace
for f being linear-Functional of X
for y1, y2 being Point of X st ( for x being Point of X holds
( f . x = x .|. y1 & f . x = x .|. y2 ) ) holds
y1 = y2
proof end;

theorem :: DUALSP04:41
for X being RealHilbertSpace
for f being Point of ()
for g being Lipschitzian linear-Functional of X st g = f holds
ex y being Point of X st
( ( for x being Point of X holds g . x = x .|. y ) & = )
proof end;