:: BHSP_3 semantic presentation

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

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is Cauchy means :Def1: :: BHSP_3:def 1
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃, b₄ being Nat st b₃ >= b₂ & b₄ >= b₂ holds
dist (a₂ . b₃),(a₂ . b₄) < b₁;

end;

:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :

notation

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
synonym c₂ is_Cauchy_sequence for Cauchy c₂;

end;

theorem Th1: :: BHSP_3:1

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is_Cauchy_sequence

proof end;

theorem Th2: :: BHSP_3:2

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is_Cauchy_sequence iff for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅, b₆ being Nat st b₅ >= b₄ & b₆ >= b₄ holds
||.((b₂ . b₅) - (b₂ . b₆)).|| < b₃ )

proof end;

theorem Th3: :: BHSP_3:3

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_Cauchy_sequence & b₃ is_Cauchy_sequence holds
b₂ + b₃ is_Cauchy_sequence

proof end;

theorem Th4: :: BHSP_3:4

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_Cauchy_sequence & b₃ is_Cauchy_sequence holds
b₂ - b₃ is_Cauchy_sequence

proof end;

theorem Th5: :: BHSP_3:5

for b₁ being RealUnitarySpace
for b₂ being Real
for b₃ being sequence of b₁ st b₃ is_Cauchy_sequence holds
b₂ * b₃ is_Cauchy_sequence

proof end;

theorem Th6: :: BHSP_3:6

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is_Cauchy_sequence holds
- b₂ is_Cauchy_sequence

proof end;

theorem Th7: :: BHSP_3:7

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is_Cauchy_sequence holds
b₃ + b₂ is_Cauchy_sequence

proof end;

theorem Th8: :: BHSP_3:8

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is_Cauchy_sequence holds
b₃ - b₂ is_Cauchy_sequence

proof end;

theorem Th9: :: BHSP_3:9

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
b₂ is_Cauchy_sequence

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂, c₃ be sequence of c₁;
pred c₂ is_compared_to c₃ means :Def2: :: BHSP_3:def 2
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
dist (a₂ . b₃),(a₃ . b₃) < b₁;

end;

:: deftheorem Def2 defines is_compared_to BHSP_3:def 2 :

theorem Th10: :: BHSP_3:10

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds b₂ is_compared_to b₂

proof end;

theorem Th11: :: BHSP_3:11

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_compared_to b₃ holds
b₃ is_compared_to b₂

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂, c₃ be sequence of c₁;
redefine pred is_compared_to as c₂ is_compared_to c₃;
reflexivity by Th10;
symmetry by Th11;

end;

theorem Th12: :: BHSP_3:12

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is_compared_to b₃ & b₃ is_compared_to b₄ holds
b₂ is_compared_to b₄

proof end;

theorem Th13: :: BHSP_3:13

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ holds
( b₂ is_compared_to b₃ iff for b₄ being Real st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₆ >= b₅ holds
||.((b₂ . b₆) - (b₃ . b₆)).|| < b₄ )

proof end;

theorem Th14: :: BHSP_3:14

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₂ . b₅ = b₃ . b₅ holds
b₂ is_compared_to b₃

proof end;

theorem Th15: :: BHSP_3:15

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_Cauchy_sequence & b₂ is_compared_to b₃ holds
b₃ is_Cauchy_sequence

proof end;

theorem Th16: :: BHSP_3:16

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₂ is_compared_to b₃ holds
b₃ is convergent

proof end;

theorem Th17: :: BHSP_3:17

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃, b₄ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ & b₃ is_compared_to b₄ holds
( b₄ is convergent & lim b₄ = b₂ )

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is bounded means :Def3: :: BHSP_3:def 3
ex b₁ being Real st
( b₁ > 0 & ( for b₂ being Nat holds ||.(a₂ . b₂).|| <= b₁ ) );

end;

:: deftheorem Def3 defines bounded BHSP_3:def 3 :

theorem Th18: :: BHSP_3:18

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₃ is bounded holds
b₂ + b₃ is bounded

proof end;

theorem Th19: :: BHSP_3:19

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is bounded holds
- b₂ is bounded

proof end;

theorem Th20: :: BHSP_3:20

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₃ is bounded holds
b₂ - b₃ is bounded

proof end;

theorem Th21: :: BHSP_3:21

for b₁ being RealUnitarySpace
for b₂ being Real
for b₃ being sequence of b₁ st b₃ is bounded holds
b₂ * b₃ is bounded

proof end;

theorem Th22: :: BHSP_3:22

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is bounded

proof end;

theorem Th23: :: BHSP_3:23

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat ex b₄ being Real st
( b₄ > 0 & ( for b₅ being Nat st b₅ <= b₃ holds
||.(b₂ . b₅).|| < b₄ ) )

proof end;

theorem Th24: :: BHSP_3:24

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
b₂ is bounded

proof end;

theorem Th25: :: BHSP_3:25

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₂ is_compared_to b₃ holds
b₃ is bounded

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be increasing Seq_of_Nat;
let c₃ be sequence of c₁;
redefine func * as c₃ * c₂ -> sequence of a₁;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be sequence of c₁;
mode subsequence of c₂ -> sequence of a₁ means :Def4: :: BHSP_3:def 4
ex b₁ being increasing Seq_of_Nat st a₃ = a₂ * b₁;
existence

