:: Introduction to Banach and Hilbert spaces - Part I
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct UNITSTR  ->  RLSStruct ;
aggrUNITSTR(# carrier, ZeroF, addF, Mult, scalar #) ->  UNITSTR ;
sel scalar c1 ->  Function of [: the carrier of c1, the carrier of c1:],REAL;
end;

registration
cluster non empty strict for UNITSTR ;
existence
 ex b1 being UNITSTR st
( not b1 is empty & b1 is strict )
proofend;
end;

registration
let D be non empty set ;
let Z be Element of D;
let a be BinOp of D;
let m be Function of [:REAL,D:],D;
let s be Function of [:D,D:],REAL;
cluster UNITSTR(# D,Z,a,m,s #) ->  non empty ;
coherence
 not UNITSTR(# D,Z,a,m,s #) is empty ;
end;

deffunc H1( UNITSTR ) ->  Element of the carrier of $1 = 0. $1;

definition
let X be non empty UNITSTR ;
let x, y be Point of X;
funcx .|. y ->  Real equals :: BHSP_1:def 1
 the scalar of X . [x,y];
correctness
coherence
the scalar of X . [x,y] is Real;
;
end;

:: deftheorem  defines .|. BHSP_1:def_1_:_
 for X being non empty UNITSTR
for x, y being Point of X holds x .|. y = the scalar of X . [x,y];

set V0 = the RealLinearSpace;

Lm1:  the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def_3;

reconsider nilfunc = [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):] --> 0 as Function of [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):],REAL by FUNCOP_1:45;

 ( ( for x, y being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [x,y] = 0 ) & 0. the RealLinearSpace in the carrier of ((0). the RealLinearSpace) )
by Lm1, FUNCOP_1:7, TARSKI:def_1;

then Lm2:  nilfunc . [(0. the RealLinearSpace),(0. the RealLinearSpace)] = 0
;

Lm3:  for u, v being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [u,v] = nilfunc . [v,u]
proofend;

Lm4:  for u, v, w being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
proofend;

Lm5:  for u, v being VECTOR of ((0). the RealLinearSpace)
for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
proofend;

set X0 = UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #);

Lm6: now__::_thesis:_for_x,_y,_z_being_Point_of_UNITSTR(#_the_carrier_of_((0)._the_RealLinearSpace),(0._((0)._the_RealLinearSpace)),_the_addF_of_((0)._the_RealLinearSpace),_the_Mult_of_((0)._the_RealLinearSpace),nilfunc_#)
for_a_being_Real_holds_
(_(_x_.|._x_=_0_implies_x_=_H1(_UNITSTR(#_the_carrier_of_((0)._the_RealLinearSpace),(0._((0)._the_RealLinearSpace)),_the_addF_of_((0)._the_RealLinearSpace),_the_Mult_of_((0)._the_RealLinearSpace),nilfunc_#))_)_&amp;_(_x_=_H1(_UNITSTR(#_the_carrier_of_((0)._the_RealLinearSpace),(0._((0)._the_RealLinearSpace)),_the_addF_of_((0)._the_RealLinearSpace),_the_Mult_of_((0)._the_RealLinearSpace),nilfunc_#))_implies_x_.|._x_=_0_)_&amp;_0_<=_x_.|._x_&amp;_x_.|._y_=_y_.|._x_&amp;_(x_+_y)_.|._z_=_(x_.|._z)_+_(y_.|._z)_&amp;_(a_*_x)_.|._y_=_a_*_(x_.|._y)_)
let x, y, z be Point of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: for a being Real holds
( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) &amp; ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = 0 ) &amp; 0 <= x .|. x &amp; x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
let a be Real; ::_thesis: ( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) &amp; ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = 0 ) &amp; 0 <= x .|. x &amp; x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
 H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) = 0. the RealLinearSpace by RLSUB_1:11;
hence  ( x .|. x = 0 iff x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) by Lm1, FUNCOP_1:7, TARSKI:def_1; ::_thesis: ( 0 <= x .|. x &amp; x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
thus  0 <= x .|. x by FUNCOP_1:7; ::_thesis: ( x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
thus  x .|. y = y .|. x by Lm3; ::_thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
thus  (x + y) .|. z = (x .|. z) + (y .|. z) ::_thesis: (a * x) .|. y = a * (x .|. y)
proof
reconsider u = x, v = y, w = z as VECTOR of ((0). the RealLinearSpace) ;
 (x + y) .|. z = nilfunc . [(u + v),w] ;
hence  (x + y) .|. z = (x .|. z) + (y .|. z) by Lm4; ::_thesis: verum
end;
thus  (a * x) .|. y = a * (x .|. y) ::_thesis: verum
proof
reconsider u = x, v = y as VECTOR of ((0). the RealLinearSpace) ;
 (a * x) .|. y = nilfunc . [(a * u),v] ;
hence  (a * x) .|. y = a * (x .|. y) by Lm5; ::_thesis: verum
end;
end;

definition
let IT be non empty UNITSTR ;
attrIT is RealUnitarySpace-like  means :Def2: :: BHSP_1:def 2
 for x, y, z being Point of IT
for a being Real holds
( ( x .|. x = 0 implies x = 0. IT ) &amp; ( x = 0. IT implies x .|. x = 0 ) &amp; 0 <= x .|. x &amp; x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) );
end;

:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def_2_:_
 for IT being non empty UNITSTR holds
( IT is RealUnitarySpace-like iff for x, y, z being Point of IT
for a being Real holds
( ( x .|. x = 0 implies x = 0. IT ) &amp; ( x = 0. IT implies x .|. x = 0 ) &amp; 0 <= x .|. x &amp; x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for UNITSTR ;
existence
 ex b1 being non empty UNITSTR st
( b1 is RealUnitarySpace-like &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is strict )
proofend;
end;

definition
mode RealUnitarySpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR ;
end;

definition
let X be RealUnitarySpace;
let x, y be Point of X;
:: original:.|.
redefine funcx .|. y ->  Real;
commutativity
 for x, y being Point of X holds x .|. y = y .|. x by Def2;
end;

theorem :: BHSP_1:1
for X being RealUnitarySpace holds (0. X) .|. (0. X) = 0 by Def2;

theorem :: BHSP_1:2
for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z) by Def2;

theorem :: BHSP_1:3
for a being Real
for X being RealUnitarySpace
for x, y being Point of X holds x .|. (a * y) = a * (x .|. y) by Def2;

theorem :: BHSP_1:4
for a being Real
for X being RealUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)
proofend;

theorem Th5: :: BHSP_1:5
for a, b being Real
for X being RealUnitarySpace
for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
proofend;

theorem :: BHSP_1:6
for a, b being Real
for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z)) by Th5;

theorem :: BHSP_1:7
for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = x .|. (- y)
proofend;

theorem Th8: :: BHSP_1:8
for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = - (x .|. y)
proofend;

theorem :: BHSP_1:9
for X being RealUnitarySpace
for x, y being Point of X holds x .|. (- y) = - (x .|. y) by Th8;

theorem Th10: :: BHSP_1:10
for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. (- y) = x .|. y
proofend;

theorem Th11: :: BHSP_1:11
for X being RealUnitarySpace
for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)
proofend;

theorem Th12: :: BHSP_1:12
for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)
proofend;

