RUSUB_6: On the Formalization of {G}ram-Schmidt Process for Orthonormalizing a Set of Vectors

definition

let V be non empty RLSStruct ;
let r be FinSequence of REAL ;
let x be FinSequence of V;

func r (*) x -> FinSequence of V means :DefR: :: RUSUB_6:def 1
( len it = len x & ( for i being Nat st 1 <= i & i <= len x holds
it . i = (r /. i) * (x /. i) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem DefR defines (*) RUSUB_6:def 1 :

theorem Th1: :: RUSUB_6:1

for V being RealLinearSpace
for A being Subset of V
for x being FinSequence of V
for r being FinSequence of REAL st rng x c= A & len x = len r holds
Sum (r (*) x) in Lin A

proof end;

theorem Th2: :: RUSUB_6:2

for V being RealLinearSpace
for A, B being Subset of V st A c= the carrier of (Lin B) holds
Lin A is Subspace of Lin B

proof end;

theorem Th3: :: RUSUB_6:3

for V being RealLinearSpace
for A, B being Subset of V st A c= the carrier of (Lin B) & B c= the carrier of (Lin A) holds
Lin A = Lin B

proof end;

definition

let V be non empty UNITSTR ;
let u be Point of V;
let x be FinSequence of V;

func u .|. x -> FinSequence of REAL means :DefSK: :: RUSUB_6:def 2
( len it = len x & ( for i being Nat st 1 <= i & i <= len x holds
it . i = u .|. (x /. i) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem DefSK defines .|. RUSUB_6:def 2 :

theorem Added: :: RUSUB_6:4

for V being non empty UNITSTR
for u being Point of V
for x being FinSequence of V
for i being Nat st 1 <= i & i <= len x holds
((u .|. x) (*) x) . i = (u .|. (x /. i)) * (x /. i)

proof end;

theorem Th4: :: RUSUB_6:5

for V being RealUnitarySpace
for u being Point of V
for x being FinSequence of V holds u .|. (Sum x) = Sum (u .|. x)

proof end;

theorem Th5: :: RUSUB_6:6

for V being RealUnitarySpace
for u being Point of V
for n being Nat
for x being FinSequence of V st 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n)

proof end;

theorem Th6: :: RUSUB_6:7

for H being RealUnitarySpace ex F being Function of [: the carrier of H,( the carrier of H *):],( the carrier of H *) st
for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F . (x,e) & Fe = (x .|. e) (*) e )

proof end;

theorem Th8: :: RUSUB_6:8

for H being RealUnitarySpace
for G being OrthonormalFamily of H holds G is linearly-independent

proof end;

definition

let H be RealUnitarySpace;

func ProjSeq H -> Function of [: the carrier of H,( the carrier of H *):],( the carrier of H *) means :Def1: :: RUSUB_6:def 3
for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = it . (x,e) & Fe = (x .|. e) (*) e );

existence by Th6;
uniqueness

proof end;

end;

:: deftheorem Def1 defines ProjSeq RUSUB_6:def 3 :

theorem Th7: :: RUSUB_6:9

for H being RealUnitarySpace
for x being FinSequence of H st x is one-to-one & rng x is linearly-independent & 1 <= len x holds
ex e being FinSequence of H st
( len x = len e & rng e is OrthonormalFamily of H & e is one-to-one & Lin (rng x) = Lin (rng e) & e /. 1 = (1 / ||.(x /. 1).||) * (x /. 1) & ( for k being Nat st 1 <= k & k < len x holds
ex g being FinSequence of H st
( g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (e | k) is OrthonormalFamily of H & e | k is one-to-one & Lin (rng (x | k)) = Lin (rng (e | k)) ) ) )

proof end;

definition

let H be RealUnitarySpace;
let x be FinSequence of H;
assume A1: ( x is one-to-one & rng x is linearly-independent & 1 <= len x ) ;

func GramSchmidt x -> FinSequence of H means :Def2: :: RUSUB_6:def 4
( len x = len it & rng it is OrthonormalFamily of H & it is one-to-one & Lin (rng x) = Lin (rng it) & it /. 1 = (1 / ||.(x /. 1).||) * (x /. 1) & ( for k being Nat st 1 <= k & k < len x holds
ex g being FinSequence of H st
( g = (ProjSeq H) . [(x /. (1 + k)),(it | k)] & it /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (it | k) is OrthonormalFamily of H & it | k is one-to-one & Lin (rng (x | k)) = Lin (rng (it | k)) ) ) );

existence by Th7, A1;
uniqueness

proof end;

end;

:: deftheorem Def2 defines GramSchmidt RUSUB_6:def 4 :

theorem :: RUSUB_6:10

for H being RealUnitarySpace
for x being FinSequence of H st x is one-to-one & rng x is linearly-independent & 1 <= len x holds
rng (GramSchmidt x) is linearly-independent

proof end;