:: Completeness of the Real {E}uclidean Space
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 28, 2005
:: Copyright (c) 2005-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 NUMBERS, SUBSET_1, NAT_1, BINOP_1, FUNCT_1, ARYTM_3, FINSEQ_2,
ZFMISC_1, RELAT_1, COMPLEX1, STRUCT_0, XBOOLE_0, NORMSP_1, SUPINF_2,
EUCLID, ALGSTR_0, RLVECT_1, PRE_TOPC, REAL_1, CARD_1, XXREAL_0, ARYTM_1,
FINSEQ_1, CARD_3, ORDINAL4, TARSKI, RVSUM_1, SQUARE_1, SEQ_2, ORDINAL2,
SEQ_1, VALUED_1, RSSPACE3, LOPBAN_1, REWRITE1, BHSP_1, PROB_2, BINOP_2,
METRIC_1, BHSP_3, REAL_NS1, RELAT_2, NORMSP_0, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, BINOP_1,
PRE_TOPC, ORDINAL1, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCT_2,
STRUCT_0, ALGSTR_0, FUNCOP_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1,
COMPLEX1, REAL_1, RLVECT_1, BHSP_1, BHSP_2, BINOP_2, VALUED_1, SEQ_1,
SEQ_2, RVSUM_1, NORMSP_0, NORMSP_1, EUCLID, RSSPACE3, LOPBAN_1, BHSP_3;
constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, SEQ_2, FINSEQOP, REALSET2,
BHSP_2, BHSP_3, RSSPACE3, LOPBAN_1, RVSUM_1, EUCLID, RELSET_1, COMSEQ_2,
BINOP_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, NUMBERS,
XXREAL_0, XREAL_0, MEMBERED, FINSEQ_2, STRUCT_0, NORMSP_0, NORMSP_1,
BHSP_1, REVROT_1, RSSPACE3, VALUED_0, VALUED_1, FUNCT_2, EUCLID,
FINSEQ_1, CARD_1, SQUARE_1, RVSUM_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions RLVECT_1, RSSPACE3, BHSP_3, ALGSTR_0, NORMSP_0;
equalities RLVECT_1, BINOP_1, BHSP_1, RSSPACE3, SQUARE_1, STRUCT_0, ALGSTR_0,
VALUED_1, NORMSP_0;
expansions RLVECT_1, BINOP_1, BHSP_1, RSSPACE3, BHSP_3, NORMSP_0;
theorems XREAL_0, NORMSP_1, EUCLID, RLVECT_1, SEQ_2, SEQ_4, BINOP_1, COMPLEX1,
ABSVALUE, RSSPACE3, FINSEQ_1, FINSEQ_2, RVSUM_1, FUNCT_2, LOPBAN_1,
ZFMISC_1, FUNCOP_1, SEQ_1, NAT_1, SQUARE_1, FUNCT_1, FINSEQ_5, XREAL_1,
RFUNCT_4, BHSP_2, EUCLID_2, EUCLID_4, EUCLIDLP, XXREAL_0, VALUED_1,
NORMSP_0, ORDINAL1, CARD_1;
schemes NAT_1, SEQ_1, BINOP_1, BINOP_2, FUNCT_2, FINSEQ_1;
begin :: R^n space as RealLinearSpace
reserve n for Nat;
Lm1: for n being Nat ex ADD be BinOp of REAL n st (for a,b being Element of
REAL n holds ADD.(a,b) = a+b) & ADD is commutative associative
proof
let n be Nat;
deffunc P(Element of REAL n,Element of REAL n) = $1+$2;
consider ADD be BinOp of REAL n such that
A1: for a,b being Element of REAL n holds ADD.(a,b)=P(a,b) from BINOP_1:
sch 4;
now
let a,b,c be Element of REAL n;
reconsider a1=a,b1=b,c1=c as Element of n-tuples_on REAL by EUCLID:def 1;
thus ADD.(a,ADD.(b,c)) = a+ADD.(b,c) by A1
.= a+(b+c) by A1
.= (a1+b1)+c1 by RVSUM_1:15
.= ADD.(a,b)+c by A1
.= ADD.(ADD.(a,b),c) by A1;
end;
then
A2: ADD is associative;
now
let a,b be Element of REAL n;
thus ADD.(a,b) = a+b by A1
.= ADD.(b,a) by A1;
end;
then ADD is commutative;
hence thesis by A1,A2;
end;
definition
let n be Nat;
func Euclid_add n -> BinOp of REAL n means
:Def1:
for a,b being Element of REAL n holds it.(a,b) = a+b;
existence
proof
consider ADD be BinOp of REAL n such that
A1: for a,b being Element of REAL n holds ADD.(a,b) = a+b and
ADD is commutative associative by Lm1;
take ADD;
thus thesis by A1;
end;
uniqueness
proof
deffunc O(Element of REAL n, Element of REAL n)=$1+$2;
for o1,o2 being BinOp of REAL n st (for a,b being Element of REAL n
holds o1.(a,b) = O(a,b)) & (for a,b being Element of REAL n holds o2.(a,b) = O(
a,b)) holds o1 = o2 from BINOP_2:sch 2;
hence thesis;
end;
end;
registration
let n be Nat;
cluster Euclid_add n -> commutative associative;
coherence
proof
ex ADD be BinOp of REAL n st ( for a,b being Element of REAL n holds
ADD.(a,b) = a+b)& ADD is commutative associative by Lm1;
hence thesis by Def1;
end;
end;
definition
let n be Nat;
func Euclid_mult n -> Function of [: REAL, REAL n :], REAL n means
:Def2:
for r be Real, x be Element of REAL n holds it.(r,x) = r*x;
existence
proof
deffunc F(Real,Element of REAL n) = $1 * $2;
consider f be Function of [:REAL, REAL n:], REAL n such that
A1: for r be Element of REAL
, x be Element of REAL n holds f.(r,x) = F(r,x) from BINOP_1:sch 4;
take f;
let r be Real, x be Element of REAL n;
reconsider r as Element of REAL by XREAL_0:def 1;
f.(r,x) = F(r,x) by A1;
hence thesis;
end;
uniqueness
proof
let mult1,mult2 be Function of [: REAL, REAL n :], REAL n such that
A2: for r be Real, x be Element of REAL n holds mult1.(r,x)
= r*x and
A3: for r be Real, x be Element of REAL n holds mult2.(r,x) = r*x;
for r being Element of REAL, x being Element of REAL n holds mult1.(r,
x) = mult2.(r,x)
proof
let r be Element of REAL;
let x be Element of REAL n;
thus mult1.(r,x) = r*x by A2
.= mult2.(r,x) by A3;
end;
hence thesis;
end;
end;
definition
let n be Nat;
func Euclid_norm n -> Function of REAL n,REAL means
:Def3:
for x being Element of REAL n holds it.x = |.x.|;
existence
proof
deffunc F(Element of REAL n) = In(|.$1.|,REAL);
consider f being Function of REAL n, REAL such that
A1: for x being Element of REAL n holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let x be Element of REAL n;
f.x = F(x) by A1;
hence thesis;
end;
uniqueness
proof
let f,g be Function of REAL n, REAL;
assume that
A2: for x being Element of REAL n holds f.x = |.x.| and
A3: for x being Element of REAL n holds g.x = |.x.|;
now
let x be Element of REAL n;
thus f.x = |.x.| by A2
.= g.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let n be Nat;
func REAL-NS n -> strict non empty NORMSTR means
:Def4:
the carrier of it =
REAL n & 0.it = 0*n & the addF of it = Euclid_add n & the Mult of it =
Euclid_mult n & the normF of it = Euclid_norm n;
existence
proof
take NORMSTR(#REAL n, 0*n, Euclid_add n, Euclid_mult n, Euclid_norm n #);
thus thesis;
end;
uniqueness;
end;
registration
let n be non zero Nat;
cluster REAL-NS n -> non trivial;
coherence
proof
the carrier of REAL-NS n = REAL n by Def4
.= the carrier of TOP-REAL n by EUCLID:22;
hence thesis;
end;
end;
theorem Th1:
for x be VECTOR of REAL-NS n, y be Element of REAL n st x=y holds
||.x.|| = |.y.|
proof
let x be VECTOR of REAL-NS n;
let y be Element of REAL n;
assume
A1: x=y;
thus ||.x.|| = (the normF of REAL-NS n).x
.= (Euclid_norm n).y by A1,Def4
.= |.y.| by Def3;
end;
theorem Th2:
for n be Nat for x,y be VECTOR of REAL-NS n, a,b be
Element of REAL n st x=a & y=b holds x+y = a + b
proof
let n be Nat;
let x,y be VECTOR of REAL-NS n;
let a,b be Element of REAL n;
assume x=a & y=b;
hence x+y = (Euclid_add n).(a,b) by Def4
.= a+b by Def1;
end;
theorem Th3:
for x be VECTOR of REAL-NS n, y be Element of REAL n, a be Real
st x=y holds a * x = a * y
proof
let x be Point of REAL-NS n, y be Element of REAL n, a be Real;
assume
A1: x = y;
reconsider a as Real;
a * x =(Euclid_mult n).(a,x) by Def4
.=a*y by A1,Def2;
hence thesis;
end;
registration
let n be Nat;
cluster REAL-NS n -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence
proof
reconsider x1=0.(REAL-NS n) as Element of REAL n by Def4;
|.x1.| = 0 iff x1 = 0*n by EUCLID:7,8;
hence ||. 0.(REAL-NS n) .|| = 0 by Def4,Th1;
for x,y being Point of REAL-NS n, a be Real
holds ( ||.x.|| = 0 iff x
= 0.(REAL-NS n) ) & ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y.|| <= ||.x.|| +
||.y.||
proof
let x,y be Point of REAL-NS n;
let a be Real;
thus ||.x.|| = 0 iff x = 0.(REAL-NS n)
proof
reconsider x1=x as Element of REAL n by Def4;
|.x1.| = 0 iff x1 = 0*n by EUCLID:7,8;
hence thesis by Def4,Th1;
end;
thus ||.a * x.|| = |.a.| * ||.x.||
proof
reconsider x1=x as Element of REAL n by Def4;
thus ||.a * x.|| = |.a*x1.| by Th1,Th3
.= |.a.|*|.x1.| by EUCLID:11
.= |.a.|*||.x.|| by Th1;
end;
thus ||.x + y.|| <= ||.x.|| + ||.y.||
proof
reconsider x1=x,y1=y as Element of REAL n by Def4;
|. x1+ y1 .| <= |. x1 .| + |. y1 .| by EUCLID:12;
then
A1: |. x1+ y1 .| <= ||.x.|| +|. y1 .| by Th1;
||.x + y.|| = |. x1+ y1 .| by Th1,Th2;
hence thesis by A1,Th1;
end;
end;
hence REAL-NS n is discerning RealNormSpace-like by NORMSP_1:def 1;
A2: for a,b be Real, v being VECTOR of REAL-NS n holds (a + b) * v
= a * v + b * v
proof
let a,b be Real;
reconsider a,b as Real;
let v be VECTOR of REAL-NS n;
(a + b) * v = a * v + b * v
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
A3: a * v = a * v1 & b * v = b * v1 by Th3;
thus (a + b) * v =(Euclid_mult n).(a + b,v) by Def4
.=(a + b) * v2 by Def2
.=a*v2 + b*v2 by RVSUM_1:50
.=a * v + b * v by A3,Th2;
end;
hence thesis;
end;
A4: for a be Real, v,w being VECTOR of REAL-NS n holds a * (v + w)
= a * v + a * w
proof
let a be Real;
reconsider a as Real;
let v,w be VECTOR of REAL-NS n;
a * (v + w) = a * v + a * w
proof
reconsider v1 = v, w1 = w as Element of REAL n by Def4;
reconsider v2=v1,w2=w1 as Element of n-tuples_on REAL by EUCLID:def 1;
A5: a * v =a * v1 & a * w =a * w1 by Th3;
thus a * (v + w) =(Euclid_mult n).(a,v+w) by Def4
.=(Euclid_mult n).(a,v1+w1) by Th2
.= a*(v2+w2) by Def2
.=a*v2 + a*w2 by RVSUM_1:51
.=a * v+ a * w by A5,Th2;
end;
hence thesis;
end;
A6: for a,b be Real, v being VECTOR of REAL-NS n holds (a * b) * v
= a * (b * v)
proof
let a,b be Real;
reconsider a,b as Real;
let v be VECTOR of REAL-NS n;
(a * b) * v = a * (b * v)
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
A7: b * v = b * v1 by Th3;
(a * b) * v=(Euclid_mult n).(a * b,v) by Def4
.=(a * b) * v1 by Def2
.=a * (b * v2) by RVSUM_1:49;
hence thesis by A7,Th3;
end;
hence thesis;
end;
for v being VECTOR of REAL-NS n holds 1 * v = v
proof
let v be VECTOR of REAL-NS n;
thus 1 * v = v
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
thus 1 * v =(Euclid_mult n).(1,v) by Def4
.=1 * v2 by Def2
.=v by RVSUM_1:52;
end;
end;
hence REAL-NS n is vector-distributive scalar-distributive
scalar-associative scalar-unital
by A4,A2,A6;
for v,w being VECTOR of REAL-NS n holds v + w = w + v
proof
let v, w be VECTOR of REAL-NS n;
thus v + w = w + v
proof
reconsider v1 = v, w1 = w as Element of REAL n by Def4;
thus v+w = (Euclid_add n).(v,w) by Def4
.= (Euclid_add n).(w1,v1) by BINOP_1:def 2
.= w+v by Def4;
end;
end;
hence REAL-NS n is Abelian;
for u,v,w being VECTOR of REAL-NS n holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of REAL-NS n;
thus (u + v) + w = u + (v + w)
proof
reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def4;
A8: v + w =v1+w1 by Th2;
thus (u + v) + w =(Euclid_add n).((the addF of REAL-NS n).(u,v),w) by
Def4
.=(Euclid_add n).((Euclid_add n).(u1,v1), w1) by Def4
.=(Euclid_add n).(u1,(Euclid_add n).(v1,w1)) by BINOP_1:def 3
.=(Euclid_add n).(u1,v1+w1) by Def1
.= u1 + (v1 + w1) by Def1
.= u + (v + w) by A8,Th2;
end;
end;
hence REAL-NS n is add-associative;
for v being VECTOR of REAL-NS n holds v + 0.(REAL-NS n) = v
proof
let v be VECTOR of REAL-NS n;
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
reconsider zz = n|->In(0,REAL)
as Element of n-tuples_on REAL;
0.(REAL-NS n) = 0*n by Def4;
hence v + 0.(REAL-NS n) =v1 + 0*n by Th2
.= v2 + zz by EUCLID:def 4
.=v by RVSUM_1:16;
end;
hence REAL-NS n is right_zeroed;
REAL-NS n is right_complementable
proof
let v be VECTOR of REAL-NS n;
thus ex w being VECTOR of REAL-NS n st v + w = 0.(REAL-NS n)
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n-tuples_on REAL by EUCLID:def 1;
A9: 0.(REAL-NS n) = 0*n by Def4
.= n|->0 by EUCLID:def 4;
reconsider w=-v1 as VECTOR of REAL-NS n by Def4;
take w;
thus v + w =v2+(-v2) by Th2
.=0.(REAL-NS n) by A9,RVSUM_1:22;
end;
end;
hence thesis;
end;
end;
theorem Th4:
for x be VECTOR of REAL-NS n, a be Element of REAL n st x=a holds -x = -a
proof
let x be VECTOR of REAL-NS n;
let a be Element of REAL n;
assume
A1: x=a;
reconsider a1=a as Element of n-tuples_on REAL by EUCLID:def 1;
-x = (-1)*x by RLVECT_1:16
.=-a1 by A1,Th3;
hence thesis;
end;
theorem Th5:
for x,y be VECTOR of REAL-NS n, a,b be Element of REAL n st x=a &
y=b holds x-y = a - b
proof
let x,y be VECTOR of REAL-NS n;
let a,b be Element of REAL n;
assume that
A1: x=a and
A2: y=b;
-y = -b by A2,Th4;
hence thesis by A1,Th2;
end;
theorem Th6:
for f be FinSequence of REAL st dom f = Seg n holds f is Element of REAL n
proof
A1: n in NAT by ORDINAL1:def 12;
let f be FinSequence of REAL;
assume dom f= Seg n;
then len f = n by A1,FINSEQ_1:def 3;
then f is Element of n-tuples_on REAL by FINSEQ_2:92;
hence thesis by EUCLID:def 1;
end;
theorem Th7:
for n be Nat, x be Element of REAL n st (for i be
Nat st i in Seg n holds 0 <= x.i) holds 0 <= Sum x & for i be
Nat st i in Seg n holds x.i <= Sum x
proof
defpred P[Nat] means for x be Element of REAL $1 st (for i be
Nat st i in Seg $1 holds 0 <= x.i) holds 0 <= Sum x & (for i be
Nat st i in Seg $1 holds x.i <= Sum x);
A1: now
let k be Nat such that
A2: P[k];
now
let x be Element of REAL (k+1);
assume
A3: for i be Nat st i in Seg (k+1) holds 0 <= x.i;
thus 0 <= Sum x & for i be Nat st i in Seg (k+1) holds x.i <=
Sum x
proof
set xk= x|k;
A4: 0 <= x.(k+1) by A3,FINSEQ_1:4;
A5: k+1 = len x by CARD_1:def 7;
then len(x|k) = k by FINSEQ_1:59,NAT_1:11;
then
A6: xk is Element of k-tuples_on REAL by FINSEQ_2:92;
1 <= k+1 by NAT_1:11;
then k+1 in Seg len x by A5,FINSEQ_1:1;
then
A7: k+1 in dom x by FINSEQ_1:def 3;
reconsider xk as Element of REAL k by A6,EUCLID:def 1;
A8: xk = x|Seg k by FINSEQ_1:def 16;
x = x| (k+1) by A5,FINSEQ_1:58
.= x|Seg(k+1) by FINSEQ_1:def 16
.= xk^<* x.(k+1) *> by A7,A8,FINSEQ_5:10;
then
A9: Sum x=Sum xk + x.(k+1) by RVSUM_1:74;
A10: now
let i be Nat;
assume
A11: i in Seg k;
k <= k+1 by NAT_1:11;
then Seg k c= Seg(k+1) by FINSEQ_1:5;
then 0 <= x.i by A3,A11;
then 0 <= (x|Seg k).i by A11,FUNCT_1:49;
hence 0 <= xk.i by FINSEQ_1:def 16;
end;
A12: k+1 in Seg (k+1) by FINSEQ_1:4;
A13: now
let i be Nat;
assume
A14: i in Seg (k+1);
then
A15: 1 <= i by FINSEQ_1:1;
A16: i <=k+1 by A14,FINSEQ_1:1;
per cases by A16,XXREAL_0:1;
suppose
i < k+1;
then i <=k by NAT_1:13;
then
A17: i in Seg k by A15,FINSEQ_1:1;
then xk.i <= Sum xk by A2,A10;
then
A18: x.i <= Sum xk by A8,A17,FUNCT_1:49;
Sum xk <= Sum xk + x.(k+1) by A3,A12,XREAL_1:31;
hence x.i <=Sum x by A9,A18,XXREAL_0:2;
end;
suppose
i=k+1;
hence x.i <= Sum x by A2,A10,A9,XREAL_1:31;
end;
end;
0 <=Sum xk by A2,A10;
hence thesis by A4,A9,A13;
end;
end;
hence P[k+1];
end;
A19: P[0] by RVSUM_1:72;
thus for k be Nat holds P[k] from NAT_1:sch 2(A19,A1);
end;
theorem Th8:
for x be Element of REAL n, i be Nat st i in Seg n holds |.x.i.| <= |.x.|
proof
let x be Element of REAL n;
let i be Nat;
reconsider sx = sqr x as Element of REAL n by EUCLID:def 1;
A1: now
let k be Nat;
assume k in Seg n;
sx.k = (x.k)^2 by VALUED_1:11;
hence 0 <= sx.k by XREAL_1:63;
end;
A2: 0 <= |.x.i.|*|.x.i.| by XREAL_1:63;
|.x.i.| * |.x.i.| = (x.i)^2
proof
per cases by ABSVALUE:1;
suppose
|.x.i.| = x.i;
hence thesis;
end;
suppose
|.x.i.| = -(x.i);
hence thesis;
end;
end;
then
A3: (sqr x).i = |.x.i.|*|.x.i.| by VALUED_1:11;
assume i in Seg n;
then |.x.i.|*|.x.i.| <= Sum sqr x by A3,A1,Th7;
then
A4: sqrt (|.x.i.|*|.x.i.|) <= sqrt Sum sqr x by A2,SQUARE_1:26;
sqrt (|.x.i.|)^2 = |.x.i.| by COMPLEX1:46,SQUARE_1:22;
hence thesis by A4,EUCLID:def 5;
end;
theorem Th9:
for x be Point of REAL-NS n, y be Element of REAL n st x=y holds
for i be Nat st i in Seg n holds |.y.i.| <= ||.x.||
proof
let x be Point of REAL-NS n, y be Element of REAL n;
assume x=y;
then ||.x.|| = |.y.| by Th1;
hence thesis by Th8;
end;
theorem Th10:
for x be Element of REAL (n+1) holds |.x.|^2 = |.(x|n).|^2 + (x. (n+1))^2
proof
let x be Element of REAL (n+1);
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider x as Element of (n+1)-tuples_on REAL by EUCLID:def 1;
A1: x|n = x|Seg n by FINSEQ_1:def 16;
A2: n+1 = len x by CARD_1:def 7;
then n+1 in Seg len x by FINSEQ_1:4;
then
A3: n+1 in dom x by FINSEQ_1:def 3;
len (x|n) = n by A2,FINSEQ_1:59,NAT_1:11;
then reconsider xn = x|n as Element of n-tuples_on REAL by FINSEQ_2:92;
sqr x is Element of REAL (n+1) & for k be Nat st k in Seg (n+
1) holds 0 <= (sqr x).k
proof
thus sqr x is Element of REAL (n+1) by EUCLID:def 1;
let k be Nat;
assume k in Seg(n+1);
(sqr x).k = (x.k)^2 by VALUED_1:11
.= x.k * x.k;
hence thesis by XREAL_1:63;
end;
then |.x.| = sqrt Sum sqr x & 0 <= Sum sqr x by Th7,EUCLID:def 5;
then
A4: |.x.|^2 = Sum sqr x by SQUARE_1:def 2;
sqr (x|n) is Element of REAL n & for k be Nat st k in Seg n
holds 0 <= (sqr (x|n)).k
proof
sqr xn is Element of REAL n by EUCLID:def 1;
hence sqr(x|n) is Element of REAL n;
let k be Nat;
assume k in Seg n;
(sqr xn).k = (xn.k)^2 by VALUED_1:11
.= xn.k * xn.k;
hence thesis by XREAL_1:63;
end;
then |.(x|n).| = sqrt Sum sqr (x|n) & 0 <= Sum sqr (x|n) by Th7,EUCLID:def 5;
then
A5: |.(x|n).|^2 + (x.(n+1))^2 = Sum sqr (x|n) + (x.(n+1))^2 by SQUARE_1:def 2;
A6: x = x| (n+1) by A2,FINSEQ_1:58
.= x|Seg(n+1) by FINSEQ_1:def 16
.= (x|n)^<* x.(n+1) *> by A3,A1,FINSEQ_5:10;
(sqr(x|n))^<*(x.(n+1))^2*> = mlt(xn,xn)^<*(x.(n+1))*(x.(n+1))*>
.= mlt((xn)^<*x.(n+1)*>,(x|n)^<*x.(n+1)*>) by RFUNCT_4:2
.= sqr x by A6;
hence thesis by A4,A5,RVSUM_1:74;
end;
definition
let n be Nat;
let f be sequence of REAL n, k be Nat;
redefine func f.k -> Element of REAL n; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider k as Element of NAT by ORDINAL1:def 12;
f.k in REAL n;
hence thesis;
end;
end;
theorem Th11:
for n be Nat for x be Point of REAL-NS n, xs be
Element of REAL n, seq be sequence of REAL-NS n, xseq be sequence of REAL
n st xs = x & xseq = seq holds ( seq is convergent & lim seq = x iff
for i be Nat st i in Seg n ex rseqi be Real_Sequence st
for k be Nat
holds rseqi.k = (xseq.k).i & rseqi is convergent & xs.i = lim rseqi )
proof
defpred P[Nat] means
for x be Point of REAL-NS $1, xs be Element of REAL $1,
seq be sequence of REAL-NS $1, xseq be sequence of REAL $1 st
xs= x & xseq=seq
holds ((seq is convergent & lim seq = x) iff
(for i be Nat st i in Seg $1 ex rseqi be Real_Sequence st for k be Nat
holds rseqi.k = (xseq.k).i & rseqi is convergent & xs.i= lim rseqi));
A1: now
let n be Nat;
assume
A2: P[n];
now
let x be Point of REAL-NS (n+1), xs be Element of REAL (n+1), seq be
sequence of REAL-NS (n+1), xseq be sequence of REAL (n+1);
assume
A3: xs= x & xseq=seq;
A4: now
assume
A5: for i be Nat st i in Seg (n+1) ex rseqi be
Real_Sequence st for k be Nat holds rseqi.k = (xseq.k).i & rseqi is
convergent & xs.i= lim rseqi;
thus seq is convergent & lim seq = x
proof
len xs= n+1 by CARD_1:def 7;
then len (xs|n) = n by FINSEQ_1:59,NAT_1:11;
then dom(xs|n) = Seg n by FINSEQ_1:def 3;
then reconsider xsn=xs|n as Element of REAL n by Th6;
reconsider xn=xsn as Point of REAL-NS n by Def4;
defpred P1[Nat,Element of REAL n] means $2=(xseq.$1) |n;
set seq2 = ||.seq - x.|| (#) ||.seq - x.||;
consider rseqn1 be Real_Sequence such that
A6: for k be Nat holds rseqn1.k = (xseq.k).(n+1) &
rseqn1 is convergent & xs.(n+1)= lim rseqn1 by A5,FINSEQ_1:4;
A7: for i be Element of NAT ex y be Element of REAL n st P1[i ,y]
proof
let i be Element of NAT;
take y=(xseq.i) |n;
len (xseq.i)= n+1 by CARD_1:def 7;
then len (xseq.i|n) = n by FINSEQ_1:59,NAT_1:11;
then dom(xseq.i|n) = Seg n by FINSEQ_1:def 3;
hence thesis by Th6;
end;
consider xseqn be sequence of REAL n such that
A8: for i be Element of NAT holds P1[i,xseqn.i] from FUNCT_2:sch 3(A7);
reconsider seqn=xseqn as sequence of REAL-NS n by Def4;
set seqn2 = ||.seqn - xn.|| (#) ||.seqn - xn.||;
deffunc F(Nat)=|.rseqn1.$1 -xs.(n+1).|;
consider absrseq be Real_Sequence such that
A9: for i be Nat holds absrseq.i =F(i) from SEQ_1:
sch 1;
A10: for i be Nat st i in Seg n ex rseqi be Real_Sequence
st for k be Nat holds rseqi.k = (xseqn.k).i & rseqi is convergent &
xsn.i= lim rseqi
proof
let i be Nat such that
A11: i in Seg n;
n <= n+1 by NAT_1:11;
then Seg n c= Seg (n+1) by FINSEQ_1:5;
then consider rseqi be Real_Sequence such that
A12: for k be Nat holds rseqi.k = (xseq.k).i &
rseqi is convergent & xs.i= lim rseqi by A5,A11;
A13: now
let k be Nat;
A14: k in NAT by ORDINAL1:def 12;
thus rseqi.k=(xseq.k).i by A12
.=((xseq.k) |Seg n).i by A11,FUNCT_1:49
.=((xseq.k) |n).i by FINSEQ_1:def 16
.=(xseqn.k).i by A8,A14;
end;
xsn.i = (xs|Seg n).i by FINSEQ_1:def 16
.=xs.i by A11,FUNCT_1:49;
hence thesis by A12,A13;
end;
then
A15: xn=lim seqn by A2;
set rseqn2 =absrseq (#) absrseq;
xsn= xn;
then
A16: seqn is convergent by A2,A10;
then
A17: ||.seqn - xn.|| is convergent by A15,NORMSP_1:24;
then
A18: seqn2 is convergent by SEQ_2:14;
now
reconsider rxs= xs as Element of (n+1)-tuples_on REAL by
EUCLID:def 1;
let k be Nat;
A19: k in NAT by ORDINAL1:def 12;
A20: ||.seq - x.||.k = ||.(seq - x).k.|| by NORMSP_0:def 4
.= ||.seq.k - x.|| by NORMSP_1:def 4;
reconsider rxseqk= (xseq.k) as Element of (n+1)-tuples_on REAL by
EUCLID:def 1;
A21: ||.seqn - xn.||.k = ||.(seqn - xn).k.|| by NORMSP_0:def 4
.= ||.seqn.k - xn.|| by NORMSP_1:def 4;
len (xseqn.k -xsn) = n by CARD_1:def 7;
then
A22: dom(xseqn.k -xsn) = Seg n by FINSEQ_1:def 3;
A23: (xseq.k-xs).(n+1) = rxseqk.(n+1)-rxs.(n+1) by RVSUM_1:27
.= rseqn1.k - xs.(n+1) by A6;
len (xseq.k-xs) = n+1 by CARD_1:def 7;
then
A24: len ((xseq.k-xs) |n) = n by FINSEQ_1:59,NAT_1:11;
A25: now
reconsider xseq2 = xseqn.k, xs2 = xsn as Element of n-tuples_on
REAL by EUCLID:def 1;
reconsider xseq1 = xseq.k, xs1 = xs as Element of (n+1)
-tuples_on REAL by EUCLID:def 1;
let i be Nat;
assume i in dom ((xseq.k-xs) |n);
then
A26: i in Seg n by A24,FINSEQ_1:def 3;
A27: (xseqn.k-xsn).i = xseq2.i-xs2.i by RVSUM_1:27;
A28: (xseq.k-xs).i = xseq1.i-xs1.i by RVSUM_1:27;
thus ((xseq.k-xs) |n).i =((xseq.k-xs) |Seg n).i
by FINSEQ_1:def 16
.= (xseq.k-xs).i by A26,FUNCT_1:49
.= ((xseq.k) |Seg n).i - xs.i by A26,A28,FUNCT_1:49
.= ((xseq.k) |Seg n).i - (xs|Seg n).i by A26,FUNCT_1:49
.= ((xseq.k) |n).i- (xs|Seg n).i by FINSEQ_1:def 16
.= ((xseq.k) |n).i-(xs|n).i by FINSEQ_1:def 16
.= (xseqn.k -xsn).i by A8,A27,A19;
end;
dom ((xseq.k-xs) |n) = Seg n by A24,FINSEQ_1:def 3;
then
A29: (xseq.k-xs) |n=xseqn.k -xsn by A22,A25,FINSEQ_1:13;
A30: 0<= (rseqn1.k - xs.(n+1))^2 by XREAL_1:63;
A31: absrseq.k = |.rseqn1.k - xs.(n+1).| by A9;
||.seq.k - x.|| = |.xseq.k-xs .| by A3,Th1,Th5;
hence seq2.k = |.xseq.k-xs .|^2 by A20,SEQ_1:8
.= |.xseqn.k-xsn .|^2 +(rseqn1.k - xs.(n+1))^2 by A23,A29,Th10
.= ||. seqn.k-xn .||^2 +(rseqn1.k - xs.(n+1))^2 by Th1,Th5
.= ( ||.seqn - xn.|| (#) ||.seqn - xn.||).k + (rseqn1.k - xs.(
n+1))^2 by A21,SEQ_1:8
.= seqn2.k + |.(rseqn1.k - xs.(n+1))*(rseqn1.k - xs.(n+1)).|
by A30,ABSVALUE:def 1
.= seqn2.k + |.rseqn1.k - xs.(n+1).| *|.rseqn1.k - xs.(n+1)
.| by COMPLEX1:65
.= seqn2.k + rseqn2.k by A31,SEQ_1:8;
end;
then
A32: seq2=seqn2+rseqn2 by SEQ_1:7;
A33: now
let e be Real;
assume e > 0;
then consider m be Nat such that
A34: for k be Nat st m <= k holds |.rseqn1.k -xs.
(n+1).| < e by A6,SEQ_2:def 7;
now
let k be Nat;
assume m <= k;
then |.|.rseqn1.k -xs.(n+1).|-0 .| < e by A34;
hence |.absrseq.k-0 .| < e by A9;
end;
hence ex m be Nat st for k be Nat st m <= k
holds |.absrseq.k-0 .| < e;
end;
then
A35: absrseq is convergent by SEQ_2:def 6;
then lim absrseq = 0 by A33,SEQ_2:def 7;
then
A36: lim rseqn2 = 0 * 0 by A35,SEQ_2:15
.=0;
A37: rseqn2 is convergent by A35,SEQ_2:14;
then
A38: seq2 is convergent by A18,A32,SEQ_2:5;
lim ||.seqn - xn.|| = 0 by A16,A15,NORMSP_1:24;
then lim seqn2 = 0 * 0 by A17,SEQ_2:15
.= 0;
then
A39: lim seq2 = 0+ 0 by A18,A37,A36,A32,SEQ_2:6
.= 0;
A40: for e be Real st e > 0 ex m be Nat st for k be
Nat st k >= m holds ||.seq.k - x.|| < e
proof
let e be Real such that
A41: e > 0;
e*0 < e*e by A41,XREAL_1:97;
then consider m be Nat such that
A42: for k be Nat st m<=k holds |.seq2.k-0 .| < e*e
by A38,A39,SEQ_2:def 7;
now
let k be Nat such that
A43: m<= k;
||.seq - x.||.k = ||.(seq - x).k.|| by NORMSP_0:def 4
.= ||.seq.k - x.|| by NORMSP_1:def 4;
then seq2.k = ( ||.seq.k - x.|| )*( ||.seq.k - x.|| ) by SEQ_1:8;
then
|.seq2.k-0 .| = ||.seq.k - x.|| * ||.seq.k - x.|| by ABSVALUE:def 1;
then
A44: ||.seq.k - x.|| * ||.seq.k - x.|| < e*e by A42,A43;
A45: sqrt( ||.seq.k - x.|| * ||.seq.k - x.|| ) = sqrt( ||.seq.k
- x.||^2)
.= ||.seq.k - x.|| by SQUARE_1:22;
sqrt(e*e) = sqrt(e^2) .= e by A41,SQUARE_1:22;
hence ||.seq.k - x.|| < e by A44,A45,SQUARE_1:27;
end;
hence thesis;
end;
then seq is convergent by NORMSP_1:def 6;
hence thesis by A40,NORMSP_1:def 7;
end;
end;
now
assume
A46: seq is convergent & lim seq = x;
now
let i be Nat such that
A47: i in Seg (n+1);
deffunc F(Nat) = (xseq.$1).i;
consider rseqi be Real_Sequence such that
A48: for l be Nat holds rseqi.l = F(l) from SEQ_1:sch
1;
A49: now
let e be Real such that
A50: e > 0;
thus ex k be Nat st for m be Nat st k<=m
holds |.rseqi.m-xs.i.| < e
proof
consider k be Nat such that
A51: for m be Nat st m >= k holds ||.(seq.m) - x
.|| < e by A46,A50,NORMSP_1:def 7;
take k;
let m be Nat;
assume k<=m;
then
A52: ||.(seq.m) - x.|| < e by A51;
len ((xseq.m) - xs) = (n+1) by CARD_1:def 7;
then i in dom ((xseq.m) - xs) by A47,FINSEQ_1:def 3;
then (xseq.m).i-xs.i = ((xseq.m) - xs).i by VALUED_1:13;
then
A53: |.(xseq.m).i-xs.i.| <= ||.(seq.m) - x.|| by A3,A47,Th5,Th9;
rseqi.m-xs.i=(xseq.m).i-xs.i by A48;
hence thesis by A52,A53,XXREAL_0:2;
end;
end;
then
A54: rseqi is convergent by SEQ_2:def 6;
then xs.i= lim rseqi by A49,SEQ_2:def 7;
hence ex rseqi be Real_Sequence st for k be Nat holds
rseqi.k = (xseq.k).i & rseqi is convergent & xs.i= lim rseqi by A48,A54;
end;
hence for i be Nat st i in Seg (n+1) ex rseqi be
Real_Sequence st for k be Nat holds rseqi.k = (xseq.k).i & rseqi is
convergent & xs.i= lim rseqi;
end;
hence
seq is convergent & lim seq = x iff for i be Nat st i in
Seg (n+1) ex rseqi be Real_Sequence st for k be Nat holds rseqi.k =
(xseq.k).i & rseqi is convergent & xs.i= lim rseqi by A4;
end;
hence P[n+1];
end;
A55: P[0]
proof
let x be Point of REAL-NS 0, xs be Element of REAL 0, seq be sequence of
REAL-NS 0, xseq be sequence of REAL 0;
assume that
A56: xs= x and
A57: xseq=seq;
now
assume for i be Nat st i in Seg 0 ex rseqi be Real_Sequence st
for k be Nat holds rseqi.k = (xseq.k).i & rseqi is convergent & xs.i
= lim rseqi;
A58: for i be Nat holds seq.i=0.(REAL-NS 0)
proof
let i be Nat;
xseq.i = 0.REAL 0;
hence thesis by A57,Def4;
end;
xs = 0*0;
then
A59: x=0.(REAL-NS 0) by A56,Def4;
A60: for r be Real st 0 < r ex m be Nat st
for k be Nat st m <= k holds ||. seq.k - x .|| < r
proof
let r be Real;
assume
A61: 0 < r;
take m = 1;
let k be Nat;
assume m <= k;
||. seq.k - x .|| = ||. 0.(REAL-NS 0) - 0.(REAL-NS 0) .|| by A59,A58
.= ||. 0.(REAL-NS 0) .|| by RLVECT_1:15
.= 0;
hence thesis by A61;
end;
then seq is convergent by NORMSP_1:def 6;
hence seq is convergent & lim seq = x by A60,NORMSP_1:def 7;
end;
hence thesis;
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(A55,A1);
end;
theorem Th12:
for f be sequence of REAL-NS n st f is Cauchy_sequence_by_Norm
holds f is convergent
proof
let vseq be sequence of REAL-NS n such that
A1: vseq is Cauchy_sequence_by_Norm;
reconsider xvseq=vseq as sequence of REAL n by Def4;
defpred P[set, set] means ex rseqi be Real_Sequence st
for l be Nat holds rseqi.l = (xvseq.l).$1 & rseqi is convergent &
$2 = lim rseqi;
A2: for i be Nat st i in Seg n ex y be Element of REAL st P[i,y]
proof
let i be Nat such that
A3: i in Seg n;
deffunc F(Nat) = (xvseq.$1).i;
consider rseqi be Real_Sequence such that
A4: for l be Nat holds rseqi.l = F(l) from SEQ_1:sch 1;
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr;
now
let e be Real such that
A5: e > 0;
thus ex k be Nat st for m be Nat st k<=m holds
|.rseqi.m -rseqi.k.| < e
proof
consider k be Nat such that
A6: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n
) - (vseq.m).|| < e by A1,A5,RSSPACE3:8;
take k;
let m be Nat;
assume k<=m;
then
A7: ||.(vseq.m) - (vseq.k).|| < e by A6;
len ((xvseq.m) - (xvseq.k)) =n by CARD_1:def 7;
then i in dom ((xvseq.m) - (xvseq.k)) by A3,FINSEQ_1:def 3;
then (xvseq.m).i-(xvseq.k).i = ((xvseq.m) - (xvseq.k)).i by VALUED_1:13
;
then
A8: |.(xvseq.m).i-(xvseq.k).i.| <= ||.(vseq.m) - (vseq.k).|| by A3,Th5,Th9;
rseqi.m=(xvseq.m).i & rseqi.k=(xvseq.k).i by A4;
hence thesis by A7,A8,XXREAL_0:2;
end;
end;
then rseqi is convergent by SEQ_4:41;
hence thesis by A4;
end;
consider f be FinSequence of REAL such that
A9: dom f = Seg n & for k be Nat st k in Seg n holds P[k,f.k] from
FINSEQ_1:sch 5(A2);
reconsider tseq=f as Element of REAL n by A9,Th6;
reconsider xseq=tseq as Point of REAL-NS n by Def4;
A10: xseq=tseq;
for k be Nat st k in Seg n holds P[k,f.k] by A9;
hence thesis by A10,Th11;
end;
Lm2: REAL-NS n is RealBanachSpace
proof
for seq be sequence of REAL-NS n st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th12;
hence thesis by LOPBAN_1:def 15;
end;
registration
let n;
cluster REAL-NS n -> complete;
coherence by Lm2;
end;
begin :: R^n space as RealNormSpace
definition
let n be Nat;
func Euclid_scalar n -> Function of [:REAL n,REAL n:],REAL means
:Def5:
for x,y being Element of REAL n holds it.(x,y) = Sum mlt(x,y);
existence
proof
deffunc F(Element of REAL n,Element of REAL n)
= In(Sum mlt($1,$2),REAL);
consider f be Function of [:REAL n, REAL n:], REAL such that
A1: for x,y be Element of REAL n
holds f.(x,y) = F(x,y) from BINOP_1:sch 4;
take f;
let x,y be Element of REAL n;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
uniqueness
proof
let scalar1,scalar2 be Function of [: REAL n, REAL n :], REAL such that
A2: for x,y be Element of REAL n holds scalar1.(x,y) = Sum mlt(x,y) and
A3: for x,y be Element of REAL n holds scalar2.(x,y) = Sum mlt(x,y);
for x,y be Element of REAL n holds scalar1.(x,y) = scalar2.(x,y)
proof
let x,y be Element of REAL n;
scalar1.(x,y) = Sum mlt(x,y) by A2;
hence thesis by A3;
end;
hence thesis;
end;
end;
definition
let n be Nat;
func REAL-US n -> strict non empty UNITSTR means
:Def6:
the carrier of it =
REAL n & 0.it = 0*n & the addF of it = Euclid_add n & the Mult of it =
Euclid_mult n & the scalar of it = Euclid_scalar n;
existence
proof
take UNITSTR(#REAL n, 0*n, Euclid_add n, Euclid_mult n, Euclid_scalar n#);
thus thesis;
end;
uniqueness;
end;
registration
let n be non zero Nat;
cluster REAL-US n -> non trivial;
coherence
proof
the carrier of REAL-US n = REAL n by Def6
.= the carrier of TOP-REAL n by EUCLID:22;
hence thesis;
end;
end;
registration
let n be Nat;
cluster REAL-US n -> RealUnitarySpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable;
coherence
proof
now
let x,y,z be Point of REAL-US n, a be Real;
reconsider x1=x, y1=y, z1=z as Element of REAL n by Def6;
reconsider x2=x1, y2=y1, z2=z1 as Element of n-tuples_on REAL by
EUCLID:def 1;
A1: len x2 = n & len y2 = n by CARD_1:def 7;
A2: for k be Nat st k in dom mlt(x1,x1) holds 0 <= mlt(x1,x1).k
proof
let k be Nat;
assume k in dom mlt(x1,x1);
mlt(x1,x1).k = x1.k * x1.k by RVSUM_1:59;
hence thesis by XREAL_1:63;
end;
A3: x .|. x = (Euclid_scalar n).(x,x) by Def6
.= Sum mlt(x1,x1) by Def5;
hence 0 <= x .|. x by A2,RVSUM_1:84;
thus x .|. x = 0 iff x = 0.(REAL-US n)
proof
now
assume that
A4: x .|. x = 0 and
A5: x <> 0.(REAL-US n);
for k be Element of NAT st k in dom x2 holds x2.k = 0
proof
let k be Element of NAT;
dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
then [:rng x1, rng x1:] c= dom multreal by ZFMISC_1:96;
then
A6: dom(multreal.:(x1,x1)) = dom x1 /\ dom x1 by FUNCOP_1:69;
assume k in dom x2;
then
A7: k in dom mlt(x1,x1) by A6,RVSUM_1:def 9;
then 0 <= mlt(x1,x1).k by A2;
then mlt(x1,x1).k = 0 by A3,A2,A4,A7,RVSUM_1:85;
then (x1.k)^2 = 0 by RVSUM_1:59;
hence thesis by SQUARE_1:12;
end;
then x1 = n |-> (0 qua Real) by RFUNCT_4:4;
then x = 0*n by EUCLID:def 4;
hence contradiction by A5,Def6;
end;
hence x .|. x = 0 implies x = 0.(REAL-US n);
assume x = 0.(REAL-US n);
then x = 0*n by Def6
.= n |-> (0 qua Real) by EUCLID:def 4;
then mlt(x2,x2) = 0 * x2 by RVSUM_1:63
.= n |-> 0 by RVSUM_1:53;
hence thesis by A3,RVSUM_1:81;
end;
A8: len z2 = n by CARD_1:def 7;
thus x .|. y = (Euclid_scalar n).(x,y) by Def6
.= Sum mlt(y1,x1) by Def5
.= (Euclid_scalar n).(y,x) by Def5
.= y .|. x by Def6;
A9: x .|. z = (Euclid_scalar n).(x,z) by Def6
.= Sum mlt(x1,z1) by Def5;
a*x is Element of REAL n by Def6;
then reconsider ax = a*x as Element of n-tuples_on REAL by EUCLID:def 1;
A10: for k be Nat st k in Seg n holds (ax).k = (a*x1).k
proof
reconsider a as Real;
let k be Nat;
assume k in Seg n;
a*x = (Euclid_mult n).(a,x1) by Def6
.= a*x1 by Def2;
hence thesis;
end;
A11: y .|. z = (Euclid_scalar n).(y,z) by Def6
.= Sum mlt(y1,z1) by Def5;
thus (x+y) .|. z = (Euclid_scalar n).(x+y,z) by Def6
.= (Euclid_scalar n).((Euclid_add n).(x1,y1),z1) by Def6
.= (Euclid_scalar n).(x1+y1,z1) by Def1
.= Sum mlt(x1+y1,z1) by Def5
.= Sum ( mlt(x1,z1)+mlt(y1,z1) ) by A1,A8,RVSUM_1:118
.= Sum mlt(x2,z2) + Sum mlt(y2,z2) by RVSUM_1:89
.= x .|. z + y .|. z by A9,A11;
thus (a*x) .|. y = (Euclid_scalar n).(a*x,y) by Def6
.= (Euclid_scalar n).(a*x1,y1) by A10,FINSEQ_2:119
.= Sum mlt(a*x1,y1) by Def5
.= Sum (a*mlt(x2,y2)) by RVSUM_1:65
.= a * Sum mlt(x2,y2) by RVSUM_1:87
.= a * (Euclid_scalar n).(x1,y1) by Def5
.= a * ( x .|. y ) by Def6;
end;
hence REAL-US n is RealUnitarySpace-like;
A12: for a,b be Real for v be VECTOR of REAL-US n holds (a * b) * v
= a * (b * v)
proof
let a,b be Real;
let v be VECTOR of REAL-US n;
reconsider v1=v as Element of REAL n by Def6;
reconsider a,b as Real;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
b*v is Element of REAL n by Def6;
then reconsider bv = b*v as Element of n-tuples_on REAL by EUCLID:def 1;
for k be Nat st k in Seg n holds bv.k = (b*v1).k
proof
reconsider b as Element of REAL by XREAL_0:def 1;
let k be Nat;
assume k in Seg n;
b*v = (Euclid_mult n).(b,v1) by Def6
.= b*v1 by Def2;
hence thesis;
end;
then b*v1 = b*v by FINSEQ_2:119;
then
A13: a*(b*v) = (Euclid_mult n).(a,b*v1) by Def6
.= a*(b*v2) by Def2;
(a*b)*v = (Euclid_mult n).(a*b,v1) by Def6
.= (a*b)*v2 by Def2
.= a*(b*v2) by RVSUM_1:49;
hence thesis by A13;
end;
A14: for a be Real for v,w be VECTOR of REAL-US n holds a * (v + w)
= a * v + a * w
proof
let a be Real;
let v,w be VECTOR of REAL-US n;
reconsider v1=v, w1=w as Element of REAL n by Def6;
reconsider a as Real;
reconsider v2=v1, w2=w1 as Element of n-tuples_on REAL by EUCLID:def 1;
a*v is Element of REAL n by Def6;
then reconsider av = a*v as Element of n-tuples_on REAL by EUCLID:def 1;
A15: for k be Nat st k in Seg n holds av.k = (a*v1).k
proof
let k be Nat;
assume k in Seg n;
a*v = (Euclid_mult n).(a,v1) by Def6
.= a*v1 by Def2;
hence thesis;
end;
a*w is Element of REAL n by Def6;
then reconsider aw = a*w as Element of n-tuples_on REAL by EUCLID:def 1;
for k be Nat st k in Seg n holds aw.k = (a*w1).k
proof
reconsider a as Element of REAL by XREAL_0:def 1;
let k be Nat;
assume k in Seg n;
a*w = (Euclid_mult n).(a,w1) by Def6
.= a*w1 by Def2;
hence thesis;
end;
then A16: a*v1 is Element of n-tuples_on REAL & a*w1 = a*w by EUCLID:def 1
,FINSEQ_2:119;
A17: a*v + a*w = (Euclid_add n).(a*v,a*w) by Def6
.= (Euclid_add n).(a*v1,a*w1) by A15,A16,FINSEQ_2:119
.= a*v2 + a*w2 by Def1;
a * (v + w) = (Euclid_mult n).(a,v+w) by Def6
.= (Euclid_mult n).(a,(Euclid_add n).(v1,w1)) by Def6
.= (Euclid_mult n).(a,v1+w1) by Def1
.= a*(v1+w1) by Def2
.= a*v2 + a*w2 by RVSUM_1:51;
hence thesis by A17;
end;
A18: for a,b be Real for v be VECTOR of REAL-US n holds (a + b) * v
= a * v + b * v
proof
let a,b be Real;
let v be VECTOR of REAL-US n;
reconsider v1=v as Element of REAL n by Def6;
reconsider a,b as Real;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
A19: (a+b)*v = (Euclid_mult n).(a+b,v1) by Def6
.= (a+b)*v2 by Def2
.= a*v1 + b*v1 by RVSUM_1:50;
a*v is Element of REAL n by Def6;
then reconsider av = a*v as Element of n-tuples_on REAL by EUCLID:def 1;
A20: for k be Nat st k in Seg n holds av.k = (a*v1).k
proof
reconsider a as Element of REAL by XREAL_0:def 1;
let k be Nat;
assume k in Seg n;
a*v = (Euclid_mult n).(a,v1) by Def6
.= a*v1 by Def2;
hence thesis;
end;
b*v is Element of REAL n by Def6;
then reconsider bv = b*v as Element of n-tuples_on REAL by EUCLID:def 1;
for k be Nat st k in Seg n holds bv.k = (b*v1).k
proof
reconsider b as Element of REAL by XREAL_0:def 1;
let k be Nat;
assume k in Seg n;
b*v = (Euclid_mult n).(b,v1) by Def6
.= b*v1 by Def2;
hence thesis;
end;
then A21: a*v1 is Element of n-tuples_on REAL & b*v1 = b*v by EUCLID:def 1
,FINSEQ_2:119;
a*v + b*v = (Euclid_add n).(a*v,b*v) by Def6
.= (Euclid_add n).(a*v1,b*v1) by A20,A21,FINSEQ_2:119
.= a*v2 + b*v2 by Def1;
hence thesis by A19;
end;
for v being VECTOR of REAL-US n holds 1 * v = v
proof
let v be VECTOR of REAL-US n;
reconsider v1=v as Element of REAL n by Def6;
reconsider v2=v1 as Element of n-tuples_on REAL by EUCLID:def 1;
1 * v = (Euclid_mult n).(1,v1) by Def6
.= 1 * v2 by Def2
.= v2 by RVSUM_1:52;
hence thesis;
end;
hence REAL-US n is vector-distributive scalar-distributive
scalar-associative scalar-unital
by A14,A18,A12;
thus REAL-US n is Abelian
proof
let v,w be VECTOR of REAL-US n;
reconsider v1 = v, w1 = w as Element of REAL n by Def6;
thus v + w = (Euclid_add n).(v,w) by Def6
.= (Euclid_add n).(w1,v1) by BINOP_1:def 2
.= w + v by Def6;
end;
for u,v,w being Element of REAL-US n holds (u + v) + w = u + (v + w)
proof
let u,v,w be Element of REAL-US n;
reconsider u1=u, v1=v, w1=w as Element of REAL n by Def6;
reconsider u2=u1, v2=v1, w2=w1 as Element of n-tuples_on REAL by
EUCLID:def 1;
A22: u + (v + w) = (Euclid_add n).(u1,v+w) by Def6
.= (Euclid_add n).(u2,(Euclid_add n).(v2,w2)) by Def6
.= (Euclid_add n).(u2,v1+w1) by Def1;
(u + v) + w = (Euclid_add n).(u+v,w1) by Def6
.= (Euclid_add n).((Euclid_add n).(u1,v1),w1) by Def6
.= (Euclid_add n).(u1+v1,w1) by Def1
.= (u1+v1)+w2 by Def1
.= u2+(v2+w2) by RVSUM_1:15;
hence thesis by A22,Def1;
end;
hence REAL-US n is add-associative;
for v being Element of REAL-US n holds v + 0.(REAL-US n) = v
proof
let v be Element of REAL-US n;
reconsider v1=v as Element of REAL n by Def6;
v + 0.(REAL-US n) = (Euclid_add n).(v,0.(REAL-US n)) by Def6
.= (Euclid_add n).(v1,0*n) by Def6
.= v1 + 0*n by Def1;
hence thesis by EUCLID_4:1;
end;
hence REAL-US n is right_zeroed;
let v be Element of REAL-US n;
reconsider v1=v as Element of REAL n by Def6;
reconsider w = -v1 as Element of REAL-US n by Def6;
take w;
thus v + w = (Euclid_add n).(v1,-v1) by Def6
.= v1 + -v1 by Def1
.= 0*n by EUCLIDLP:2
.= 0.(REAL-US n) by Def6;
end;
end;
theorem Th13:
for n be Nat, a be Real, x1,y1 be Point of REAL-NS n,
x2,y2 be Point of REAL-US n st x1 = x2 & y1 = y2 holds x1 + y1 = x2 + y2 & -x1
= -x2 & a * x1 = a * x2
proof
let n be Nat, a be Real;
let x1,y1 be Point of REAL-NS n;
reconsider x=x1, y=y1 as Element of REAL n by Def4;
let x2,y2 be Point of REAL-US n;
assume that
A1: x1 = x2 and
A2: y1 = y2;
thus x1 + y1 = (Euclid_add n).(x,y) by Def4
.= x2 + y2 by A1,A2,Def6;
thus -x1 = (-1)*x1 by RLVECT_1:16
.= (Euclid_mult n).(-1,x) by Def4
.= (-1)*x2 by A1,Def6
.= -x2 by RLVECT_1:16;
thus a * x1 = (Euclid_mult n).(a,x) by Def4
.= a*x2 by A1,Def6;
end;
theorem
for n be Nat, x1 be Point of REAL-NS n, x2 be Point of
REAL-US n st x1 = x2 holds ||.x1.||^2 = x2 .|. x2
proof
let n be Nat, x1 be Point of REAL-NS n, x2 be Point of REAL-US n;
reconsider x=x1 as Element of REAL n by Def4;
assume
A1: x1 = x2;
thus ||.x1.||^2 = |.x.|^2 by Th1
.= |(x,x)| by EUCLID_2:4
.= Sum mlt(x,x) by RVSUM_1:def 16
.= (Euclid_scalar n).(x,x) by Def5
.= x2 .|. x2 by A1,Def6;
end;
theorem Th15:
for n be Nat, f be set holds f is sequence of REAL-NS
n iff f is sequence of REAL-US n
proof
let n be Nat, f be set;
the carrier of REAL-NS n = REAL n by Def4
.= the carrier of REAL-US n by Def6;
hence thesis;
end;
theorem Th16:
for n be Nat, seq1 be sequence of REAL-NS n, seq2 be
sequence of REAL-US n st seq1 = seq2 holds (seq1 is convergent implies seq2 is
convergent & lim seq1 = lim seq2) & (seq2 is convergent implies seq1 is
convergent & lim seq1 = lim seq2)
proof
let n be Nat;
let seq1 be sequence of REAL-NS n;
let seq2 be sequence of REAL-US n;
assume
A1: seq1 = seq2;
A2: the carrier of REAL-NS n = REAL n by Def4
.= the carrier of REAL-US n by Def6;
now
reconsider LIMIT = lim seq1 as Point of REAL-US n by A2;
assume
A3: seq1 is convergent;
then consider RNg be Point of REAL-NS n such that
A4: for r be Real st 0 < r ex m be Nat st
for k be Nat st m <= k holds ||.(seq1.k) - RNg.|| < r by NORMSP_1:def 6;
reconsider RUg = RNg as Point of REAL-US n by A2;
for r be Real st 0 < r
ex m be Nat st for k be Nat st m <= k holds dist(seq2.k, RUg) < r
proof
let r be Real;
assume 0 < r;
then consider m be Nat such that
A5: for k be Nat st m <= k holds ||.(seq1.k) - RNg.|| < r by A4;
take m;
let k be Nat;
reconsider p = seq1.k - RNg as Element of REAL n by Def4;
assume
A6: m <= k;
-RNg = -RUg by Th13;
then
A7: p = seq2.k - RUg by A1,Th13;
||.(seq1.k) - RNg.|| = |.p.| by Th1
.= sqrt |(p,p)| by EUCLID_2:5
.= sqrt Sum mlt(p,p) by RVSUM_1:def 16
.= sqrt ((Euclid_scalar n).(p,p)) by Def5
.= ||. seq2.k - RUg .|| by A7,Def6;
hence thesis by A5,A6;
end;
hence
A8: seq2 is convergent by BHSP_2:def 1;
for r be Real st r > 0
ex m be Nat st for k be Nat st k >= m holds dist((seq2.k), LIMIT) < r
proof
let r be Real;
assume r > 0;
then consider m be Nat such that
A9: for k be Nat st m <= k holds ||.(seq1.k) - lim seq1
.|| < r by A3,NORMSP_1:def 7;
take m;
let k be Nat;
reconsider p = seq1.k - lim seq1 as Element of REAL n by Def4;
assume
A10: m <= k;
-lim seq1 = -LIMIT by Th13;
then
A11: p = seq2.k - LIMIT by A1,Th13;
||.(seq1.k) - lim seq1.|| = |.p.| by Th1
.= sqrt |(p,p)| by EUCLID_2:5
.= sqrt Sum mlt(p,p) by RVSUM_1:def 16
.= sqrt ((Euclid_scalar n).(p,p)) by Def5
.= ||. seq2.k-LIMIT .|| by A11,Def6;
hence thesis by A9,A10;
end;
hence lim seq2 = lim seq1 by A8,BHSP_2:def 2;
end;
hence seq1 is convergent implies seq2 is convergent & lim seq1 = lim seq2;
now
reconsider LIMIT = lim seq2 as Point of REAL-NS n by A2;
assume
A12: seq2 is convergent;
then consider RUg be Point of REAL-US n such that
A13: for r be Real st 0 < r ex m be Nat st
for k be Nat st m <= k holds dist(seq2.k, RUg) < r by BHSP_2:def 1;
reconsider RNg = RUg as Point of REAL-NS n by A2;
for r be Real st 0 < r
ex m be Nat st
for k be Nat st m <= k holds ||.(seq1.k)-RNg.|| < r
proof
let r be Real;
assume 0 < r;
then consider m be Nat such that
A14: for k be Nat st m <= k holds dist(seq2.k, RUg) < r by A13;
take m;
for k be Nat st m <= k holds ||.(seq1.k)-RNg.|| < r
proof
let k be Nat;
reconsider p = seq2.k - RUg as Element of REAL n by Def6;
assume m <= k;
then
A15: dist(seq2.k,RUg) < r by A14;
-RNg = -RUg by Th13;
then
A16: p = seq1.k - RNg by A1,Th13;
dist(seq2.k, RUg) = sqrt ((Euclid_scalar n).(p,p)) by Def6
.= sqrt Sum mlt(p,p) by Def5
.= sqrt |(p,p)| by RVSUM_1:def 16
.= |.p.| by EUCLID_2:5;
hence thesis by A15,A16,Th1;
end;
hence thesis;
end;
hence
A17: seq1 is convergent by NORMSP_1:def 6;
for r be Real st r > 0
ex m be Nat st
for k be Nat st k >= m holds ||.(seq1.k)-LIMIT.|| < r
proof
let r be Real;
assume r > 0;
then consider m be Nat such that
A18: for k be Nat st k >= m holds dist((seq2.k), lim seq2
) < r by A12,BHSP_2:def 2;
take m;
let k be Nat;
assume k >= m;
then
A19: dist(seq2.k,lim seq2) < r by A18;
reconsider p = seq2.k - lim seq2 as Element of REAL n by Def6;
-lim seq2 = -LIMIT by Th13;
then
A20: p = seq1.k - LIMIT by A1,Th13;
dist(seq2.k, lim seq2) = sqrt ((Euclid_scalar n).(p,p)) by Def6
.= sqrt Sum mlt(p,p) by Def5
.= sqrt |(p,p)| by RVSUM_1:def 16
.= |.p.| by EUCLID_2:5;
hence thesis by A19,A20,Th1;
end;
hence lim seq1 = lim seq2 by A17,NORMSP_1:def 7;
end;
hence thesis;
end;
theorem
for n be Nat, seq1 be sequence of REAL-NS n, seq2 be
sequence of REAL-US n st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy
proof
let n be Nat, seq1 be sequence of REAL-NS n, seq2 be sequence of
REAL-US n;
assume that
A1: seq1 = seq2 and
A2: seq1 is Cauchy_sequence_by_Norm;
let r be Real;
assume
A3: r > 0;
reconsider r as Real;
r > 0 by A3;
then consider k be Nat such that
A4: for n,m be Nat st n >= k & m >= k holds dist(seq1.n, seq1
.m) < r by A2;
take k;
let m1,m2 be Nat;
reconsider p = seq2.m1 - seq2.m2 as Element of REAL n by Def6;
-seq1.m2 = -seq2.m2 by A1,Th13;
then seq1.m1 + (-seq1.m2) = seq2.m1 + (-seq2.m2) by A1,Th13;
then
A5: ||. seq1.m1 - seq1.m2 .|| = |.p.| by Th1
.= sqrt |(p,p)| by EUCLID_2:5
.= sqrt Sum mlt(p,p) by RVSUM_1:def 16
.= sqrt ((Euclid_scalar n).(p,p)) by Def5
.= ||. seq2.m1-seq2.m2 .|| by Def6;
assume m1 >= k & m2 >= k;
then dist(seq1.m1, seq1.m2) < r by A4;
hence thesis by A5;
end;
theorem Th18:
for n be Nat, seq1 be sequence of REAL-NS n, seq2 be
sequence of REAL-US n st seq1 = seq2 & seq2 is Cauchy holds seq1 is
Cauchy_sequence_by_Norm
proof
let n be Nat, seq1 be sequence of REAL-NS n, seq2 be sequence of
REAL-US n;
assume that
A1: seq1 = seq2 and
A2: seq2 is Cauchy;
let r be Real;
assume r > 0;
then consider k be Nat such that
A3: for m1,m2 be Nat st m1 >= k & m2 >= k holds dist(seq2.m1,
seq2.m2) < r by A2;
take k;
let m1,m2 be Nat;
reconsider p = seq2.m1 - seq2.m2 as Element of REAL n by Def6;
-seq1.m2 = -seq2.m2 by A1,Th13;
then
A4: p = seq1.m1 - seq1.m2 by A1,Th13;
assume m1 >= k & m2 >= k;
then
A5: dist(seq2.m1, seq2.m2) < r by A3;
||. seq2.m1 - seq2.m2 .|| = sqrt ((Euclid_scalar n). (p,p)) by Def6
.= sqrt Sum mlt(p,p) by Def5
.= sqrt |(p,p)| by RVSUM_1:def 16
.= |.p.| by EUCLID_2:5
.= ||. seq1.m1 - seq1.m2 .|| by A4,Th1;
hence thesis by A5;
end;
registration
let n;
cluster REAL-US n -> complete;
coherence
proof
let seq be sequence of REAL-US n;
reconsider seq9 = seq as sequence of REAL-NS n by Th15;
assume seq is Cauchy;
then seq9 is convergent by Th12,Th18;
hence thesis by Th16;
end;
end;