:: CLVECT_3 semantic presentation

deffunc H₁( ComplexUnitarySpace) -> Element of the carrier of a₁ = 0. a₁;

scheme :: CLVECT_3:sch 1
s1{ F₁() -> ComplexUnitarySpace, F₂() -> Point of F₁(), F₃( Nat, Point of F₁()) -> Point of F₁() } :

ex b₁ being Function of NAT ,the carrier of F₁() st
( b₁ . 0 = F₂() & ( for b₂ being Element of NAT
for b₃ being Point of F₁() st b₃ = b₁ . b₂ holds
b₁ . (b₂ + 1) = F₃(b₂,b₃) ) )

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
func Partial_Sums c₂ -> sequence of a₁ means :Def1: :: CLVECT_3:def 1
( a₃ . 0 = a₂ . 0 & ( for b₁ being Nat holds a₃ . (b₁ + 1) = (a₃ . b₁) + (a₂ . (b₁ + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Sums CLVECT_3:def 1 :

theorem Th1: :: CLVECT_3:1

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ holds (Partial_Sums b₂) + (Partial_Sums b₃) = Partial_Sums (b₂ + b₃)

proof end;

theorem Th2: :: CLVECT_3:2

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ holds (Partial_Sums b₂) - (Partial_Sums b₃) = Partial_Sums (b₂ - b₃)

proof end;

theorem Th3: :: CLVECT_3:3

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex holds Partial_Sums (b₃ * b₂) = b₃ * (Partial_Sums b₂)

proof end;

theorem Th4: :: CLVECT_3:4

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds Partial_Sums (- b₂) = - (Partial_Sums b₂)

proof end;

theorem Th5: :: CLVECT_3:5

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄, b₅ being Complex holds (b₄ * (Partial_Sums b₂)) + (b₅ * (Partial_Sums b₃)) = Partial_Sums ((b₄ * b₂) + (b₅ * b₃))

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is summable means :Def2: :: CLVECT_3:def 2
Partial_Sums a₂ is convergent;
func Sum c₂ -> Point of a₁ equals :: CLVECT_3:def 3
lim (Partial_Sums a₂);
correctness ;

end;

:: deftheorem Def2 defines summable CLVECT_3:def 2 :

:: deftheorem Def3 defines Sum CLVECT_3:def 3 :

theorem Th6: :: CLVECT_3:6

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is summable & b₃ is summable holds
( b₂ + b₃ is summable & Sum (b₂ + b₃) = (Sum b₂) + (Sum b₃) )

proof end;

theorem Th7: :: CLVECT_3:7

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is summable & b₃ is summable holds
( b₂ - b₃ is summable & Sum (b₂ - b₃) = (Sum b₂) - (Sum b₃) )

proof end;

theorem Th8: :: CLVECT_3:8

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex st b₂ is summable holds
( b₃ * b₂ is summable & Sum (b₃ * b₂) = b₃ * (Sum b₂) )

proof end;

theorem Th9: :: CLVECT_3:9

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is summable holds
( b₂ is convergent & lim b₂ = 0. b₁ )

proof end;

theorem Th10: :: CLVECT_3:10

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₁ is Hilbert holds
( b₂ is summable 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
||.(((Partial_Sums b₂) . b₅) - ((Partial_Sums b₂) . b₆)).|| < b₃ )

proof end;

theorem Th11: :: CLVECT_3:11

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is summable holds
Partial_Sums b₂ is bounded

proof end;

theorem Th12: :: CLVECT_3:12

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ . 0 ) holds
Partial_Sums (b₃ ^\ 1) = ((Partial_Sums b₃) ^\ 1) - b₂

proof end;

theorem Th13: :: CLVECT_3:13

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is summable holds
for b₃ being Nat holds b₂ ^\ b₃ is summable

proof end;

theorem Th14: :: CLVECT_3:14

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st ex b₃ being Nat st b₂ ^\ b₃ is summable holds
b₂ is summable

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
let c₃ be Nat;
func Sum c₂,c₃ -> Point of a₁ equals :: CLVECT_3:def 4
(Partial_Sums a₂) . a₃;
correctness ;

end;

:: deftheorem Def4 defines Sum CLVECT_3:def 4 :

theorem Th15: :: CLVECT_3:15

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds Sum b₂,0 = b₂ . 0 by Def1;

theorem Th16: :: CLVECT_3:16

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds Sum b₂,1 = (Sum b₂,0) + (b₂ . 1)

proof end;

theorem Th17: :: CLVECT_3:17

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds Sum b₂,1 = (b₂ . 0) + (b₂ . 1)

proof end;

theorem Th18: :: CLVECT_3:18

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds Sum b₂,(b₃ + 1) = (Sum b₂,b₃) + (b₂ . (b₃ + 1)) by Def1;

theorem Th19: :: CLVECT_3:19

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds b₂ . (b₃ + 1) = (Sum b₂,(b₃ + 1)) - (Sum b₂,b₃)

proof end;

theorem Th20: :: CLVECT_3:20

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ . 1 = (Sum b₂,1) - (Sum b₂,0)

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
let c₃, c₄ be Nat;
func Sum c₂,c₃,c₄ -> Point of a₁ equals :: CLVECT_3:def 5
(Sum a₂,a₃) - (Sum a₂,a₄);
correctness ;

end;

:: deftheorem Def5 defines Sum CLVECT_3:def 5 :

theorem Th21: :: CLVECT_3:21

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds Sum b₂,1,0 = b₂ . 1

proof end;

theorem Th22: :: CLVECT_3:22

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds Sum b₂,(b₃ + 1),b₃ = b₂ . (b₃ + 1) by Th19;

theorem Th23: :: CLVECT_3:23

proof end;

theorem Th24: :: CLVECT_3:24

proof end;

definition

let c₁ be Complex_Sequence;
let c₂ be Nat;
func Sum c₁,c₂ -> Complex equals :: CLVECT_3:def 6
(Partial_Sums a₁) . a₂;
correctness ;

end;

:: deftheorem Def6 defines Sum CLVECT_3:def 6 :

definition

let c₁ be Complex_Sequence;
let c₂, c₃ be Nat;
func Sum c₁,c₂,c₃ -> Complex equals :: CLVECT_3:def 7
(Sum a₁,a₂) - (Sum a₁,a₃);
correctness ;

end;

:: deftheorem Def7 defines Sum CLVECT_3:def 7 :

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is absolutely_summable means :Def8: :: CLVECT_3:def 8
||.a₂.|| is summable;

end;

:: deftheorem Def8 defines absolutely_summable CLVECT_3:def 8 :

theorem Th25: :: CLVECT_3:25

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is absolutely_summable & b₃ is absolutely_summable holds
b₂ + b₃ is absolutely_summable

proof end;

theorem Th26: :: CLVECT_3:26

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex st b₂ is absolutely_summable holds
b₃ * b₂ is absolutely_summable

proof end;

theorem Th27: :: CLVECT_3:27

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds ||.b₂.|| . b₄ <= b₃ . b₄ ) & b₃ is summable holds
b₂ is absolutely_summable

proof end;

theorem Th28: :: CLVECT_3:28

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds
( b₂ . b₄ <> 0. b₁ & b₃ . b₄ = ||.(b₂ . (b₄ + 1)).|| / ||.(b₂ . b₄).|| ) ) & b₃ is convergent & lim b₃ < 1 holds
b₂ is absolutely_summable

proof end;

theorem Th29: :: CLVECT_3:29

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

proof end;

theorem Th30: :: CLVECT_3:30

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st ( for b₃ being Nat holds b₂ . b₃ <> 0. b₁ ) & ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
||.(b₂ . (b₄ + 1)).|| / ||.(b₂ . b₄).|| >= 1 holds
not b₂ is summable

proof end;

theorem Th31: :: CLVECT_3:31

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₂ . b₄ <> 0. b₁ ) & ( for b₄ being Nat holds b₃ . b₄ = ||.(b₂ . (b₄ + 1)).|| / ||.(b₂ . b₄).|| ) & b₃ is convergent & lim b₃ > 1 holds
not b₂ is summable

