DUALSP04: The Orthogonal Projection and {R}iesz Representation Theorem

:: The Orthogonal Projection and {R}iesz Representation Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 1, 2015
:: Copyright (c) 2015-2021 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 = ||.x.||;

proof end;

proof end;

end;

:: deftheorem Def1 defines normRU DUALSP04:def 1 :

Lm01: for X being RealUnitarySpace holds NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU 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,(normRU X) #);

correctness by Lm01;

end;

:: deftheorem defines RUSp2RNSp DUALSP04:def 2 :

theorem RHS3: :: DUALSP04:1

for X being RealUnitarySpace
for x being Point of X
for x1 being Point of (RUSp2RNSp X) 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 (RUSp2RNSp X) 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 (RUSp2RNSp X) st x = x1 holds
||.x.|| = ||.x1.|| by Def1;

theorem RHS8: :: DUALSP04:4

for X being RealUnitarySpace
for s1 being sequence of X
for s2 being sequence of (RUSp2RNSp X) 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 (RUSp2RNSp X) 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 (RUSp2RNSp X) 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;

cluster RUSp2RNSp X -> complete ;

correctness 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 (RUSp2RNSp X) st
( Z = Y & Z is open );

end;

:: deftheorem defines open DUALSP04:def 3 :

definition

let X be RealUnitarySpace;
let Y be Subset of X;

attr Y is closed means :: DUALSP04:def 4
ex Z being Subset of (RUSp2RNSp X) st
( Z = Y & Z is closed );

end;

:: deftheorem defines closed DUALSP04:def 4 :

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 :

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 :

theorem LM3B: :: DUALSP04:10

for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),REAL
for x0 being Point of X
for y0 being Point of (RUSp2RNSp X) 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 (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 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 :

theorem LM4: :: DUALSP04:13

for X being RealUnitarySpace
for f being Function of X,REAL
for g being 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 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:];

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 );

proof end;

proof end;

end;

:: deftheorem Def10 defines BoundedLinearFunctionals DUALSP04:def 8 :

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

proof end;

registration

let X be RealUnitarySpace;

cluster BoundedLinearFunctionals X -> non empty linearly-closed ;

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,(BoundedLinearFunctionals X));

coherence by Def10;

end;

:: deftheorem defines Bound2Lipschitz DUALSP04:def 9 :

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 } ;

proof end;

end;

:: deftheorem defines PreNorms DUALSP04:def 10 :

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;

cluster PreNorms g -> non empty bounded_above ;

coherence by Th27X;

end;

definition

let X be RealUnitarySpace;

func BoundedLinearFunctionalsNorm X -> Function of (BoundedLinearFunctionals X),REAL means :Def14: :: DUALSP04:def 11
for x being object st x in BoundedLinearFunctionals X holds
it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));

proof end;

proof end;

end;

:: deftheorem Def14 defines BoundedLinearFunctionalsNorm DUALSP04:def 11 :

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 by Th23;

end;

theorem Th24: :: DUALSP04:16

for X being RealUnitarySpace
for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)

proof end;

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;

:: deftheorem defines DualSp DUALSP04:def 12 :

theorem Th26: :: DUALSP04:17

for X being RealUnitarySpace
for f being Point of (DualSp X)
for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

proof end;

theorem Th27: :: DUALSP04:18

for X being RealUnitarySpace
for f being Point of (DualSp X) holds 0 <= ||.f.||

proof end;

theorem LM6A: :: DUALSP04:19

for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),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 (RUSp2RNSp X) 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 (RUSp2RNSp X)

proof end;

theorem LM8: :: DUALSP04:22

for X being RealUnitarySpace
for u being linear-Functional of X
for v being linear-Functional of (RUSp2RNSp X) st u = v holds
PreNorms u = PreNorms v

proof end;

theorem LM9: :: DUALSP04:23

for X being RealUnitarySpace holds BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X)

proof end;

theorem LM10A: :: DUALSP04:24

for X being RealUnitarySpace holds LinearFunctionals X = LinearFunctionals (RUSp2RNSp X)

proof end;

theorem LM10B: :: DUALSP04:25

for X being RealUnitarySpace holds X *' = (RUSp2RNSp X) *'

proof end;

theorem :: DUALSP04:26

for X being RealUnitarySpace holds DualSp X = DualSp (RUSp2RNSp X)

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 (Ort_Comp N) c= the carrier of (Ort_Comp M)

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 (Ort_Comp M))

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 (Ort_Comp M) 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 (Ort_Comp M) 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 * (||.x.|| * ||.x.||)) + (2 * (||.y.|| * ||.y.||))

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 " {0} is empty

proof end;

registration

let X be RealUnitarySpace;
let f be linear-Functional of X;

cluster f " {0} -> non empty ;

correctness 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 " {0} 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 " {0};

existence by KLXY1, RUSUB_1:29;
uniqueness by RUSUB_1:24;

end;

:: deftheorem defuker defines UKer DUALSP04:def 13 :

theorem Lm89A: :: DUALSP04:37

for X being RealUnitarySpace
for f being linear-Functional of X st f is Lipschitzian holds
f " {0} 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 (DualSp X)
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 ) & ||.f.|| = ||.y.|| )

proof end;