proof end;

end;

:: deftheorem Def4 defines subsequence BHSP_3:def 4 :

theorem Th26: :: BHSP_3:26

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being increasing Seq_of_Nat
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ . (b₃ . b₄)

proof end;

theorem Th27: :: BHSP_3:27

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds b₂ is subsequence of b₂

proof end;

theorem Th28: :: BHSP_3:28

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is subsequence of b₃ & b₃ is subsequence of b₄ holds
b₂ is subsequence of b₄

proof end;

theorem Th29: :: BHSP_3:29

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is constant & b₃ is subsequence of b₂ holds
b₃ is constant

proof end;

theorem Th30: :: BHSP_3:30

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is constant & b₃ is subsequence of b₂ holds
b₂ = b₃

proof end;

theorem Th31: :: BHSP_3:31

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₃ is subsequence of b₂ holds
b₃ is bounded

proof end;

theorem Th32: :: BHSP_3:32

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is subsequence of b₂ holds
b₃ is convergent

proof end;

theorem Th33: :: BHSP_3:33

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is subsequence of b₃ & b₃ is convergent holds
lim b₂ = lim b₃

proof end;

theorem Th34: :: BHSP_3:34

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_Cauchy_sequence & b₃ is subsequence of b₂ holds
b₃ is_Cauchy_sequence

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
let c₃ be Nat;
func c₂ ^\ c₃ -> sequence of a₁ means :Def5: :: BHSP_3:def 5
for b₁ being Nat holds a₄ . b₁ = a₂ . (b₁ + a₃);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th35: :: BHSP_3:35

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds b₂ ^\ 0 = b₂

proof end;

theorem Th36: :: BHSP_3:36

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds (b₂ ^\ b₃) ^\ b₄ = (b₂ ^\ b₄) ^\ b₃

proof end;

theorem Th37: :: BHSP_3:37

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds (b₂ ^\ b₃) ^\ b₄ = b₂ ^\ (b₃ + b₄)

proof end;

theorem Th38: :: BHSP_3:38

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat holds (b₂ + b₃) ^\ b₄ = (b₂ ^\ b₄) + (b₃ ^\ b₄)

proof end;

theorem Th39: :: BHSP_3:39

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds (- b₂) ^\ b₃ = - (b₂ ^\ b₃)

proof end;

theorem Th40: :: BHSP_3:40

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat holds (b₂ - b₃) ^\ b₄ = (b₂ ^\ b₄) - (b₃ ^\ b₄)

proof end;

theorem Th41: :: BHSP_3:41

for b₁ being RealUnitarySpace
for b₂ being Real
for b₃ being sequence of b₁
for b₄ being Nat holds (b₂ * b₃) ^\ b₄ = b₂ * (b₃ ^\ b₄)

proof end;

theorem Th42: :: BHSP_3:42

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being increasing Seq_of_Nat
for b₄ being Nat holds (b₂ * b₃) ^\ b₄ = b₂ * (b₃ ^\ b₄)

proof end;

theorem Th43: :: BHSP_3:43

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds b₂ ^\ b₃ is subsequence of b₂

proof end;

theorem Th44: :: BHSP_3:44

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is convergent holds
( b₂ ^\ b₃ is convergent & lim (b₂ ^\ b₃) = lim b₂ )

proof end;

theorem Th45: :: BHSP_3:45

canceled;

theorem Th46: :: BHSP_3:46

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st b₂ = b₃ ^\ b₄ holds
b₃ is convergent

proof end;

theorem Th47: :: BHSP_3:47

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_Cauchy_sequence & ex b₄ being Nat st b₂ = b₃ ^\ b₄ holds
b₃ is_Cauchy_sequence

proof end;

theorem Th48: :: BHSP_3:48

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is_Cauchy_sequence holds
b₂ ^\ b₃ is_Cauchy_sequence

proof end;

theorem Th49: :: BHSP_3:49

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat st b₂ is_compared_to b₃ holds
b₂ ^\ b₄ is_compared_to b₃ ^\ b₄

proof end;

theorem Th50: :: BHSP_3:50

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is bounded holds
b₂ ^\ b₃ is bounded

proof end;

theorem Th51: :: BHSP_3:51

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is constant holds
b₂ ^\ b₃ is constant

proof end;

definition

let c₁ be RealUnitarySpace;
attr a₁ is complete means :Def6: :: BHSP_3:def 6
for b₁ being sequence of a₁ st b₁ is_Cauchy_sequence holds
b₁ is convergent;

end;

:: deftheorem Def6 defines complete BHSP_3:def 6 :

notation

let c₁ be RealUnitarySpace;
synonym c₁ is_complete_space for complete c₁;

end;

theorem Th52: :: BHSP_3:52

canceled;

theorem Th53: :: BHSP_3:53

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₁ is_complete_space & b₂ is_Cauchy_sequence holds
b₂ is bounded

proof end;

definition

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

end;

:: deftheorem Def7 defines Hilbert BHSP_3:def 7 :

notation

let c₁ be RealUnitarySpace;
synonym c₁ is_Hilbert_space for Hilbert c₁;

end;