proof end;

theorem Th32: :: CLVECT_3:32

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = b₄ -root ||.(b₂ . b₄).|| ) & b₃ is convergent & lim b₃ < 1 holds
b₂ is absolutely_summable

proof end;

theorem Th33: :: CLVECT_3:33

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = b₄ -root (||.b₂.|| . b₄) ) & ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₃ . b₅ >= 1 holds
not b₂ is summable

proof end;

theorem Th34: :: CLVECT_3:34

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = b₄ -root (||.b₂.|| . b₄) ) & b₃ is convergent & lim b₃ > 1 holds
not b₂ is summable

proof end;

theorem Th35: :: CLVECT_3:35

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds Partial_Sums ||.b₂.|| is non-decreasing

proof end;

theorem Th36: :: CLVECT_3:36

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds (Partial_Sums ||.b₂.||) . b₃ >= 0

proof end;

theorem Th37: :: CLVECT_3:37

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds ||.((Partial_Sums b₂) . b₃).|| <= (Partial_Sums ||.b₂.||) . b₃

proof end;

theorem Th38: :: CLVECT_3:38

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds ||.(Sum b₂,b₃).|| <= Sum ||.b₂.||,b₃

proof end;

theorem Th39: :: CLVECT_3:39

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds ||.(((Partial_Sums b₂) . b₄) - ((Partial_Sums b₂) . b₃)).|| <= abs (((Partial_Sums ||.b₂.||) . b₄) - ((Partial_Sums ||.b₂.||) . b₃))

