BHSP_1: Introduction to Banach and Hilbert spaces

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

begin

definition

attr c₁ is strict ;
struct UNITSTR -> RLSStruct ;
aggr UNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> UNITSTR ;
sel scalar c₁ -> Function of [: the carrier of c₁, the carrier of c₁:],REAL;

end;

registration

cluster non empty strict UNITSTR ;
existence

proof end;

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 ;

end;

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

definition

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

end;

:: deftheorem defines .|. BHSP_1:def 1 :

consider V0 being RealLinearSpace;

Lm1: the carrier of ((0). V0) = {(0. V0)}
by RLSUB_1:def 3;

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

( ( for x, y being VECTOR of ((0). V0) holds nilfunc . [x,y] = 0 ) & 0. V0 in the carrier of ((0). V0) )
by Lm1, FUNCOP_1:13, TARSKI:def 1;

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

Lm3: for u, v being VECTOR of ((0). V0) holds nilfunc . [u,v] = nilfunc . [v,u]

proof end;

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

proof end;

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

proof end;

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

Lm6: now

let x, y, z be Point of UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)), the addF of ((0). V0), the Mult of ((0). V0),nilfunc #); :: thesis:
let a be Real; :: thesis:
H₁( UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)), the addF of ((0). V0), the Mult of ((0). V0),nilfunc #)) = 0. V0 by RLSUB_1:19;
hence ( x .|. x = 0 iff x = H₁( UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)), the addF of ((0). V0), the Mult of ((0). V0),nilfunc #)) ) by Lm1, FUNCOP_1:13, TARSKI:def 1; :: thesis:
thus 0 <= x .|. x by FUNCOP_1:13; :: thesis:
thus x .|. y = y .|. x by Lm3; :: thesis:
thus (x + y) .|. z = (x .|. z) + (y .|. z) :: thesis:

proof

reconsider u = x, v = y, w = z as VECTOR of ((0). V0) ;
(x + y) .|. z = nilfunc . [(u + v),w] ;
hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm4; :: thesis:

end;

thus (a * x) .|. y = a * (x .|. y) :: thesis:

proof

reconsider u = x, v = y as VECTOR of ((0). V0) ;
(a * x) .|. y = nilfunc . [(a * u),v] ;
hence (a * x) .|. y = a * (x .|. y) by Lm5; :: thesis:

end;

definition

let IT be non empty UNITSTR ;
attr IT 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 ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) );

end;

:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def 2 :

registration

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR ;
existence

proof end;

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 func x .|. y -> Real;
commutativity by Def2;

end;

theorem :: BHSP_1:1

canceled;

theorem :: BHSP_1:2

canceled;

theorem :: BHSP_1:3

canceled;

theorem :: BHSP_1:4

canceled;

theorem :: BHSP_1:5

canceled;

theorem :: BHSP_1:6

for X being RealUnitarySpace holds (0. X) .|. (0. X) = 0 by Def2;

theorem :: BHSP_1:7

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:8

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:9

for a being Real
for X being RealUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)

proof end;

theorem Th10: :: BHSP_1:10

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

proof end;

theorem :: BHSP_1:11

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

theorem :: BHSP_1:12

for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = x .|. (- y)

proof end;

theorem Th13: :: BHSP_1:13

for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = - (x .|. y)

proof end;

theorem :: BHSP_1:14

for X being RealUnitarySpace
for x, y being Point of X holds x .|. (- y) = - (x .|. y) by Th13;

theorem Th15: :: BHSP_1:15

for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. (- y) = x .|. y

proof end;

theorem Th16: :: BHSP_1:16

for X being RealUnitarySpace
for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)

proof end;

theorem Th17: :: BHSP_1:17

for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)

proof end;

theorem :: BHSP_1:18

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)

proof end;

theorem Th19: :: BHSP_1:19

for X being RealUnitarySpace
for x being Point of X holds (0. X) .|. x = 0

proof end;

theorem :: BHSP_1:20

for X being RealUnitarySpace
for x being Point of X holds x .|. (0. X) = 0 by Th19;

theorem Th21: :: BHSP_1:21

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

proof end;

theorem :: BHSP_1:22

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

proof end;

theorem Th23: :: BHSP_1:23

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

proof end;

theorem Th24: :: BHSP_1:24

for X being RealUnitarySpace
for x, y being Point of X holds abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))

proof end;

definition

let X be RealUnitarySpace;
let x, y be Point of X;
pred x,y are_orthogonal means :Def3: :: BHSP_1:def 3
x .|. y = 0 ;
symmetry ;

end;

:: deftheorem Def3 defines are_orthogonal BHSP_1:def 3 :

theorem :: BHSP_1:25

canceled;

theorem :: BHSP_1:26

for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
x, - y are_orthogonal

proof end;

theorem :: BHSP_1:27

for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x,y are_orthogonal

proof end;

theorem :: BHSP_1:28

for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x, - y are_orthogonal

proof end;

theorem :: BHSP_1:29

for X being RealUnitarySpace
for x being Point of X holds x, 0. X are_orthogonal

proof end;

theorem :: BHSP_1:30

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)

proof end;

theorem :: BHSP_1:31

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)

proof end;

definition

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

end;

:: deftheorem defines ||. BHSP_1:def 4 :

theorem Th32: :: BHSP_1:32

for X being RealUnitarySpace
for x being Point of X holds
( ||.x.|| = 0 iff x = 0. X )

proof end;

