:: BHSP_3 semantic presentation

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

definition

let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is Cauchy means :Def1: :: BHSP_3:def 1
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (seq . n),(seq . m) < r;

end;

:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :

notation

let X be RealUnitarySpace;
let seq be sequence of X;
synonym seq is_Cauchy_sequence for Cauchy seq;

end;

theorem :: BHSP_3:1

for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is_Cauchy_sequence

proof end;

theorem :: BHSP_3:2

for X being RealUnitarySpace
for seq being sequence of X holds
( seq is_Cauchy_sequence iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )

proof end;

theorem :: BHSP_3:3

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence holds
seq1 + seq2 is_Cauchy_sequence

proof end;

theorem :: BHSP_3:4

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence holds
seq1 - seq2 is_Cauchy_sequence

proof end;

theorem Th5: :: BHSP_3:5

for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is_Cauchy_sequence holds
a * seq is_Cauchy_sequence

proof end;

theorem :: BHSP_3:6

for X being RealUnitarySpace
for seq being sequence of X st seq is_Cauchy_sequence holds
- seq is_Cauchy_sequence

proof end;

theorem Th7: :: BHSP_3:7

for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is_Cauchy_sequence holds
seq + x is_Cauchy_sequence

proof end;

theorem :: BHSP_3:8

for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is_Cauchy_sequence holds
seq - x is_Cauchy_sequence

proof end;

theorem :: BHSP_3:9

for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is_Cauchy_sequence

proof end;

definition

let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
pred seq1 is_compared_to seq2 means :Def2: :: BHSP_3:def 2
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq1 . n),(seq2 . n) < r;

end;

:: deftheorem Def2 defines is_compared_to BHSP_3:def 2 :

theorem Th10: :: BHSP_3:10

for X being RealUnitarySpace
for seq being sequence of X holds seq is_compared_to seq

proof end;

theorem Th11: :: BHSP_3:11

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1

proof end;

definition

let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: is_compared_to
redefine pred seq1 is_compared_to seq2;
reflexivity by Th10;
symmetry by Th11;

end;

theorem :: BHSP_3:12

for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3

proof end;

theorem :: BHSP_3:13

for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )

proof end;

theorem :: BHSP_3:14

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st ex k being Nat st
for n being Nat st n >= k holds
seq1 . n = seq2 . n holds
seq1 is_compared_to seq2

proof end;

theorem :: BHSP_3:15

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_Cauchy_sequence & seq1 is_compared_to seq2 holds
seq2 is_Cauchy_sequence

proof end;

theorem :: BHSP_3:16

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent

proof end;

theorem :: BHSP_3:17

for X being RealUnitarySpace
for g being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )

proof end;

definition

let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is bounded means :Def3: :: BHSP_3:def 3
ex M being Real st
( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) );

end;

:: deftheorem Def3 defines bounded BHSP_3:def 3 :

theorem Th18: :: BHSP_3:18

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded

proof end;

theorem Th19: :: BHSP_3:19

for X being RealUnitarySpace
for seq being sequence of X st seq is bounded holds
- seq is bounded

proof end;

theorem :: BHSP_3:20

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded

proof end;

theorem :: BHSP_3:21

for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is bounded holds
a * seq is bounded

proof end;

theorem :: BHSP_3:22

for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is bounded

proof end;

theorem Th23: :: BHSP_3:23

for X being RealUnitarySpace
for seq being sequence of X
for m being Nat ex M being Real st
( M > 0 & ( for n being Nat st n <= m holds
||.(seq . n).|| < M ) )

proof end;

theorem Th24: :: BHSP_3:24

for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded

proof end;

theorem :: BHSP_3:25

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded

proof end;

definition

let X be RealUnitarySpace;
let Nseq be increasing Seq_of_Nat;
let seq be sequence of X;
:: original: *
redefine func seq * Nseq -> sequence of X;
coherence

proof end;

end;

definition

let X be 1-sorted ;
let s be sequence of X;
mode subsequence of s -> sequence of X means :Def4: :: BHSP_3:def 4
ex N being increasing Seq_of_Nat st it = s * N;
existence

proof end;

end;

:: deftheorem Def4 defines subsequence BHSP_3:def 4 :