proof end;

theorem Th40: :: CLVECT_3:40

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds ||.((Sum b₂,b₄) - (Sum b₂,b₃)).|| <= abs ((Sum ||.b₂.||,b₄) - (Sum ||.b₂.||,b₃))

proof end;

theorem Th41: :: CLVECT_3:41

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds ||.(Sum b₂,b₄,b₃).|| <= abs (Sum ||.b₂.||,b₄,b₃)

proof end;

theorem Th42: :: CLVECT_3:42

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₁ is Hilbert & b₂ is absolutely_summable holds
b₂ is summable

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
let c₃ be Complex_Sequence;
func c₃ * c₂ -> sequence of a₁ means :Def9: :: CLVECT_3:def 9
for b₁ being Nat holds a₄ . b₁ = (a₃ . b₁) * (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines * CLVECT_3:def 9 :

theorem Th43: :: CLVECT_3:43

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Complex_Sequence holds b₄ * (b₂ + b₃) = (b₄ * b₂) + (b₄ * b₃)

proof end;

theorem Th44: :: CLVECT_3:44

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Complex_Sequence holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂)

proof end;

theorem Th45: :: CLVECT_3:45

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Complex_Sequence holds (b₃ (#) b₄) * b₂ = b₃ * (b₄ * b₂)

proof end;

theorem Th46: :: CLVECT_3:46

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence
for b₄ being Complex holds (b₄ (#) b₃) * b₂ = b₄ * (b₃ * b₂)

proof end;

theorem Th47: :: CLVECT_3:47

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence holds b₃ * (- b₂) = (- b₃) * b₂

proof end;

Lemma25: for b₁ being Complex_Sequence st b₁ is convergent holds
b₁ is bounded

proof end;

theorem Th48: :: CLVECT_3:48

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence st b₃ is convergent & b₂ is convergent holds
b₃ * b₂ is convergent

proof end;

theorem Th49: :: CLVECT_3:49

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence st b₃ is bounded & b₂ is bounded holds
b₃ * b₂ is bounded

proof end;

theorem Th50: :: CLVECT_3:50

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence st b₃ is convergent & b₂ is convergent holds
( b₃ * b₂ is convergent & lim (b₃ * b₂) = (lim b₃) * (lim b₂) )

proof end;

definition

let c₁ be Complex_Sequence;
attr a₁ is Cauchy means :Def10: :: CLVECT_3:def 10
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃, b₄ being Nat st b₃ >= b₂ & b₄ >= b₂ holds
|.((a₁ . b₃) - (a₁ . b₄)).| < b₁;

end;

:: deftheorem Def10 defines Cauchy CLVECT_3:def 10 :

notation

let c₁ be Complex_Sequence;
synonym c₁ is_Cauchy_sequence for Cauchy c₁;

end;

theorem Th51: :: CLVECT_3:51

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence st b₁ is Hilbert & b₂ is Cauchy & b₃ is Cauchy holds
b₃ * b₂ is Cauchy

proof end;

theorem Th52: :: CLVECT_3:52

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence
for b₄ being Nat holds (Partial_Sums ((b₃ - (b₃ ^\ 1)) * (Partial_Sums b₂))) . b₄ = ((Partial_Sums (b₃ * b₂)) . (b₄ + 1)) - ((b₃ * (Partial_Sums b₂)) . (b₄ + 1))

proof end;

theorem Th53: :: CLVECT_3:53

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence
for b₄ being Nat holds (Partial_Sums (b₃ * b₂)) . (b₄ + 1) = ((b₃ * (Partial_Sums b₂)) . (b₄ + 1)) - ((Partial_Sums (((b₃ ^\ 1) - b₃) * (Partial_Sums b₂))) . b₄)

proof end;

theorem Th54: :: CLVECT_3:54

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Complex_Sequence
for b₄ being Nat holds Sum (b₃ * b₂),(b₄ + 1) = ((b₃ * (Partial_Sums b₂)) . (b₄ + 1)) - (Sum (((b₃ ^\ 1) - b₃) * (Partial_Sums b₂)),b₄) by Th53;