:: On the Formalization of {G}ram-Schmidt Process for Orthonormalizing a
:: Set of Vectors
:: by Hiroyuki Okazaki
::
:: Received March 31, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RUSUB_6, NUMBERS, BHSP_1, PRE_TOPC, ARYTM_1, ARYTM_3, XXREAL_0,
CARD_1, SUBSET_1, RELAT_1, XBOOLE_0, TARSKI, BHSP_5, STRUCT_0, FUNCT_1,
ZFMISC_1, NAT_1, PROB_2, FINSEQ_1, SQUARE_1, NORMSP_1, SUPINF_2,
RLVECT_3, RLVECT_1, RLVECT_2, RLSUB_1, CARD_3, VALUED_1, PARTFUN1,
ORDINAL4, FINSEQ_2, FUNCT_7, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
ORDINAL1, PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, XCMPLX_0, XXREAL_0,
SQUARE_1, FINSEQ_1, FINSEQ_2, PRE_POLY, MATRIX_0, STRUCT_0, PRE_TOPC,
RLVECT_1, RLSUB_1, RLVECT_2, RLVECT_3, RVSUM_1, BHSP_1, BHSP_5;
constructors SQUARE_1, BHSP_5, RELSET_1, RLVECT_2, RLVECT_3, REALSET1,
RVSUM_1, MATRIX_3;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, RLVECT_1, NUMBERS,
XREAL_0, STRUCT_0, SQUARE_1, NAT_1, RELAT_1, FINSEQ_1, FINSEQ_2, INT_1,
FUNCOP_1, CARD_1, BHSP_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, FINSEQ_1;
equalities FINSEQ_1, FINSEQ_2, BHSP_1, BINOP_1, XREAL_0;
expansions FUNCT_1, TARSKI, BINOP_1;
theorems SQUARE_1, FUNCT_1, NAT_1, RLVECT_1, BHSP_1, BHSP_5, XCMPLX_1,
XREAL_1, XXREAL_0, RLVECT_2, RLVECT_3, TARSKI, FINSEQ_1, FINSEQ_3,
RLSUB_1, XBOOLE_0, STRUCT_0, PARTFUN1, RELAT_1, INT_1, RLVECT_4,
RLVECT_5, FINSEQ_5, RVSUM_1;
schemes NAT_1, RECDEF_1, BINOP_1, FINSEQ_1, FINSEQ_2;
begin :: Preliminaries
Lm1: for X being RealUnitarySpace,
x being Point of X holds ||.x.|| ^2 = x .|. x
proof
let X be RealUnitarySpace, x be Point of X;
0 <= x .|. x by BHSP_1:def 2;
hence ||.x.|| ^2 = x .|. x by SQUARE_1:def 2;
end;
definition
let V be non empty RLSStruct,
r be FinSequence of REAL,
x be FinSequence of V;
func r (*) x -> FinSequence of V means :DefR:
len it = len x &
for i being Nat st 1 <= i & i <= len x holds it.i = (r/.i) * (x/.i);
existence
proof
deffunc F(Nat) = (r/.$1)*(x/.$1);
consider z being FinSequence of V such that
A1: len z = len x &
for j being Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
thus thesis by A1,FINSEQ_3:25;
end;
uniqueness
proof
let f,g be FinSequence of V such that
A1: len f = len x and
A2: for i being Nat st 1 <= i & i <= len x holds f.i = (r/.i) * (x/.i) and
A3: len g = len x and
A4: for i being Nat st 1 <= i & i <= len x holds g.i = (r/.i) * (x/.i);
thus len f = len g by A1,A3;
let i be Nat such that
A5: 1 <= i & i <= len f;
thus f.i = (r/.i) * (x/.i) by A1,A2,A5
.= g.i by A1,A4,A5;
end;
end;
theorem Th1:
for V being RealLinearSpace,
A being Subset of V,
x be FinSequence of V,
r be FinSequence of REAL
st rng x c= A & len x = len r
holds Sum (r(*)x) in Lin A
proof
let V be RealLinearSpace,
A be Subset of V;
defpred P[Nat] means
for x be FinSequence of V,
r be FinSequence of REAL
st $1 = len x & rng x c= A & len x = len r
holds Sum (r(*)x) in Lin A;
A1:P[0]
proof
let x be FinSequence of V,
r be FinSequence of REAL;
assume A2: 0 = len x & rng x c= A & len x = len r;
set y = r(*)x;
len y = len x by DefR;
then y = <*> (the carrier of V) by A2; then
Sum y = 0.V by RLVECT_1:43; then
Sum y = 0.(Lin A) by RLSUB_1:11;
hence Sum y in Lin A by STRUCT_0:def 5;
end;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let x be FinSequence of V,
r be FinSequence of REAL;
assume
A5: k+1 = len x & rng x c= A & len x = len r;
set y = r(*)x;
set x1=x | k;
set y1=y | k;
set r1=r | k;
A6:k <= k+1 by NAT_1:11;
AA: len y = len x by DefR; then
A7: len x1 = k & len y1 = k & len r1 = k by A5,FINSEQ_1:59,NAT_1:11;
rng x1 c= rng x by RELAT_1:70; then
A8: k= len x1 & rng x1 c= A & len x1=len y1
& len x1 = len r1 by A7,A5;
D1:for i be Nat st 1<=i & i <= len x1
holds y1.i = r1/.i*x1/.i
proof
let i be Nat;
assume A10: 1<=i & i <= len x1; then
A11: i <= len x by A6,A7,A5,XXREAL_0:2; then
A13: i in dom x by A10,FINSEQ_3:25;
A14: i in dom r by A10,A11,A5,FINSEQ_3:25;
A16: i in dom x1 by A10,FINSEQ_3:25;
A19: y1.i =y.i by FUNCT_1:49,A10,FINSEQ_1:1,A7;
i in Seg k by A10,A7; then
i in dom r1 by FINSEQ_1:def 3,A7; then
A20: r1/.i = r1.i by PARTFUN1:def 6
.= r.i by FUNCT_1:49,A10,FINSEQ_1:1,A7
.= r/.i by A14,PARTFUN1:def 6;
x1/.i = x1.i by A16,PARTFUN1:def 6
.= x.i by FUNCT_1:49,A10,FINSEQ_1:1,A7
.= x/.i by A13,PARTFUN1:def 6;
hence thesis by A10,A19,A20,A11,DefR;
end;
y1 = r1(*)x1 by A7,D1,DefR; then
A22: Sum y1 in Lin A by A4,A8;
1 <= k+1 by NAT_1:11; then
A24: y.(len y) = r/.(k+1)*x/.(k+1) by A5,AA,DefR;
dom y1 = Seg k by A7,FINSEQ_1:def 3; then
A26: Sum y = Sum y1 + r/.(k+1)*x/.(k+1) by RLVECT_1:38,A7,A5,DefR,A24;
A27:dom x = Seg (k+1) by A5,FINSEQ_1:def 3; then
A29:x/.(k+1) = x.(k+1) by PARTFUN1:def 6,FINSEQ_1:4;
k+1 in Seg (k+1) by FINSEQ_1:4; then
x/.(k+1) in rng x by A29,A27,FUNCT_1:def 3; then
r/.(k+1)*x/.(k+1) in Lin A by RLSUB_1:21,RLVECT_3:15,A5;
hence Sum y in Lin A by A26,A22,RLSUB_1:20;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th2:
for V being RealLinearSpace,
A,B being Subset of V
st A c= the carrier of Lin B holds
Lin A is Subspace of Lin B
proof
let V be RealLinearSpace,
A,B be Subset of V;
assume A1: A c= the carrier of Lin B;
reconsider D = the carrier of Lin B as Subset of V by RLSUB_1:def 2;
Lin A is Subspace of Lin D by RLVECT_3:20,A1;
hence thesis by RLVECT_3:18;
end;
theorem Th3:
for V being RealLinearSpace,
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
let V be RealLinearSpace,
A,B be Subset of V;
assume that
A1: A c= the carrier of Lin B and
A2: B c= the carrier of Lin A;
A3: Lin A is Subspace of Lin B by A1,Th2;
Lin B is Subspace of Lin A by A2,Th2;
hence thesis by RLSUB_1:26,A3;
end;
definition
let V be non empty UNITSTR,
u be Point of V,
x be FinSequence of V;
func u .|. x -> FinSequence of REAL means :DefSK:
len it = len x &
for i being Nat st 1 <= i & i <= len x holds it.i = u .|. (x/.i);
existence
proof
deffunc F(Nat) = In(u .|. (x/.$1),REAL);
consider z being FinSequence of REAL such that
A1: len z = len x and
A2: for j being Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
thus len z = len x by A1;
let i be Nat;
assume 1 <= i & i <= len x;
then z.i = F(i) by A1,A2,FINSEQ_3:25;
hence thesis;
end;
uniqueness
proof
let f,g be FinSequence of REAL such that
A1: len f = len x and
A2: for i being Nat st 1 <= i & i <= len x holds f.i = u .|. (x/.i) and
A3: len g = len x and
A4: for i being Nat st 1 <= i & i <= len x holds g.i = u .|. (x/.i);
thus len f = len g by A1,A3;
let i be Nat such that
A5: 1 <= i & i <= len f;
thus f.i = u .|. (x/.i) by A1,A2,A5
.= g.i by A1,A4,A5;
end;
end;
theorem Added:
for V being non empty UNITSTR,
u being Point of V,
x being FinSequence of V,
i being Nat st 1 <= i <= len x
holds ((u.|.x)(*)x).i = (u .|. (x/.i)) * (x/.i)
proof
let V be non empty UNITSTR,
u be Point of V,
x be FinSequence of V,
i be Nat such that
A1: 1 <= i <= len x;
len (u.|.x) = len x by DefSK; then
i in dom (u.|.x) by A1,FINSEQ_3:25; then
A2: (u.|.x).i = (u.|.x)/.i by PARTFUN1:def 6;
thus ((u.|.x)(*)x).i = (u.|.x)/.i * (x/.i) by A1,DefR
.= (u .|. (x/.i)) * (x/.i) by A1,A2,DefSK;
end;
theorem Th4:
for V being RealUnitarySpace,
u be Point of V,
x be FinSequence of V
holds u .|. (Sum x) = Sum (u .|. x)
proof
let V be RealUnitarySpace,
u be Point of V,
x be FinSequence of V;
defpred P[Nat] means
for x be FinSequence of V st $1 = len x holds u .|. (Sum x) = Sum (u .|. x);
A1:P[0]
proof
let x be FinSequence of V;
assume A2:0=len x; then
x = <*> the carrier of V; then
A3: Sum x =0.V by RLVECT_1:43;
set r = u .|. x;
len r = len x by DefSK;
then r = <*> REAL by A2;
hence u .|. (Sum x) = Sum r by A3,BHSP_1:15,RVSUM_1:72;
end;
A4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
let x be FinSequence of V;
set r = u .|. x;
set x1=x | k;
set r1=r | k;
assume
A6: k+1=len x; then
A7: 1 <= k+1 & k+1 <= len x by NAT_1:11;
A8: k <= k+1 by NAT_1:11;
B1: len r = len x by DefSK; then
A9: len x1 = k & len r1 = k by A6,FINSEQ_1:59,NAT_1:11;
for i be Nat st 1<=i & i <= len x1 holds r1.i = u .|. (x1/.i)
proof
let i be Nat;
assume A10: 1<=i & i <= len x1; then
A11: i <= len x by A8,A9,A6,XXREAL_0:2; then
A13: i in dom x by A10,FINSEQ_3:25;
A20: r1.i = r.i by FUNCT_1:49,A9,A10,FINSEQ_1:1;
i in dom x1 by A10,FINSEQ_3:25; then
x1/.i = x1.i by PARTFUN1:def 6
.= x.i by FUNCT_1:49,A9,A10,FINSEQ_1:1
.= x/.i by A13,PARTFUN1:def 6;
hence thesis by A10,A20,A11,DefSK;
end; then
A22b: r1 = u .|. x1 by A9,DefSK;
A23a:r= r1 ^ <*(r . (k + 1))*> by B1,FINSEQ_3:55,A6
.=r1 ^ <*u .|. (x/.(k+1)) *> by A7,DefSK;
A24: len x = len x1 + 1 by A6,FINSEQ_1:59,NAT_1:11;
A25: dom x1 = Seg k by A9,FINSEQ_1:def 3;
k+1 in Seg (k+1) by FINSEQ_1:4; then
k+1 in dom x by A6,FINSEQ_1:def 3; then
x/.(k+1) = x.(len x) by A6,PARTFUN1:def 6;
hence u .|. (Sum x)
= u .|. (Sum x1 + x/.(k+1)) by A24,A25,RLVECT_1:38
.= u .|. (Sum x1) + u .|.(x/.(k+1)) by BHSP_1:2
.= Sum r1 + u .|.(x/.(k+1)) by A22b,A5,A9
.= Sum r by A23a,RVSUM_1:74;
end;
B3: len (u .|. x) = len x by DefSK;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
hence thesis by B3;
end;
theorem Th5:
for V being RealUnitarySpace,
u be Point of V,
n be Nat,
x be FinSequence of V
st 1 <= n & n <= len x &
for i be Nat st 1 <= i & i <= len x & n <> i
holds u .|. (x/.i) = 0
holds u .|. (Sum x) = u .|. (x/.n)
proof
let V be RealUnitarySpace,
u be Point of V,
n be Nat;
defpred P[Nat] means
for x be FinSequence of V
st $1 = len x & 1<=n & n <= len x &
for i be Nat st 1<=i & i <= len x & n <> i
holds u .|. (x/.i) = 0
holds u .|. (Sum x) = u .|. (x/.n);
A1:P[0];
A2:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A3: P[k];
let x be FinSequence of V;
assume A4: k+1 = len x & 1<=n & n <= len x &
for i be Nat st 1<=i & i <= len x & n <> i
holds u .|. (x/.i) = 0; then
A5: n in dom x by FINSEQ_3:25;
defpred P1[Nat,object] means $2 = u .|. (x/.$1);
A6: for k being Nat st k in Seg len x holds
ex v being Element of REAL st P1[k,v];
consider r being FinSequence of REAL such that
A7: dom r = Seg len x &
for k being Nat st k in Seg len x holds
P1[k,r . k] from FINSEQ_1:sch 5(A6);
A8: len x = len r
& for i be Nat st 1<=i & i <= len x
holds r.i = u .|. (x/.i)
by A7,FINSEQ_1:def 3,FINSEQ_1:1;
set x1=x | k;
set r1=r | k;
A11: len x1 = k & len r1 = k by A4,A8,FINSEQ_1:59,NAT_1:11;
A24: dom r1 = Seg len r1 by FINSEQ_1:def 3;
per cases;
suppose A25:n = k+1;
for i be object st i in dom r1 holds r1.i = 0
proof
let t be object;
assume A27: t in dom r1; then
reconsider i=t as Nat;
A28: 1<=i & i <= len r1 by A27,A24,FINSEQ_1:1;
A29: i <= k by A11,A27,A24,FINSEQ_1:1; then
A31: i <= len x by A4,NAT_1:13;
i <> n by NAT_1:13,A25,A29; then
u .|. (x/.i) = 0 by A4,A28,A31; then
r.i = 0 by A28,A31, A7,FINSEQ_1:1;
hence r1.t = 0 by A27,A24,FUNCT_1:49,A11;
end; then
r1 = (len r1 |-> 0) by FINSEQ_1:def 3; then
A32: Sum r1 = 0 by RVSUM_1:81;
r = r1 ^ <*(r . (k + 1))*> by FINSEQ_3:55,A8,A4
.= r1 ^ <*u .|. (x/.n) *> by A25,A4,A7,FINSEQ_1:1; then
W1: Sum r = 0 + u .|. (x/.n) by A32,RVSUM_1:74;
u .|. (Sum x) = Sum (u .|. x) by Th4;
hence u .|. (Sum x) = u .|. (x/.n) by A8,W1,DefSK;
end;
suppose A33: n <> k+1;
A34: k= len x1 & 1<=n & n <= len x1 &
for i be Nat st 1<=i & i <= len x1 & n <> i
holds u .|. (x1/.i) = 0
proof
n < k + 1 by A33,A4,XXREAL_0:1;
hence k= len x1 & 1<=n & n <= len x1 by NAT_1:13,A4,A11;
let i be Nat;
assume A35: 1<=i & i <=len x1 & n <> i;
k <= k+1 by NAT_1:11; then
A36:i <= len x by A4,A11,A35,XXREAL_0:2;
A38: i in Seg k by A35,A11;
A39: i in dom x1 by A35,FINSEQ_3:25;
i in dom x by A35,A36,FINSEQ_3:25; then
x/.i = x.i by PARTFUN1:def 6
.= x1.i by FUNCT_1:49,A38
.= x1/.i by PARTFUN1:def 6,A39;
hence thesis by A4,A35,A36;
end; then
A40: n in Seg k; then
n in dom x1 by A11,FINSEQ_1:def 3; then
A41:x1/.n =x1.n by PARTFUN1:def 6
.=x.n by FUNCT_1:49,A40
.=x/.n by PARTFUN1:def 6,A5;
A43: len x = len x1 + 1 by A4,FINSEQ_1:59,NAT_1:11;
A44: dom x1 = Seg k by A11,FINSEQ_1:def 3;
A0: 1 <= k+1 by NAT_1:11; then
k+1 in dom x by A4,FINSEQ_3:25; then
A45a:x/.(k+1) = x.(len x) by A4,PARTFUN1:def 6;
A46: u .|. (x/.(k+1)) = 0 by A33,A4,A0;
thus u .|. (Sum x)
= u .|. (Sum x1 + x/.(k+1)) by A45a,A43,A44,RLVECT_1:38
.= u .|. (Sum x1) + u .|.(x/.(k+1)) by BHSP_1:2
.= u .|. (x/.n) by A46,A41,A3,A34;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th6:
for H being RealUnitarySpace holds
ex F be Function of [:the carrier of H,(the carrier of H)* :],
(the carrier of H)*
st for x be Point of H, e be FinSequence of H
ex Fe be FinSequence of H
st Fe = F.(x,e) & Fe = (x.|.e) (*) e
proof
let H be RealUnitarySpace;
set CH = the carrier of H;
defpred P1[ object, object, object ] means
ex x be Point of H,e be FinSequence of CH
st $1=x & $2=e
&
ex Fe be FinSequence of CH
st Fe = $3 & Fe = (x.|.e) (*) e;
A1: for x, y being object st x in CH & y in CH* holds
ex z being object st z in CH* & P1[x,y,z]
proof
let x0, y0 be object;
assume A2: x0 in CH & y0 in CH*; then
reconsider xn=x0 as Point of H;
reconsider e=y0 as FinSequence of CH by A2,FINSEQ_1:def 11;
defpred P2[ object, object ] means
$2= (xn.|. (e/.$1))*(e/.$1);
A3: for k being Nat st k in Seg len e holds
ex z being Element of CH st P2[k,z];
consider Fe being FinSequence of CH such that
A4:dom Fe = Seg len e
& for k being Nat st k in Seg len e holds
P2[k,Fe . k] from FINSEQ_1:sch 5(A3);
A5: len Fe = len e by A4,FINSEQ_1:def 3;
A6: for i be Nat st 1 <= i & i <= len Fe holds
Fe.i = (xn.|. (e/.i))*(e/.i)
proof
let i be Nat;
assume 1 <= i & i <= len Fe; then
i in Seg len Fe;
hence thesis by A4,A5;
end;
take Fe;
thus Fe in CH* by FINSEQ_1:def 11;
Fe = (xn.|.e)(*)(e)
proof
thus len Fe = len ((xn.|.e)(*)(e)) by A5,DefR;
let i be Nat such that
E1: 1 <= i & i <= len Fe;
len (xn.|.e) = len e by DefSK;
then i in dom (xn.|.e) by A5,E1,FINSEQ_3:25; then
E2: (xn.|.e)/.i = (xn.|.e).i by PARTFUN1:def 6;
thus Fe.i = (xn.|. (e/.i))*(e/.i) by A6,E1
.= (xn.|.e)/.i * (e/.i) by E1,E2,A5,DefSK
.= ((xn.|.e)(*)e).i by E1,A5,DefR;
end;
hence thesis;
end;
consider F being Function of [:CH,CH*:],CH* such that
A7:for z, y being object st z in CH & y in CH*
holds
P1[z,y,F . (z,y)] from BINOP_1:sch 1(A1);
take F;
let z be Point of H,e0 be FinSequence of CH;
e0 in CH* by FINSEQ_1:def 11; then
P1[z,e0,F . (z,e0)] by A7;
hence thesis;
end;
theorem Th8:
for H being RealUnitarySpace,
G be OrthonormalFamily of H holds
G is linearly-independent
proof
let H be RealUnitarySpace,
G be OrthonormalFamily of H;
for l being Linear_Combination of G st Sum l = 0. H holds
Carrier l = {}
proof
let l be Linear_Combination of G;
assume A1: Sum l = 0. H;
consider F being FinSequence of H such that
A2: F is one-to-one & rng F = Carrier l
& Sum l = Sum (l (#) F) by RLVECT_2:def 8;
assume A3: Carrier l <> {};
A4: Carrier l = { v where v is Element of H : l . v <> 0 }
by RLVECT_2:def 4;
A5: Carrier l c= G by RLVECT_2:def 6;
consider y be object such that
A6: y in Carrier l by A3,XBOOLE_0:def 1;
consider u be Element of H such that
A7: y=u & l.u <> 0 by A4,A6;
consider n be object such that
A9: n in dom F & u = F.n by FUNCT_1:def 3,A2,A6,A7;
A10: dom F = Seg len F by FINSEQ_1:def 3;
reconsider n as Nat by A9;
A11: u = F/.n by A9,PARTFUN1:def 6;
len (l (#) F) = len F &
for i being Nat st i in dom (l (#) F) holds
(l (#) F). i = (l . (F /. i)) * (F /. i)
by RLVECT_2:def 7; then
A13: 1 <= n & n <= len (l (#) F) by A9,A10,FINSEQ_1:1;
A14: dom (l (#) F) = Seg len (l (#) F) by FINSEQ_1:def 3
.= Seg len F by RLVECT_2:def 7
.= dom F by FINSEQ_1:def 3; then
(l (#) F). n = (l . (F /. n)) * (F /. n)
by A9,RLVECT_2:def 7; then
A15: (l (#) F)/. n = (l . (F /. n)) * (F /. n)
by A14,A9,PARTFUN1:def 6;
(F/.n) .|. ((l (#) F)/.n)
= (l . (F /. n)) *((F/.n) .|.(F /. n)) by BHSP_1:3,A15
.= (l . (F /. n)) * 1 by A5,A6,A7,BHSP_5:def 9,A11; then
A17: (F/.n) .|. ((l (#) F)/.n) <> 0 by A7,A9,PARTFUN1:def 6;
A18: for i be Nat st 1<=i & i <= len (l (#) F) & n <> i
holds (F/.n) .|. ((l (#) F)/.i) = 0
proof
let i be Nat;
assume A19:1<=i & i <= len (l (#) F) & n <> i; then
A20a:i in Seg len (l (#) F);
A20: i in dom (l (#) F) by A19,FINSEQ_3:25; then
(l (#) F). i = (l . (F /. i)) * (F /. i) by RLVECT_2:def 7; then
A21: (l (#) F)/. i = (l . (F /. i)) * (F /. i)
by A20,PARTFUN1:def 6;
A22:i in dom F by A20a,A14,FINSEQ_1:def 3; then
F.i in rng F by FUNCT_1:def 3; then
F.i in G by A2,A5; then
A23:F/.i in G by A22,PARTFUN1:def 6;
A25: F.i <> F.n by A9,A22,A2,A19;
A27:F/.i <> F/.n by A9,A25,A22,PARTFUN1:def 6,A11;
thus (F/.n) .|. ((l (#) F)/.i)
= (l . (F /. i)) *((F/.n) .|.(F /. i)) by BHSP_1:3,A21
.=(l . (F /. i)) * 0
by A23,A5,A6,A7,A11,A27,BHSP_5:def 8,BHSP_5:def 9
.= 0;
end;
(F/.n) .|. (Sum (l (#) F))
=(F/.n) .|. ((l (#) F)/.n) by Th5,A13,A18;
hence contradiction by A17,BHSP_1:15,A1,A2;
end;
hence thesis by RLVECT_3:def 1;
end;
begin :: Gram-Schmidt process
::orthonormalizing a set of vectors
definition
let H be RealUnitarySpace;
func ProjSeq(H) ->
Function of [:the carrier of H,(the carrier of H)* :],
(the carrier of H)* means :Def1:
for x be Point of H, e be FinSequence of H
ex Fe be FinSequence of H
st Fe = it.(x,e) & Fe = (x.|.e)(*)e;
existence by Th6;
uniqueness
proof
let F1,F2 be Function of [:the carrier of H,(the carrier of H)* :],
(the carrier of H)*;
assume A1: for x be Point of H, e be FinSequence of H holds
ex Fe be FinSequence of H
st Fe = F1.(x,e) & Fe = (x.|.e)(*)e;
assume A2: for x be Point of H,e be FinSequence of H holds
ex Fe be FinSequence of H
st Fe = F2.(x,e) & Fe = (x.|.e)(*)e;
set CH = the carrier of H;
for z,w being set st z in CH
& w in CH* holds F1.(z,w) = F2.(z,w)
proof
let z,w be set;
assume A3: z in CH & w in CH*; then
reconsider x = z as Point of H;
reconsider e = w as FinSequence of CH by A3,FINSEQ_1:def 11;
A4: ex Fe1 be FinSequence of H st
Fe1 = F1.(x,e) & Fe1 = (x.|.e)(*)e by A1;
ex Fe2 be FinSequence of H st
Fe2 = F2.(x,e) & Fe2 = (x.|.e)(*)e by A2;
hence F1.(z,w) = F2.(z,w) by A4;
end;
hence F1 = F2;
end;
end;
theorem Th7:
for H being RealUnitarySpace holds
for x be FinSequence of H
st x is one-to-one & rng x is linearly-independent
& 1 <= len x holds
ex e be 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 be 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 be 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
let H be RealUnitarySpace;
set CH = the carrier of H;
let x be FinSequence of H;
assume A1:x is one-to-one
& rng x is linearly-independent & 1 <= len x;
len (<*>CH) = 0; then
A2: <*>CH in 0-tuples_on CH & 0 <= len x;
0-tuples_on CH in
{ i-tuples_on CH where i is Nat : i <= len x }; then
reconsider
FINCH = union { i-tuples_on CH where i is Nat : i <= len x }
as non empty set by A2,TARSKI:def 4;
set F = ProjSeq(H);
defpred P1[object,object,object] means
ex e be CH -valued FinSequence,
n be Nat
st e = $2 & n = $1 &
( len e < len x implies
ex g be CH -valued FinSequence
st g = F.[x/.(1+ len e),e] &
$3 = e ^ <* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*>);
A4: for n being Nat st 1 <= n & n < len x holds
for e being Element of FINCH ex f being Element of FINCH
st P1[n,e,f]
proof
let n be Nat;
assume 1 <= n & n < len x;
let e be Element of FINCH;
consider X be set such that
A5: e in X & X in { i-tuples_on CH where i is Nat : i <= len x }
by TARSKI:def 4;
consider i be Nat such that
A6: X = i-tuples_on CH & i <= len x by A5;
ex e0 be Element of CH* st e=e0 & len e0 = i by A5,A6;
then
reconsider e1=e as CH -valued FinSequence;
len e1 < len x implies
ex g be CH -valued FinSequence
st g = F.[x/.(1+ len e1),e1] &
ex f be Element of FINCH st
f = e1^<* 1/ ||. x/.(1+ len e1)-Sum(g) .||
* (x/.(1+ len e1)-Sum(g))*>
proof
assume
A7: len e1 < len x;
set Fe = F.[x/.(1+ len e1),e1];
rng e1 c= CH; then
reconsider E1 = e1 as FinSequence of CH by FINSEQ_1:def 4;
ex Fe be FinSequence of H
st Fe = F.((x/.(1+ len E1)),E1) & Fe = ((x/.(1+ len E1)).|.E1)(*)E1
by Def1; then
reconsider g=Fe as CH -valued FinSequence;
take g;
thus g = F.[x/.(1+ len e1),e1];
set f = e1^<* 1/ ||. x/.(1+ len e1)-Sum(g) .||
* (x/.(1+ len e1)-Sum(g))*>;
len f = len e1 + len <* 1/ ||. x/.(1+ len e1)-Sum(g) .||
* (x/.(1+ len e1)-Sum(g))*> by FINSEQ_1:22
.=len e1 + 1 by FINSEQ_1:40; then
A8: len f <= len x by A7,NAT_1:13;
f is FinSequence of CH by FINSEQ_1:75; then
f in CH* by FINSEQ_1:def 11; then
A9: f in (len f)-tuples_on CH;
(len f)-tuples_on CH in
{ i-tuples_on CH where i is Nat : i <= len x } by A8; then
reconsider f as Element of FINCH by A9,TARSKI:def 4;
take f;
thus thesis;
end;
hence thesis;
end;
set E0 = <* ( 1/||.x/.1 .|| ) * (x/.1) *>;
1-tuples_on CH
in { i-tuples_on CH where i is Nat : i <= len x} by A1;
then
reconsider E0 as Element of FINCH by TARSKI:def 4;
consider E being FinSequence of FINCH such that
len E = len x and
A10:E . 1 = E0 or len x = 0 and
A11:for n being Nat st 1 <= n & n < len x holds
P1[n,E . n,E . (n + 1) ] from RECDEF_1:sch 4(A4);
A14: for k be Nat st k < len x
holds ex e be FinSequence of CH
st len e = k+1 & E.(k+1) = e
proof
defpred P[Nat] means $1 < len x
implies ex e be FinSequence of CH
st len e = $1+1 & E.($1+1) = e;
A15:P[0]
proof
assume 0 < len x;
len <* ( 1/||.x/.1 .|| ) * (x/.1) *> =0+1 by FINSEQ_1:40;
hence thesis by A10,A1;
end;
A17:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A18: P[k];
assume A19:k+1 < len x; then
consider e be FinSequence of CH such that
A20: len e = k+1 & E.(k+1) = e by A18,NAT_1:13;
ex e be CH -valued FinSequence,
n be Nat
st e = E.(k+1) & n =k+1
&
( len e < len x implies
ex g be CH -valued FinSequence
st g = F.[x/.(1+ len e),e] &
E.((k+1)+1) = e^<* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*>) by A11,A19,NAT_1:11;
then consider g be CH -valued FinSequence such that
A21: g = F.[x/.(1+ len e),e]
&
E.((k+1)+1) = e^<* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*> by A19,A20;
take e1= e^<* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*>;
thus len e1 = len e
+ len (<* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*> ) by FINSEQ_1:22
.= (k+1)+1 by A20,FINSEQ_1:40;
thus E.((k+1)+1) = e1 by A21;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A15,A17);
hence thesis;
end;
A22:
for k be Nat st 1 <= k & k < len x holds
ex f,g be FinSequence of CH
st E.k = f & len f = k
& g = F.[x/.(1+ k),f]
& E.(k+1) = f^<* 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) *>
proof
let k be Nat;
assume A23: 1 <= k & k < len x; then
1-1 <= k-1 by XREAL_1:9; then
k-1 in NAT by INT_1:3; then
reconsider k1 = k-1 as Nat;
k1 <= k - 0 by XREAL_1:10; then
k1 < len x by A23,XXREAL_0:2; then
A24: ex e be FinSequence of CH
st len e = k1+1 & E.(k1+1) = e by A14;
consider e be CH -valued FinSequence,
n be Nat such that
A25: e = E.k & n =k
&
( len e < len x implies
ex g be CH -valued FinSequence
st g = F.[x/.(1+ len e),e]
&
E.(k+1) = e^<* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*> ) by A11,A23;
consider g be CH -valued FinSequence such that
A26: g = F.[x/.(1+ len e),e] &
E.(k+1) = e^<* 1/ ||. x/.(1+ len e)-Sum(g) .||
* (x/.(1+ len e)-Sum(g))*>
by A23,A24,A25;
rng g c= CH; then
reconsider g as FinSequence of CH by FINSEQ_1:def 4;
rng e c= CH; then
reconsider e as FinSequence of CH by FINSEQ_1:def 4;
take e,g;
thus E.k = e & len e = k
& g = F.[x/.(1+k),e]
& E.(k+1) = e^<* 1/ ||. x/.(1+k)-Sum g .||
* (x/.(1+k)-Sum g) *> by A24,A25,A26;
end;
defpred Q1[Nat,object,object] means
ex f,g be FinSequence of CH,
ek1 be Point of H
st E.$1 = f & len f = $1 & ek1=$3
& g = F.[x/.(1+ $1),f]
& E.($1+1) = f^ <*ek1*>
& ek1 = 1/ ||. x/.(1+ $1)-Sum g .||
* (x/.(1+ $1)-Sum g);
A27: for k being Nat st 1 <= k & k < len x holds
for e being Element of H ex h being Element of H st Q1[k,e,h]
proof
let k be Nat;
assume A28:1 <= k & k < len x;
let e be Element of H;
consider f,g be FinSequence of CH such that
A29: E.k = f & len f = k
& g = F.[x/.(1+ k),f]
& E.(k+1) = f^<* 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) *> by A28,A22;
take h = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g);
thus thesis by A29;
end;
set e0 = (1/||.x/.1 .||) * (x/.1);
consider e being FinSequence of H such that
A30:len e = len x and
A31:e . 1 = e0 or len x = 0 and
A32:for n being Nat st 1 <= n & n < len x holds
Q1[n,e. n,e . (n + 1) ] from RECDEF_1:sch 4(A27);
A33a:1 in Seg len x by A1;
A33: 1 in dom e by A30,A1,FINSEQ_3:25; then
A34: e/.1 = (1/||.x/.1 .||) * (x/.1) by A1,A31,PARTFUN1:def 6;
A35: for n being Nat st 1 <= n & n < len x holds
ex f,g be FinSequence of CH
st E.n = f & len f = n
& g = F.[x/.(1+ n),f]
& E.(n+1) = f^ <*e/.(n+1)*>
& e/.(n+1) = 1/ ||. x/.(1+ n)-Sum g .||
* (x/.(1+ n)-Sum g)
proof
let k be Nat;
assume A36: 1 <= k & k < len x; then
consider f,g be FinSequence of CH,
ek1 be Point of H such that
A37: E.k = f & len f = k & ek1=e.(k+1)
& g = F.[x/.(1+ k),f]
& E.(k+1) = f^ <*ek1*>
& ek1 = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) by A32;
1<=k+1 & k+1 <= len x by A36,NAT_1:13; then
k+1 in dom e by A30,FINSEQ_3:25; then
e.(k+1) = e/.(k+1) by PARTFUN1:def 6;
hence thesis by A37;
end;
take e;
thus len x = len e by A30;
A38: for n being Nat st 1<=n & n <= len x
holds E.n = e |n
proof
defpred P4[Nat] means
1<=$1 & $1 <= len x implies E.$1 = e| $1;
A39: P4[0];
A40: for k be Nat st P4[k] holds P4[k+1]
proof
let k be Nat;
assume A41: P4[k];
assume
A42:1<=k+1 & k+1 <= len x;
per cases;
suppose A43:k = 0;
e <> {} by A30,A1;
hence E.(k+1) = e|(k+1) by FINSEQ_5:20,A31,A43,A1,A10;
end;
suppose A45a: k <> 0; then
1 <= k by NAT_1:14; then
consider f,g be FinSequence of CH such that
A47: E.k = f & len f = k
& g = F.[x/.(1+ k),f]
& E.(k+1) = f^ <*e/.(k+1)*>
& e/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) by A35,A42,NAT_1:13;
A48:k+1 in dom e by A30,A42,FINSEQ_3:25;
hence E.(k+1) = (e|k) ^ <*e.(k+1)*>
by PARTFUN1:def 6,A47,A45a,A41,A42,NAT_1:13,NAT_1:14
.= e |(k+1) by FINSEQ_5:10,A48;
end;
end;
for k be Nat holds P4[k] from NAT_1:sch 2(A39,A40);
hence thesis;
end;
A49: for k being Nat st 1<=k & k < len x holds
ex g be FinSequence of CH
st g = F.[x/.(1+ k),e|k]
& e/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g)
proof
let n be Nat;
assume A50: 1<=n & n < len x; then
A51: E.n = e|n by A38;
consider f,g be FinSequence of CH such that
A52: E.n = f & len f = n
& g = F.[x/.(1+ n),f]
& E.(n+1) = f^ <*e/.(n+1)*>
& e/.(n+1) = 1/ ||. x/.(1+ n)-Sum g .||
* (x/.(1+ n)-Sum g) by A35,A50;
thus thesis by A51,A52;
end;
defpred P3[Nat] means
$1 <= len x implies
rng (e|$1) is OrthonormalFamily of H &
(e|$1) is one-to-one &
Lin rng (x|$1) = Lin rng (e|$1);
A53: P3[0]
proof
assume 0 <= len x;
A54:for t, u being Point of H st t in rng (e|0)
& u in rng (e|0) & t <> u holds t .|. u = 0;
for t being Point of H st t in rng (e|0)
holds t .|. t = 1;
hence rng (e|0) is OrthonormalFamily of H
by BHSP_5:def 9,BHSP_5:def 8,A54;
thus thesis;
end;
A56: for k be Nat st P3[k] holds P3[k+1]
proof
let k be Nat;
assume A57: P3[k];
assume
A58: k+1 <= len x; then
A60: rng (e|k) is OrthonormalFamily of H &
(e|k) is one-to-one &
Lin rng (x|k) = Lin rng (e|k) by A57,NAT_1:13;
A63:for t,u be Point of H
st t = (e|(k+1)).(k+1) & u in rng (e|k)
holds t .|. u = 0 & u .|. t = 0
proof
let t,u be Point of H;
assume A64: t = (e|(k+1)).(k+1) & u in rng (e|k);
Seg (k+1) c= Seg len x by A58,FINSEQ_1:5; then
A65:Seg (k+1) c= dom e by A30,FINSEQ_1:def 3;
k <> 0 by A64; then
A66: 1 <= k by NAT_1:14;
A67: k < len x by A58,NAT_1:13;
consider g be FinSequence of CH such that
A68: g = F.[x/.(1+ k),e|k]
& e/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) by A66,A49,A58,NAT_1:13;
set z = x/.(1+ k);
set f = e|k;
A69: k+1 in Seg (k+1) by FINSEQ_1:4;
A70: t = e.(k+1) by A64,FUNCT_1:49,FINSEQ_1:4
.= e/.(k+1) by A69,A65,PARTFUN1:def 6;
A71: u .|. t = (1/ ||. x/.(1+ k)-Sum g .||)
* (u .|. (x/.(1+ k)-Sum g)) by A68,A70,BHSP_1:3
.= (1/ ||. x/.(1+ k)-Sum g .||)
* (u .|. (x/.(1+ k)) - u .|. (Sum g)) by BHSP_1:12;
A72: len (e|k) = k by FINSEQ_1:59,A30,A67; then
A73: dom (e|k) = Seg k by FINSEQ_1:def 3;
consider i be object such that
A74: i in dom (e|k) & u = (e|k).i by A64,FUNCT_1:def 3;
reconsider i as Nat by A74;
A75a:Seg k c= Seg (k+1) by FINSEQ_1:5,NAT_1:11;
A77: u = e.i by FUNCT_1:49,A74,A73
.= e/.i by A74,A73,A75a,A65,PARTFUN1:def 6;
consider Fe be FinSequence of H such that
A78: Fe = F.(x/.(1+k),e|k) & Fe = ((x/.(1+k)).|.(e|k))(*)(e|k) by Def1;
W1: len Fe = len (e|k) by A78,DefR; then
A79: 1 <=i & i <= len Fe by A72,A74,A73,FINSEQ_1:1; then
A82:g/.i = Fe.i by PARTFUN1:def 6,A68,A78,FINSEQ_3:25
.= (x/.(1+k)).|. ((e|k)/.i) *((e|k)/.i) by A78,A79,W1,Added;
(e|k).i in rng (e|k) by A74,FUNCT_1:def 3; then
A83: (e|k)/.i in rng (e|k) by A74,PARTFUN1:def 6;
A84:1 <=i & i <= len g by A68,A78,A72,A74,A73,FINSEQ_1:1,W1;
A85:u =(e|k)/.i by A74,PARTFUN1:def 6;
for n be Nat st 1<= n & n <= len g & n <> i holds u .|. (g/.n) = 0
proof
let n be Nat;
assume A86: 1<= n & n <= len g & n <> i; then
n in Seg len Fe by A68,A78; then
A88: n in dom Fe by FINSEQ_1:def 3;
A89:g/.n =Fe.n by A88,PARTFUN1:def 6,A68,A78
.=(x/.(1+k)).|. ((e|k)/.n) *((e|k)/.n) by A78,A68,A86,W1,Added;
A90: (e|k)/.i in rng (e|k) by A85,A74,FUNCT_1:def 3;
n in Seg (len (e|k)) by A86,A78,A68,W1; then
A91:n in dom (e|k) by FINSEQ_1:def 3; then
A92: (e|k)/.n = (e|k).n by PARTFUN1:def 6; then
A93: (e|k)/.n in rng (e|k) by A91,FUNCT_1:def 3;
A94: (e|k)/.n <> (e|k)/.i
by A92,A60,A86,A91,A74,PARTFUN1:def 6;
thus u .|. (g/.n) = ((e|k)/.i) .|.
( (x/.(1+k)).|. ((e|k)/.n) *((e|k)/.n)) by A89,A74,PARTFUN1:def 6
.= (x/.(1+k)).|. ((e|k)/.n)
* (((e|k)/.i ) .|. ((e|k)/.n)) by BHSP_1:3
.= (x/.(1+k)).|. ((e|k)/.n) * 0
by BHSP_5:def 8,A94,A90,A93,A57,A58,NAT_1:13,BHSP_5:def 9
.=0;
end; then
A95: u .|. (Sum g) = u .|. (g/.i) by A84,Th5
.= ((e|k)/.i) .|. (g/.i) by A74,PARTFUN1:def 6
.= (x/.(1+k)).|. ((e|k)/.i) * ((e|k)/.i) .|.((e|k)/.i)
by BHSP_1:3,A82
.= (x/.(1+k)).|. ((e|k)/.i) * 1
by A83,BHSP_5:def 9,A57,A58,NAT_1:13
.= (x/.(1+k)).|. ((e|k)/.i);
(e|k)/.i = (e|k).i by A74,PARTFUN1:def 6
.= e.i by A73,A74,FUNCT_1:49
.= e/.i by A74,A73,A75a,PARTFUN1:def 6,A65;
hence thesis by A71,A77,A95;
end;
A96:for t, u being Point of H st t in rng (e|(k+1))
& u in rng (e|(k+1)) & t <> u holds
t .|. u = 0
proof
let t,u be Point of H;
assume A97: t in rng (e|(k+1))
& u in rng (e|(k+1)) & t <> u; then
consider nt be object such that
A98: nt in dom (e|(k+1)) & t=(e|(k+1)).nt by FUNCT_1:def 3;
consider nu be object such that
A99: nu in dom (e|(k+1)) & u=(e|(k+1)).nu by A97,FUNCT_1:def 3;
Seg (k+1) c= Seg (len x) by A58,FINSEQ_1:5; then
A100:Seg (k+1) c= dom e by A30,FINSEQ_1:def 3;
len (e|(k+1)) = k+1 by FINSEQ_1:59,A58,A30; then
A101:dom (e|(k+1)) = Seg (k+1) by FINSEQ_1:def 3;
reconsider nt,nu as Nat by A98,A99;
A102: 1<= nt & nt <= k + 1 by A98,A101,FINSEQ_1:1;
A103: 1<= nu & nu <= k + 1 by A99,A101,FINSEQ_1:1;
per cases;
suppose nt = k+1 or nu = k+1; then
(nt = k+1 & nu < k+1) or (nt < k+1 & nu = k+1)
by A102,A103,XXREAL_0:1,A97,A98,A99; then
(nt = k+1 & nu <= k) or (nt <= k & nu = k+1)
by NAT_1:13; then
A105: (nt = k+1 & nu in Seg k) or (nt in Seg k & nu = k+1)
by A102,A103;
t= e.nt & u= e.nu by FUNCT_1:47,A98,A99; then
(nt = k+1 & u in rng (e|k))
or (t in rng (e|k) & nu = k+1)
by FUNCT_1:50,A105,A98,A99,A100,A101;
hence t .|. u = 0 by A63,A98,A99;
end;
suppose nt <> k+1 & nu <> k+1; then
nt < k+1 & nu < k+1 by A102,A103,XXREAL_0:1; then
nt <=k & nu <= k by NAT_1:13; then
A106: nt in Seg k & nu in Seg k by A102,A103;
t= e.nt & u= e.nu by FUNCT_1:47,A98,A99; then
t in rng (e|k) & u in rng (e|k)
by FUNCT_1:50,A106,A98,A99,A100,A101;
hence t .|. u = 0
by A97,BHSP_5:def 8,BHSP_5:def 9,A57,A58,NAT_1:13;
end;
end;
A108: ||. x/.1 .|| <> 0
proof
A109: 1 in dom x by A1,FINSEQ_3:25;
set a = ||. x/.1 .||;
assume a = 0; then
x/.1 = 0.H by BHSP_1:26; then
x.1 =0.H by A1,PARTFUN1:def 6,FINSEQ_3:25; then
0.H in rng x by A109,FUNCT_1:def 3;
hence contradiction by A1,RLVECT_3:6;
end;
A110: k <> 0 implies for g be FinSequence of CH
st g = F.[x/.(1+ k),e|k]
holds Sum g in Lin rng (e|k)
proof
assume k <> 0;
let g be FinSequence of CH;
assume A112: g = F.[x/.(1+ k),e|k];
set a = ||. x/.(1+ k)-Sum g .||;
set z = x/.(1+ k)-Sum g;
consider Fe be FinSequence of H such that
A114: Fe = F.(x/.(1+k),e|k) & Fe = ((x/.(1+k)).|. (e|k))(*)(e|k) by Def1;
defpred P20[ object, object ] means
$2= (x/.(1+k)).|. ((e|k)/.$1);
A116: for n being Nat st n in Seg len (e|k) holds
ex z being Element of REAL st P20[n,z];
consider r being FinSequence of REAL such that
A117:dom r = Seg len (e|k)
& for n being Nat st n in Seg len (e|k) holds
P20[n,r.n] from FINSEQ_1:sch 5(A116);
A118: len r = len (e|k) by A117,FINSEQ_1:def 3;
WW: len Fe = len(e|k) by A114,DefR;
A119: for i be Nat st 1 <= i & i <= len (e|k) holds
r/.i=(x/.(1+k)).|. ((e|k)/.i)
proof
let i be Nat;
assume 1 <= i & i <= len (e|k); then
A120: i in Seg len (e|k); then
r.i=(x/.(1+k)).|. ((e|k)/.i) by A117;
hence thesis by A120,A117,PARTFUN1:def 6;
end;
for i be Nat st 1 <= i & i <= len (e|k) holds Fe.i = r/.i*((e|k)/.i)
proof
let i be Nat;
assume A122:1 <= i & i <= len (e|k);
hence Fe.i = (x/.(1+k)).|. ((e|k)/.i) *((e|k)/.i) by A114,Added
.= r/.i*((e|k)/.i) by A122,A119;
end;
then Fe = r(*)(e|k) by DefR,WW;
hence Sum g in Lin rng (e|k) by Th1,A114,A112,A118;
end;
A123: k <> 0 implies
for g be FinSequence of CH
st g = F.[x/.(1+ k),e|k]
holds ||. x/.(1+ k)-Sum g .|| <> 0
proof
assume A124:k <> 0;
let g be FinSequence of CH;
assume A125: g = F.[x/.(1+ k),e|k];
set a = ||. x/.(1+ k)-Sum g .||;
set z = x/.(1+ k)-Sum g;
assume a = 0; then
x/.(1+ k)-Sum g + Sum g = 0.H + Sum g by BHSP_1:26; then
A126: x/.(1+ k) = Sum g by RLVECT_4:1;
Seg (k+1) c= Seg (len x) by A58,FINSEQ_1:5; then
A127: Seg (k+1) c= dom x by FINSEQ_1:def 3;
k+1 in dom x by A127,FINSEQ_1:4; then
x.(1+ k) = Sum g by PARTFUN1:def 6,A126; then
A129: x.(1+ k) in Lin rng (x|k) by A125,A110,A124,A57,A58,NAT_1:13;
A145a: for y be object holds
y in rng (x|k) iff y in rng (x|(k+1)) \ {x.(k+1)}
proof
let y be object;
hereby assume y in rng (x|k); then
consider t be object such that
A130: t in dom (x|k) & y=(x|k).t by FUNCT_1:def 3;
A131: t in dom x & t in Seg k by RELAT_1:57,A130; then
A132: y = x.t by A130,FUNCT_1:49;
reconsider t as Nat by A130;
A133: 1 <= t & t <= k by A131,FINSEQ_1:1;
k < k + 1 by NAT_1:19; then
Seg k c= Seg (k+1) by FINSEQ_1:5; then
A135: t in Seg (k+1) by RELAT_1:57,A130; then
A136: y = (x|(k+1)).t by FUNCT_1:49,A132;
len (x|(k+1)) = k+1 by FINSEQ_1:59,A58; then
dom (x|(k+1)) = Seg (k+1) by FINSEQ_1:def 3; then
A137: y in rng (x|(k+1)) by A136,A135,FUNCT_1:def 3;
Seg (k+1) c= Seg (len x) by A58,FINSEQ_1:5; then
Seg (k+1) c= dom x by FINSEQ_1:def 3; then
A139:k+1 in dom x by FINSEQ_1:4;
t <> k+1 by A133,NAT_1:19; then
x.t <> x.(k+1) by A131,A139,A1; then
not y in {x.(k+1)} by A132,TARSKI:def 1;
hence y in rng (x|(k+1)) \ {x.(k+1)} by A137,XBOOLE_0:def 5;
end;
assume y in rng (x|(k+1)) \ {x.(k+1)}; then
A140: y in rng (x|(k+1)) & not y in {x.(k+1)}
by XBOOLE_0:def 5; then
consider t be object such that
A141: t in dom (x|(k+1)) & y =(x|(k+1)).t
by FUNCT_1:def 3;
A142: k < k + 1 by NAT_1:19;
len (x|(k+1)) = k+1 by FINSEQ_1:59,A58; then
A143: dom (x|(k+1)) = Seg (k+1) by FINSEQ_1:def 3; then
A144: y =x.t by A141,FUNCT_1:49;
reconsider t as Nat by A141;
A145: t <> k+1 by TARSKI:def 1,A144,A140;
M1: 1<=t & t <= k+1 by A141,A143,FINSEQ_1:1; then
t < k+1 by A145,XXREAL_0:1; then
t <= k by NAT_1:13; then
A146: t in Seg k by M1;
len (x|k) = k by FINSEQ_1:59,A142,A58,XXREAL_0:2; then
A147: dom (x|k) = Seg k by FINSEQ_1:def 3;
y=(x|k).t by A144,A146,FUNCT_1:49;
hence y in rng (x|k) by A146,A147,FUNCT_1:def 3;
end;
A149: rng (x|(k+1)) is linearly-independent
by RLVECT_3:5,A1,RELAT_1:70;
len (x|(k+1)) = k+1 by FINSEQ_1:59,A58; then
A150:dom (x|(k+1)) = Seg (k+1) by FINSEQ_1:def 3;
A151:k+1 in Seg (k+1) by FINSEQ_1:4;
x.(1+ k) = (x|(1+ k)) .(1+k) by FINSEQ_1:4,FUNCT_1:49;
then
x.(1+ k) in rng (x|(k+1)) by A150,A151,FUNCT_1:def 3;
hence contradiction by RLVECT_5:17,A145a,TARSKI:2,A129,A149;
end;
for t being Point of H st t in rng (e|(k+1))
holds t .|. t = 1
proof
let t be Point of H;
assume A152: t in rng (e|(k+1));
Seg (k+1) c= Seg (len x) by A58,FINSEQ_1:5; then
A153:Seg (k+1) c= dom e by A30,FINSEQ_1:def 3;
len (e|(k+1)) = k+1 by FINSEQ_1:59,A58,A30; then
A154:dom (e|(k+1)) = Seg (k+1) by FINSEQ_1:def 3;
consider nt be object such that
A155: nt in dom (e|(k+1)) & t=(e|(k+1)).nt
by FUNCT_1:def 3,A152;
reconsider nt as Nat by A155;
A156:t= e.nt by FUNCT_1:47,A155
.= e/.nt by A155,A154,A153,PARTFUN1:def 6;
A157: 1<= nt & nt <= k + 1 by A155,A154,FINSEQ_1:1;
per cases;
suppose A159:nt = k+1;
per cases;
suppose k = 0; then
A161: t = (1/||.x/.1 .||) * (x/.1)
by A33,A1,A31,PARTFUN1:def 6,A156,A159;
set a = ||. x/.1 .||;
set z = x/.1;
A162: 1 in dom x by A1,FINSEQ_3:25;
A163: a <> 0
proof
assume a = 0; then
x/.1 = 0.H by BHSP_1:26; then
x.1 = 0.H by A1,FINSEQ_3:25,PARTFUN1:def 6; then
0.H in rng x by A162,FUNCT_1:def 3;
hence contradiction by A1,RLVECT_3:6;
end;
thus t .|. t = (1/a)*(z .|. ((1/a)*z)) by BHSP_1:def 2,A161
.= (1/a)*((1/a)*(z .|.z)) by BHSP_1:3
.= (1/a)*((1/a)* ||.z.||^2) by Lm1
.= (1/a)*((1/a)* (a*a)) by SQUARE_1:def 1
.= (1/a)*((1/a)* a*a)
.= (1/a)*(1*a) by A163,XCMPLX_1:87
.= 1 by A163,XCMPLX_1:87;
end;
suppose A164: k <> 0;
A166: k < len x by A58,NAT_1:13;
consider g be FinSequence of CH such that
A167: g = F.[x/.(1+ k),e|k]
& e/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g)
by A49,A164,A166,NAT_1:14;
set a = ||. x/.(1+ k)-Sum g .||;
set z = x/.(1+ k)-Sum g;
thus t .|. t
= (1/a)*(z .|. ((1/a)*z)) by BHSP_1:def 2,A156,A167,A159
.= (1/a)*((1/a)*(z .|.z)) by BHSP_1:3
.= (1/a)*((1/a)* ||.z.||^2) by Lm1
.= (1/a)*((1/a)* (a*a)) by SQUARE_1:def 1
.= (1/a)*((1/a)* a*a)
.= (1/a)*(1*a) by A123,A167,A164,XCMPLX_1:87
.= 1 by A123,A167,A164,XCMPLX_1:87;
end;
end;
suppose nt <> k+1; then
nt < k+1 by A157,XXREAL_0:1; then
nt <= k by NAT_1:13; then
A169: nt in Seg k by A157;
t= e.nt by FUNCT_1:47,A155;
hence t .|. t = 1 by FUNCT_1:50,A155,A153,A154,A169,
BHSP_5:def 9,NAT_1:13,A57,A58;
end;
end;
hence rng (e|(k+1)) is OrthonormalFamily of H
by BHSP_5:def 8,A96,BHSP_5:def 9;
thus e|(k+1) is one-to-one
proof
assume not e|(k+1) is one-to-one; then
consider t1, t2 being object such that
A170: t1 in dom (e|(k+1)) & t2 in dom (e|(k+1))
& (e|(k+1)) . t1 = (e|(k+1)) . t2 & t1 <> t2;
A171: t1 in dom e & t1 in Seg (k+1) by A170,RELAT_1:57;
reconsider t1 as Nat by A170;
A172: t2 in dom e & t2 in Seg (k+1) by A170,RELAT_1:57;
reconsider t2 as Nat by A170;
A173: not (t1 in Seg k & t2 in Seg k)
proof
assume A174:t1 in Seg k & t2 in Seg k; then
A175: t1 in dom (e|k) & t2 in dom (e|k) by A171,A172,RELAT_1:57;
A176:(e|k).t1 = e.t1 by FUNCT_1:49,A174
.=(e|(k+1)).t1 by FUNCT_1:49,A171;
(e|k).t2 = e.t2 by FUNCT_1:49,A174
.=(e|(k+1)).t2 by FUNCT_1:49,A172;
hence contradiction by A170,A175,A60,A176;
end;
A179: 1 <=t1 & t1 <= k+1 by A171,FINSEQ_1:1;
A180: 1 <=t2 & t2 <= k+1 by A172,FINSEQ_1:1; then
(t1 > k) or (t2 > k) by A179,A173; then
k+1 <= t1 or k+1 <= t2 by NAT_1:13; then
((1<=t1 & t1 <= k+1) & t1 <> k+1 & t2= k+1)
or (t1= k+1 & (1<=t2 & t2 <= k+1) & t2 <> k+1)
by A170,A179,A180,XXREAL_0:1; then
(1<=t1 & t1 < k+1 & t2= k+1)
or (t1= k+1 & 1<=t2 & t2 < k+1) by XXREAL_0:1; then
A181a:(1<=t1 & t1 <= k & t2= k+1)
or (t1= k+1 & 1<=t2 & t2 <=k) by NAT_1:13;
per cases by A181a;
suppose
A182: t1 in Seg k & t2= k+1;
A183: (e|(k+1)) /. t1
= (e|(k+1)).t1 by A170,PARTFUN1:def 6
.= e.t1 by A171,FUNCT_1:49
.=(e|k).t1 by A182,FUNCT_1:49;
A184a:t1 in dom (e|k) by A171,RELAT_1:57,A182; then
A184: (e|(k+1)) /. t1 in rng (e|k) by A183,FUNCT_1:def 3;
A186: (e|(k+1)) /. (k+1) = (e|(k+1)).(k+1)
by A182,A170,PARTFUN1:def 6;
A187: (e|(k+1)) /. t2 =(e|(k+1)) .t2 by PARTFUN1:def 6,A170
.=(e|(k+1)) /.t1 by A170,PARTFUN1:def 6;
then
(e|(k+1)) /. t2 in rng (e|k) by A184a,A183,FUNCT_1:def 3; then
((e|(k+1)) /. t1) .|. ((e|(k+1)) /.(k+1)) = 1
by A187,A182,BHSP_5:def 9,A57,A58,NAT_1:13;
hence contradiction by A63,A184,A186;
end;
suppose
A189: t2 in Seg k & t1= k+1;
A190: (e|(k+1)) /. t2
=(e|(k+1)).t2 by A170,PARTFUN1:def 6
.= e.t2 by A172,FUNCT_1:49
.=(e|k).t2 by A189,FUNCT_1:49;
t2 in dom (e|k) by A172,RELAT_1:57,A189; then
A191: (e|(k+1)) /. t2 in rng (e|k) by A190,FUNCT_1:def 3;
A193: (e|(k+1)) /. (k+1) = (e|(k+1)).(k+1)
by A189,A170,PARTFUN1:def 6;
(e|(k+1)) /. t1 =(e|(k+1)) .t1 by PARTFUN1:def 6,A170
.= (e|(k+1)) /.t2 by A170,PARTFUN1:def 6;
then ((e|(k+1)) /. t2) .|. ((e|(k+1)) /.(k+1)) = 1
by A189,BHSP_5:def 9,A191,A57,A58,NAT_1:13;
hence contradiction by A63,A191,A193;
end;
end;
for y be object st y in rng (x|(k+1))
holds y in the carrier of Lin rng (e|(k+1))
proof
let y be object;
assume y in rng (x|(k+1)); then
consider t be object such that
A196: t in dom (x|(k+1)) & y =(x|(k+1)).t
by FUNCT_1:def 3;
len (x|(k+1)) = k+1 by FINSEQ_1:59,A58; then
A197: dom (x|(k+1)) = Seg (k+1) by FINSEQ_1:def 3; then
A198: y =x.t by A196,FUNCT_1:49;
reconsider t as Nat by A196;
A199: t in dom x & t in Seg (k+1) by A196,RELAT_1:57;
A200a:len (e|(k+1)) = k+1 by FINSEQ_1:59,A30,A58; then
A200: dom (e|(k+1)) = Seg (k+1) by FINSEQ_1:def 3;
A208: rng (e|k) c= rng (e|(k+1))
proof
let y be object;
assume y in rng (e|k); then
consider t be object such that
A202: t in dom (e|k) & y =(e|k).t by FUNCT_1:def 3;
A203: k < k + 1 by NAT_1:19; then
len (e|k) = k by FINSEQ_1:59,A58,XXREAL_0:2,A30; then
dom (e|k) = Seg k by FINSEQ_1:def 3; then
A204: y =e.t by A202,FUNCT_1:49;
reconsider t as Nat by A202;
A205: t in dom e & t in Seg k by A202,RELAT_1:57; then
1<=t & t <= k by FINSEQ_1:1; then
1<=t & t <= k+1 by A203,XXREAL_0:2; then
A206:t in Seg (k+1); then
A207: y =(e|(k+1)).t by A204,FUNCT_1:49;
t in dom (e|(k+1)) by RELAT_1:57,A205,A206;
hence y in rng (e|(k+1)) by A207,FUNCT_1:def 3;
end;
per cases;
suppose A209: k = 0; then
t in Seg (0+1) by A196,RELAT_1:57; then
y = x.1 by A198,TARSKI:def 1,FINSEQ_1:2; then
A212: y=x/.1 by A1,FINSEQ_3:25,PARTFUN1:def 6;
1 in Seg len x by A1; then
A213: 1 in dom e by A30,FINSEQ_1:def 3;
A215: ||.x/.1 .|| * e/.1 = ||.x/.1 .|| * (1/||.x/.1 .||) *x/.1
by RLVECT_1:def 7,A34
.= 1*x/.1 by A108,XCMPLX_1:87
.= x/.1 by RLVECT_1:def 8;
A216: dom (e|1) = Seg 1 by A200a,A209,FINSEQ_1:def 3;
A217: 1 in Seg 1; then
(e|1).1 = e.1 by FUNCT_1:49
.= e/.1 by A213,PARTFUN1:def 6; then
e/.1 in rng (e|1) by A216,A217,FUNCT_1:def 3; then
y in Lin rng (e|(k+1)) by A215,A209,A212,RLSUB_1:21,RLVECT_3:15;
hence y in the carrier of Lin rng (e|(k+1)) by STRUCT_0:def 5;
end;
suppose A218:k <> 0;
k < len x by A58,NAT_1:13; then
consider g be FinSequence of CH such that
A220: g = F.[x/.(1+ k),e|k]
& e/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) by A218,A49,NAT_1:14;
per cases;
suppose A223:t = k+1;
set r = ||. x/.(1+ k)-Sum g .||;
r* e/.(k+1) =r*(1/ r)*(x/.(1+ k)-Sum g) by RLVECT_1:def 7,A220
.= 1*(x/.(1+ k)-Sum g) by XCMPLX_1:87,A218,A220,A123
.=x/.(1+ k)-Sum g by RLVECT_1:def 8; then
A224: x/.(1+ k) = r* e/.(k+1) + Sum g by RLVECT_4:1;
Seg (k+1) c= Seg len e by A30,A58,FINSEQ_1:5; then
Seg (k+1) c= dom e by FINSEQ_1:def 3; then
A225:k+1 in dom e by FINSEQ_1:4;
(e|(k+1)).(k+1) = e.(k+1) by A223,A196,A197,FUNCT_1:49
.=e/.(k+1) by A225,PARTFUN1:def 6; then
e/.(k+1) in rng (e|(k+1)) by A199,A200,FUNCT_1:def 3,A223;
then
A226: r* e/.(k+1) in Lin rng (e|(k+1)) by RLSUB_1:21,RLVECT_3:15;
Lin rng (e|k) is Subspace of Lin rng (e|(k+1))
by RLVECT_3:20,A208; then
A227a: Sum g in Lin rng (e|(k+1)) by RLSUB_1:8,A218,A220,A110;
y =x/.(1+ k) by A223,A198,A199,PARTFUN1:def 6;
hence y in the carrier of Lin rng (e|(k+1))
by STRUCT_0:def 5,A224,A227a,A226,RLSUB_1:20;
end;
suppose A228: t <> k+1;
M1: 1<=t & t <= k+1 by A196,A197,FINSEQ_1:1; then
t < k+1 by A228,XXREAL_0:1; then
t <= k by NAT_1:13; then
A229: t in Seg k by M1; then
A230: t in dom (x|k) by A199,RELAT_1:57;
y = (x|k).t by A198,A229,FUNCT_1:49; then
A231a:y in rng (x|k) by A230,FUNCT_1:def 3;
Lin rng (e|k) is Subspace of Lin rng (e|(k+1))
by RLVECT_3:20,A208; then
y in Lin rng (e|(k+1))
by A231a,RLSUB_1:8,RLVECT_3:15,A57,A58,NAT_1:13;
hence y in the carrier of Lin rng (e|(k+1)) by STRUCT_0:def 5;
end;
end;
end; then
A232:rng (x|(k+1)) c= the carrier of Lin rng (e|(k+1));
for y be object st y in rng (e|(k+1))
holds y in the carrier of Lin rng (x|(k+1))
proof
let y be object;
assume y in rng (e|(k+1)); then
consider t be object such that
A233: t in dom (e|(k+1)) & y =(e|(k+1)).t
by FUNCT_1:def 3;
len (e|(k+1)) = k+1 by FINSEQ_1:59,A58,A30; then
A234: dom (e|(k+1)) = Seg (k+1) by FINSEQ_1:def 3; then
A235: y = e.t by A233,FUNCT_1:49;
reconsider t as Nat by A233;
A236: t in dom e & t in Seg (k+1) by A233,RELAT_1:57;
A237a:len (x|(k+1)) = k+1 by FINSEQ_1:59,A58; then
A237: dom (x|(k+1)) = Seg (k+1) by FINSEQ_1:def 3;
A245: rng (x|k) c= rng (x|(k+1))
proof
let y be object;
assume y in rng (x|k); then
consider t be object such that
A239: t in dom (x|k) & y = (x|k).t by FUNCT_1:def 3;
A240: k < k + 1 by NAT_1:19; then
len (x|k) = k by FINSEQ_1:59,A58,XXREAL_0:2; then
dom (x|k) = Seg k by FINSEQ_1:def 3; then
A241: y = x.t by A239,FUNCT_1:49;
reconsider t as Nat by A239;
A242: t in dom x & t in Seg k by A239,RELAT_1:57; then
S1: 1 <= t & t <= k by FINSEQ_1:1; then
t <= k+1 by A240,XXREAL_0:2; then
A243:t in Seg (k+1) by S1; then
A244: y =(x|(k+1)).t by A241,FUNCT_1:49;
t in dom (x|(k+1)) by RELAT_1:57,A242,A243;
hence y in rng (x|(k+1)) by A244,FUNCT_1:def 3;
end;
per cases;
suppose A246: k = 0; then
t in Seg (0+1) by A233,RELAT_1:57; then
A247: y = e.1 by A235,TARSKI:def 1,FINSEQ_1:2;
A248: 1 in Seg len e by A30,A1; then
1 in dom e by FINSEQ_1:def 3; then
A249: y=e/.1 by A247,PARTFUN1:def 6;
A250: 1 in dom x by A30,A248,FINSEQ_1:def 3;
A252: dom (x|1) = Seg 1 by A237a,A246,FINSEQ_1:def 3;
A253: 1 in Seg 1; then
(x|1).1 = x.1 by FUNCT_1:49
.=x/.1 by A250,PARTFUN1:def 6; then
x/.1 in rng (x|1) by A252,A253,FUNCT_1:def 3; then
y in Lin rng (x|(k+1)) by A34,A246,A249,RLSUB_1:21,RLVECT_3:15;
hence y in the carrier of Lin rng (x|(k+1))
by STRUCT_0:def 5;
end;
suppose A254:k <> 0; then
1 <= k by NAT_1:14; then
consider g be FinSequence of CH such that
A256: g = F.[x/.(1+ k),e|k]
& e/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g) by A58,NAT_1:13,A49;
per cases;
suppose A258:t = k+1;
set r = ||. x/.(1+ k)-Sum g .||;
A259: e/.(k+1) = (1/r)*x/.(1+ k)-(1/ r)*Sum g by RLVECT_1:34,A256;
Seg (k+1) c= Seg len x by A58, FINSEQ_1:5; then
Seg (k+1) c= dom x by FINSEQ_1:def 3; then
A260:k+1 in dom x by FINSEQ_1:4;
(x|(k+1)).(k+1) = x.(k+1) by A233,A234,FUNCT_1:49,A258
.=x/.(k+1) by A260,PARTFUN1:def 6; then
x/.(k+1) in rng (x|(k+1)) by A236,A237,FUNCT_1:def 3,A258; then
A261: (1/r)* x/.(k+1) in Lin rng (x|(k+1)) by RLVECT_3:15,RLSUB_1:21;
Lin rng (x|k) is Subspace of Lin rng (x|(k+1))
by RLVECT_3:20,A245; then
Sum g in Lin rng (x|(k+1)) by A254,A256,A110,A57,A58,NAT_1:13,RLSUB_1:8;
then A262a:
(1/ r)* Sum g in Lin rng (x|(k+1)) by RLSUB_1:21;
y =e/.(1+ k) by A258,A235,A236,PARTFUN1:def 6;
hence y in the carrier of Lin rng (x|(k+1))
by STRUCT_0:def 5,A259,A262a,A261,RLSUB_1:23;
end;
suppose A263:t <> k+1;
M1: 1<=t & t <= k+1 by A233,A234,FINSEQ_1:1; then
t < k+1 by A263,XXREAL_0:1; then
t <= k by NAT_1:13; then
A264: t in Seg k by M1; then
A265: t in dom (e|k) by A236,RELAT_1:57;
y = (e|k).t by A235,A264,FUNCT_1:49; then
A266a: y in rng (e|k) by A265,FUNCT_1:def 3;
Lin rng (x|k) is Subspace of Lin rng (x|(k+1))
by RLVECT_3:20,A245; then
y in Lin rng (x|(k+1)) by A266a,RLSUB_1:8,A57,A58,NAT_1:13,RLVECT_3:15;
hence y in the carrier of Lin rng (x|(k+1)) by STRUCT_0:def 5;
end;
end;
end; then
rng (e|(k+1)) c= the carrier of Lin rng (x|(k+1));
hence Lin rng (x|(k+1)) = Lin rng (e|(k+1)) by Th3,A232;
end;
A267: for k be Nat holds P3[k] from NAT_1:sch 2(A53,A56);
then
A268: rng (e|len e) is OrthonormalFamily of H &
(e|len e) is one-to-one &
Lin rng (x|len x) = Lin rng (e|len e) by A30;
dom x = Seg len x & dom e = Seg len e by FINSEQ_1:def 3;
hence thesis by A33a,A31,PARTFUN1:def 6,A49,A267,A268,A30;
end;
definition
let H be RealUnitarySpace,
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:
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 be 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 be 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
let e1,e2 be FinSequence of H;
assume that
A2: len x = len e1 &
rng e1 is OrthonormalFamily of H &
e1 is one-to-one &
Lin rng x = Lin rng e1 &
e1/.1 = ( 1/||.x/.1 .|| ) * (x/.1) &
( for k being Nat st 1<=k & k < len x holds
ex g be FinSequence of H
st g = ( ProjSeq(H)) .[x/.(1+ k),e1|k]
& e1/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g))
&
for k be Nat st k <= len x
holds rng (e1|k) is OrthonormalFamily of H &
(e1|k) is one-to-one &
Lin rng (x|k) = Lin rng (e1|k) and
A3: len x = len e2 &
rng e2 is OrthonormalFamily of H &
e2 is one-to-one &
Lin rng x = Lin rng e2 &
e2/.1 = ( 1/||.x/.1 .|| ) * (x/.1) &
( for k being Nat st 1<=k & k < len x holds
ex g be FinSequence of H
st g = ( ProjSeq(H)) .[x/.(1+ k),e2|k]
& e2/.(k+1) = 1/ ||. x/.(1+ k)-Sum g .||
* (x/.(1+ k)-Sum g)) &
for k be Nat st k <= len x
holds rng (e2|k) is OrthonormalFamily of H &
(e2|k) is one-to-one &
Lin rng (x|k) = Lin rng (e2|k);
A4: e1 <> {} & e2 <> {} by A1,A2,A3;
defpred P[Nat] means
1 <= $1 & $1 <= len x implies e1|$1 = e2|$1;
A6: P[0];
A7: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A8: P[n];
assume A9: 1 <= n+1 & n+1 <= len x;
per cases;
suppose A10: n = 0;
hence e1|(n+1) = <*e1.1*> by FINSEQ_5:20,A4
.= <*e1/.1*> by PARTFUN1:def 6,A4,A2,FINSEQ_3:32
.= <*e2.1*> by A4,PARTFUN1:def 6,A3,A2,FINSEQ_3:32
.= e2|(n+1) by A10,FINSEQ_5:20,A4;
end;
suppose
A11a:n <> 0; then
A11: 1 <= n by NAT_1:14; then
consider g1 be FinSequence of H such that
A14: g1 = ( ProjSeq(H)) .[x/.(1+ n),e1|n]
& e1/.(n+1) = 1/ ||. x/.(1+ n)-Sum g1 .||
* (x/.(1+ n)-Sum g1) by A2,A9,NAT_1:13;
consider g2 be FinSequence of H such that
A15: g2 = ( ProjSeq(H)) .[x/.(1+ n),e2|n]
& e2/.(n+1) = 1/ ||. x/.(1+ n)-Sum g2 .||
* (x/.(1+ n)-Sum g2) by A3,A11,A9,NAT_1:13;
n+1 in Seg len x by A9; then
A17: n+1 in dom e1 & n+1 in dom e2 by A2,A3,FINSEQ_1:def 3;
hence e1|(n+1) = e1|n ^ <* e1.(n+1) *> by FINSEQ_5:10
.=e1|n ^ <* e1/.(n+1) *> by A17,PARTFUN1:def 6
.=e2|n ^ <* e2.(n+1) *> by A17,PARTFUN1:def 6,
A8,A11a,NAT_1:14,A9,NAT_1:13,A14,A15
.=e2|(n+1) by FINSEQ_5:10,A17;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A7); then
A19: e1|(len x) = e2|len x by A1;
A20: dom e1 = Seg len x by A2,FINSEQ_1:def 3;
dom e2 = Seg len x by A3,FINSEQ_1:def 3;
hence e1 = e2 by A19,A20;
end;
end;
theorem
for H being RealUnitarySpace,
x be 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
let H be RealUnitarySpace,
x be FinSequence of H;
assume x is one-to-one
& rng x is linearly-independent
& 1 <= len x; then
len x = len GramSchmidt (x) &
rng GramSchmidt (x) is OrthonormalFamily of H &
GramSchmidt (x) is one-to-one by Def2;
hence thesis by Th8;
end;