theorem Th33: :: BHSP_1:33

for a being Real
for X being RealUnitarySpace
for x being Point of X holds ||.(a * x).|| = (abs a) * ||.x.||

proof end;

theorem Th34: :: BHSP_1:34

for X being RealUnitarySpace
for x being Point of X holds 0 <= ||.x.||

proof end;

theorem :: BHSP_1:35

for X being RealUnitarySpace
for x, y being Point of X holds abs (x .|. y) <= ||.x.|| * ||.y.|| by Th24;

theorem Th36: :: BHSP_1:36

for X being RealUnitarySpace
for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||

proof end;

theorem Th37: :: BHSP_1:37

for X being RealUnitarySpace
for x being Point of X holds ||.(- x).|| = ||.x.||

proof end;

theorem Th38: :: BHSP_1:38

for X being RealUnitarySpace
for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).||

proof end;

theorem :: BHSP_1:39

for X being RealUnitarySpace
for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||

proof end;

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

proof end;

end;

:: deftheorem defines dist BHSP_1:def 5 :

theorem :: BHSP_1:40

canceled;

theorem Th41: :: BHSP_1:41

for X being RealUnitarySpace
for x being Point of X holds dist (x,x) = 0

proof end;

theorem :: BHSP_1:42

for X being RealUnitarySpace
for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))

proof end;

theorem Th43: :: BHSP_1:43

for X being RealUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) <> 0 )

proof end;

theorem :: BHSP_1:44

for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) >= 0 by Th34;

theorem :: BHSP_1:45

for X being RealUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) > 0 )

proof end;

theorem :: BHSP_1:46

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

theorem :: BHSP_1:47

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

proof end;

theorem :: BHSP_1:48

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

proof end;

theorem :: BHSP_1:49

for X being RealUnitarySpace
for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y)

proof end;

theorem :: BHSP_1:50

for X being RealUnitarySpace
for x, z, y being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))

proof end;

definition

let X be non empty addLoopStr ;
let seq be sequence of X;
canceled;
canceled;
canceled;
canceled;
func - seq -> sequence of X means :Def10: :: BHSP_1:def 10
for n being Element of NAT holds it . n = - (seq . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem BHSP_1:def 6 :

:: deftheorem BHSP_1:def 7 :

:: deftheorem BHSP_1:def 8 :

:: deftheorem BHSP_1:def 9 :

:: deftheorem Def10 defines - BHSP_1:def 10 :

definition

let X be non empty addLoopStr ;
let seq be sequence of X;
let x be Point of X;
canceled;
func seq + x -> sequence of X means :Def12: :: BHSP_1:def 12
for n being Element of NAT holds it . n = (seq . n) + x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem BHSP_1:def 11 :

:: deftheorem Def12 defines + BHSP_1:def 12 :

theorem :: BHSP_1:51

canceled;

theorem :: BHSP_1:52

canceled;

theorem :: BHSP_1:53

canceled;

theorem :: BHSP_1:54

canceled;

theorem :: BHSP_1:55

canceled;

definition

let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: +
redefine func seq1 + seq2 -> Element of bool [:NAT, the carrier of X:];
commutativity

proof end;

end;

theorem :: BHSP_1:56

for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3

proof end;

theorem :: BHSP_1:57

for X being RealUnitarySpace
for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds
seq is constant

proof end;

theorem :: BHSP_1:58

for X being RealUnitarySpace
for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 - seq2 holds
seq is constant

proof end;

theorem :: BHSP_1:59

for a being Real
for X being RealUnitarySpace
for seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds
seq is constant

proof end;

theorem :: BHSP_1:60

canceled;

theorem :: BHSP_1:61

canceled;

theorem :: BHSP_1:62

canceled;

theorem :: BHSP_1:63

canceled;

theorem :: BHSP_1:64

canceled;

theorem :: BHSP_1:65

canceled;

theorem :: BHSP_1:66

canceled;

theorem :: BHSP_1:67

canceled;

theorem :: BHSP_1:68

canceled;

theorem :: BHSP_1:69

canceled;

theorem :: BHSP_1:70

canceled;

theorem :: BHSP_1:71

for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)

proof end;

theorem :: BHSP_1:72

for X being RealUnitarySpace
for seq being sequence of X holds seq = seq + (0. X)

proof end;

theorem :: BHSP_1:73

for a being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)

proof end;

theorem :: BHSP_1:74

for a, b being Real
for X being RealUnitarySpace
for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)

proof end;

theorem :: BHSP_1:75

for a, b being Real
for X being RealUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)

proof end;

theorem :: BHSP_1:76

for X being RealUnitarySpace
for seq being sequence of X holds 1 * seq = seq

proof end;

theorem :: BHSP_1:77

for X being RealUnitarySpace
for seq being sequence of X holds (- 1) * seq = - seq

proof end;

theorem :: BHSP_1:78

for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)

proof end;

theorem :: BHSP_1:79

for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)

proof end;

theorem :: BHSP_1:80

for X being RealUnitarySpace
for seq being sequence of X holds seq = seq - (0. X)

proof end;

theorem :: BHSP_1:81

for X being RealUnitarySpace
for seq being sequence of X holds seq = - (- seq)

proof end;

theorem :: BHSP_1:82

for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

proof end;

theorem :: BHSP_1:83

for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)

proof end;

theorem :: BHSP_1:84

for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

proof end;

theorem :: BHSP_1:85

for a being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)

proof end;