theorem :: BHSP_1:13
for X being RealUnitarySpace
for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)
proofend;

theorem Th14: :: BHSP_1:14
for X being RealUnitarySpace
for x being Point of X holds (0. X) .|. x = 0
proofend;

theorem :: BHSP_1:15
for X being RealUnitarySpace
for x being Point of X holds x .|. (0. X) = 0 by Th14;

theorem Th16: :: BHSP_1:16
for X being RealUnitarySpace
for x, y being Point of X holds (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y)
proofend;

theorem :: BHSP_1:17
for X being RealUnitarySpace
for x, y being Point of X holds (x + y) .|. (x - y) = (x .|. x) - (y .|. y)
proofend;

theorem Th18: :: BHSP_1:18
for X being RealUnitarySpace
for x, y being Point of X holds (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)
proofend;

theorem Th19: :: BHSP_1:19
for X being RealUnitarySpace
for x, y being Point of X holds abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
proofend;

definition
let X be RealUnitarySpace;
let x, y be Point of X;
predx,y are_orthogonal  means :Def3: :: BHSP_1:def 3
x .|. y = 0 ;
symmetry
 for x, y being Point of X st x .|. y = 0 holds
y .|. x = 0 ;
end;

:: deftheorem Def3 defines are_orthogonal BHSP_1:def_3_:_
 for X being RealUnitarySpace
for x, y being Point of X holds
( x,y are_orthogonal iff x .|. y = 0 );

theorem :: BHSP_1:20
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
x, - y are_orthogonal
proofend;

theorem :: BHSP_1:21
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x,y are_orthogonal
proofend;

theorem :: BHSP_1:22
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x, - y are_orthogonal
proofend;

theorem :: BHSP_1:23
for X being RealUnitarySpace
for x being Point of X holds x, 0. X are_orthogonal
proofend;

theorem :: BHSP_1:24
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x + y) .|. (x + y) = (x .|. x) + (y .|. y)
proofend;

theorem :: BHSP_1:25
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x - y) .|. (x - y) = (x .|. x) + (y .|. y)
proofend;

definition
let X be RealUnitarySpace;
let x be Point of X;
func||.x.|| ->  Real equals :: BHSP_1:def 4
 sqrt (x .|. x);
correctness
coherence
sqrt (x .|. x) is Real;
;
end;

:: deftheorem  defines ||. BHSP_1:def_4_:_
 for X being RealUnitarySpace
for x being Point of X holds ||.x.|| = sqrt (x .|. x);

theorem Th26: :: BHSP_1:26
for X being RealUnitarySpace
for x being Point of X holds
( ||.x.|| = 0 iff x = 0. X )
proofend;

theorem Th27: :: BHSP_1:27
for a being Real
for X being RealUnitarySpace
for x being Point of X holds ||.(a * x).|| = (abs a) * ||.x.||
proofend;