theorem Th26: :: BHSP_3:26

for X being RealUnitarySpace
for s being sequence of X
for N being increasing Seq_of_Nat
for n being Nat holds (s * N) . n = s . (N . n)

proof end;

theorem :: BHSP_3:27

for X being RealUnitarySpace
for seq being sequence of X holds seq is subsequence of seq

proof end;

theorem :: BHSP_3:28

for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X st seq1 is subsequence of seq2 & seq2 is subsequence of seq3 holds
seq1 is subsequence of seq3

proof end;

theorem Th29: :: BHSP_3:29

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is constant & seq1 is subsequence of seq holds
seq1 is constant

proof end;

theorem :: BHSP_3:30

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

proof end;

theorem Th31: :: BHSP_3:31

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded

proof end;

theorem Th32: :: BHSP_3:32

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent

proof end;

theorem Th33: :: BHSP_3:33

for X being RealUnitarySpace
for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq

proof end;

theorem Th34: :: BHSP_3:34

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is_Cauchy_sequence & seq1 is subsequence of seq holds
seq1 is_Cauchy_sequence

proof end;

definition

let X be RealUnitarySpace;
let seq be sequence of X;
let k be Nat;
func seq ^\ k -> sequence of X means :Def5: :: BHSP_3:def 5
for n being Nat holds it . n = seq . (n + k);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ^\ BHSP_3:def 5 :

theorem :: BHSP_3:35

for X being RealUnitarySpace
for seq being sequence of X holds seq ^\ 0 = seq

proof end;

theorem :: BHSP_3:36

for X being RealUnitarySpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k

proof end;

theorem :: BHSP_3:37

for X being RealUnitarySpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)

proof end;

theorem Th38: :: BHSP_3:38

for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)

proof end;

theorem Th39: :: BHSP_3:39

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat holds (- seq) ^\ k = - (seq ^\ k)

proof end;

theorem :: BHSP_3:40

for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)

proof end;

theorem :: BHSP_3:41

for X being RealUnitarySpace
for a being Real
for seq being sequence of X
for k being Nat holds (a * seq) ^\ k = a * (seq ^\ k)

proof end;

theorem :: BHSP_3:42

for X being RealUnitarySpace
for seq being sequence of X
for Nseq being increasing Seq_of_Nat
for k being Nat holds (seq * Nseq) ^\ k = seq * (Nseq ^\ k)

proof end;

theorem Th43: :: BHSP_3:43

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat holds seq ^\ k is subsequence of seq

proof end;

theorem :: BHSP_3:44

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq )

proof end;

theorem :: BHSP_3:45

canceled;

theorem :: BHSP_3:46

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent

proof end;

theorem :: BHSP_3:47

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is_Cauchy_sequence & ex k being Nat st seq = seq1 ^\ k holds
seq1 is_Cauchy_sequence

proof end;

theorem :: BHSP_3:48

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat st seq is_Cauchy_sequence holds
seq ^\ k is_Cauchy_sequence

proof end;

theorem :: BHSP_3:49

for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k

proof end;

theorem :: BHSP_3:50

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat st seq is bounded holds
seq ^\ k is bounded

proof end;

theorem :: BHSP_3:51

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat st seq is constant holds
seq ^\ k is constant

proof end;

definition

let X be RealUnitarySpace;
attr X is complete means :Def6: :: BHSP_3:def 6
for seq being sequence of X st seq is_Cauchy_sequence holds
seq is convergent;

end;

:: deftheorem Def6 defines complete BHSP_3:def 6 :

notation

let X be RealUnitarySpace;
synonym X is_complete_space for complete X;

end;

theorem :: BHSP_3:52

canceled;

theorem :: BHSP_3:53

for X being RealUnitarySpace
for seq being sequence of X st X is_complete_space & seq is_Cauchy_sequence holds
seq is bounded

proof end;

definition

let X be RealUnitarySpace;
attr X is Hilbert means :: BHSP_3:def 7
( X is RealUnitarySpace & X is_complete_space );

end;

:: deftheorem defines Hilbert BHSP_3:def 7 :

notation

let X be RealUnitarySpace;
synonym X is_Hilbert_space for Hilbert X;

end;