theorem Th28: :: BHSP_1:28
for X being RealUnitarySpace
for x being Point of X holds 0 <= ||.x.||
proofend;

theorem :: BHSP_1:29
for X being RealUnitarySpace
for x, y being Point of X holds abs (x .|. y) <= ||.x.|| * ||.y.|| by Th19;

theorem Th30: :: BHSP_1:30
for X being RealUnitarySpace
for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||
proofend;

theorem Th31: :: BHSP_1:31
for X being RealUnitarySpace
for x being Point of X holds ||.(- x).|| = ||.x.||
proofend;

theorem Th32: :: BHSP_1:32
for X being RealUnitarySpace
for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).||
proofend;

theorem :: BHSP_1:33
for X being RealUnitarySpace
for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
proofend;

definition
let X be RealUnitarySpace;
let x, y be Point of X;
func dist (x,y) ->  Real equals :: BHSP_1:def 5
||.(x - y).||;
correctness
coherence
||.(x - y).|| is Real;
;
commutativity
 for b1 being Real
for x, y being Point of X st b1 = ||.(x - y).|| holds
b1 = ||.(y - x).||
proofend;
end;

:: deftheorem  defines dist BHSP_1:def_5_:_
 for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;

theorem Th34: :: BHSP_1:34
for X being RealUnitarySpace
for x being Point of X holds dist (x,x) = 0
proofend;

theorem :: BHSP_1:35
for X being RealUnitarySpace
for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
proofend;

theorem Th36: :: BHSP_1:36
for X being RealUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) <> 0 )
proofend;

theorem :: BHSP_1:37
for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) >= 0 by Th28;

theorem :: BHSP_1:38
for X being RealUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) > 0 )
proofend;

theorem :: BHSP_1:39
for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) = sqrt ((x - y) .|. (x - y)) ;

theorem :: BHSP_1:40
for X being RealUnitarySpace
for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))
proofend;

theorem :: BHSP_1:41
for X being RealUnitarySpace
for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))
proofend;

theorem :: BHSP_1:42
for X being RealUnitarySpace
for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
proofend;

theorem :: BHSP_1:43
for X being RealUnitarySpace
for x, z, y being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
proofend;

definition
let X be non empty addLoopStr ;
let seq be sequence of X;
let x be Point of X;
funcseq + x ->  sequence of X means :Def6: :: BHSP_1:def 6
 for n being Element of NAT holds it . n = (seq . n) + x;
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (seq . n) + x
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (seq . n) + x ) &amp; ( for n being Element of NAT holds b2 . n = (seq . n) + x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines + BHSP_1:def_6_:_
 for X being non empty addLoopStr
for seq being sequence of X
for x being Point of X
for b4 being sequence of X holds
( b4 = seq + x iff for n being Element of NAT holds b4 . n = (seq . n) + x );

theorem Th44: :: BHSP_1:44
for n being Element of NAT
for X being non empty addLoopStr
for seq being sequence of X holds (- seq) . n = - (seq . n)
proofend;

definition
let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
:: original:+
redefine funcseq1 + seq2 ->  Element of bool [:NAT, the carrier of X:];
commutativity
 for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1
proofend;
end;

theorem :: BHSP_1:45
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
proofend;

theorem :: BHSP_1:46
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is constant &amp; seq2 is constant holds
seq1 + seq2 is constant
proofend;

theorem :: BHSP_1:47
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is constant &amp; seq2 is constant holds
seq1 - seq2 is constant
proofend;

theorem :: BHSP_1:48
for a being Real
for X being RealUnitarySpace
for seq1 being sequence of X st seq1 is constant holds
a * seq1 is constant
proofend;

theorem :: BHSP_1:49
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)
proofend;

theorem :: BHSP_1:50
for X being RealUnitarySpace
for seq being sequence of X holds seq = seq + (0. X)
proofend;

theorem :: BHSP_1:51
for a being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)
proofend;

theorem :: BHSP_1:52
for a, b being Real
for X being RealUnitarySpace
for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)
proofend;

theorem :: BHSP_1:53
for a, b being Real
for X being RealUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)
proofend;

theorem :: BHSP_1:54
for X being RealUnitarySpace
for seq being sequence of X holds 1 * seq = seq
proofend;

theorem :: BHSP_1:55
for X being RealUnitarySpace
for seq being sequence of X holds (- 1) * seq = - seq
proofend;

theorem :: BHSP_1:56
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)
proofend;

theorem :: BHSP_1:57
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)
proofend;

theorem :: BHSP_1:58
for X being RealUnitarySpace
for seq being sequence of X holds seq = seq - (0. X)
proofend;

theorem :: BHSP_1:59
for X being RealUnitarySpace
for seq being sequence of X holds seq = - (- seq)
proofend;

theorem :: BHSP_1:60
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proofend;

theorem :: BHSP_1:61
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
proofend;

theorem :: BHSP_1:62
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proofend;

theorem :: BHSP_1:63
for a being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)
proofend;