:: Finite Dimensional Real Normed Spaces are Proper Metric Spaces
:: by Kazuhisa Nakasho , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received September 30, 2021
:: Copyright (c) 2021-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 ARYTM_1, ARYTM_3, CARD_1, CARD_3, EUCLID, FINSEQ_1, FINSEQ_2,
FINSEQ_4, FUNCT_1, FUNCT_2, TOPMETR4, MATRIX_1, MATRLIN, NAT_1, NUMBERS,
ORDINAL4, PARTFUN1, PRE_TOPC, PRVECT_1, RANKNULL, RELAT_1, RLSUB_1,
RLVECT_1, RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI,
VALUED_0, VECTSP_1, XBOOLE_0, XXREAL_0, FUNCT_7, REAL_NS1, FUNCSDOM,
FUNCOP_1, ZFMISC_1, REAL_1, NORMSP_2, PCOMPS_1, METRIC_1, MSSUBFAM,
UNIALG_1, COMPLEX1, NORMSP_1, LOPBAN_1, DUALSP01, RCOMP_1, FCONT_1,
SEQ_1, SEQ_2, ORDINAL2, XXREAL_2, SQUARE_1, SEQ_4, REAL_NS3, CFCONT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, PARTFUN2,
ORDINAL1, FUNCT_2, BINOP_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2,
FINSEQOP, SEQ_1, SEQ_2, RVSUM_1, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC,
RLVECT_1, RLSUB_1, VECTSP_1, COMPTS_1, FUNCSDOM, METRIC_1, NORMSP_0,
NORMSP_1, MATRIX_1, FVSUM_1, MATRLIN, PCOMPS_1, RLVECT_5, EUCLID,
LOPBAN_1, VECTSP_9, RANKNULL, PRVECT_1, NFCONT_1, REAL_NS1, NORMSP_2,
DUALSP01, TOPMETR4;
constructors FVSUM_1, MATRIX13, MONOID_0, RANKNULL, RELSET_1, RLAFFIN1,
VECTSP10, PCOMPS_1, SQUARE_1, BINOP_2, REAL_NS1, RLVECT_5, REAL_1,
VECTSP_9, NFCONT_1, NORMSP_2, COMPTS_1, TBSP_1, COMSEQ_2, LOPBAN_1,
DUALSP01, SEQ_2, TOPMETR4, SEQ_4, PARTFUN2, RCOMP_1, FINSOP_1, VFUNCT_1,
FINSEQOP;
registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2,
MATRIX13, MATRLIN, NAT_1, NUMBERS, PRVECT_1, RELAT_1, RELSET_1, COMPLEX1,
RVSUM_1, STRUCT_0, VALUED_0, VECTSP_1, COMPTS_1, HAUSDORF, XREAL_0,
XXREAL_0, SQUARE_1, ORDINAL1, REAL_NS1, NORMSP_1, RLVECT_5, XBOOLE_0,
REAL_NS2;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities EUCLID, FINSEQ_1, STRUCT_0, VECTSP_1, RLVECT_1, NORMSP_2, ALGSTR_0,
PCOMPS_1, RVSUM_1, METRIC_1, MATRLIN, SQUARE_1, FVSUM_1, DUALSP01;
expansions STRUCT_0, NFCONT_1, LOPBAN_1, VECTSP_1;
theorems CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2,
NORMSP_0, NORMSP_1, NORMSP_2, MATRLIN, MATRLIN2, FINSEQOP, NAT_1,
ORDINAL1, PARTFUN1, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_5, RVSUM_1,
TARSKI, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, FUNCOP_1, REAL_NS1,
LOPBAN_1, NFCONT_1, SEQ_2, SEQ_4, LOPBAN_3, COMSEQ_2, COMPLEX1, SQUARE_1,
VALUED_1, JORDAN2B, TBSP_1, TOPMETR4, HAUSDORF, VALUED_0, NDIFF_1,
XXREAL_0, XXREAL_2, PDIFF_8, TOPREALC, RLVECT_4, RFUNCT_1, LOPBAN_7,
RCOMP_1, RLAFFIN3, NDIFF_5, LOPBAN_5, XCMPLX_1, ABSVALUE, REAL_NS2;
schemes FUNCT_2, NAT_1, FINSEQ_2;
begin :: Bolzano-Weierstrass Theorem and Its Corollary
reserve X for set,
n,m,k for Nat,
K for Field,
f for n-element real-valued FinSequence,
M for Matrix of n,m,F_Real;
theorem Th1:
for x be Element of REAL(n + 1),
y be Element of REAL n
st y = x | n
holds |.y.| <= |.x.|
proof
let x be Element of REAL(n+1),
y be Element of REAL n;
assume
A1: y = x | n;
A2: len x = n + 1 by CARD_1:def 7;
n + 1 in Seg(n + 1) by FINSEQ_1:4;
then n + 1 in dom x by A2,FINSEQ_1:def 3;
then x.(n + 1) in rng x by FUNCT_1:3;
then reconsider xn = x.(n+1) as Element of REAL;
x = y^<*xn*> by A1,A2,FINSEQ_3:55; then
sqr x = (sqr y) ^ <* sqrreal.xn *> by FINSEQOP:8;
then
A4: Sum(sqr x) = Sum(sqr y) + sqrreal.xn by RVSUM_1:74;
A5: 0 <= Sum(sqr y) by RVSUM_1:86;
sqrreal.xn = xn ^2 by RVSUM_1:def 2;
then 0 <= sqrreal.xn by XREAL_1:63;
then 0 + Sum (sqr y) <= Sum (sqr x) by A4,XREAL_1:7;
hence thesis by A5,SQUARE_1:26;
end;
theorem Th2:
for x be Element of REAL(n+1),
w be Element of REAL
st w = x.(n+1)
holds |.w.| <= |.x.|
proof
let x be Element of REAL(n+1);
let w be Element of REAL;
assume
A1: w = x.(n+1);
reconsider y = x as Point of TOP-REAL(n+1) by EUCLID:22;
reconsider y as FinSequence of REAL;
A2: len x = n+1 by CARD_1:def 7;
A3: n+1 in Seg (n+1) by FINSEQ_1:4;
then
A4: |.(y /. (n+1)).| <= |.x.| by PDIFF_8:1;
n + 1 in dom y by A2,FINSEQ_1:def 3,A3;
hence thesis by PARTFUN1:def 6,A4,A1;
end;
theorem Th3:
for x be Element of REAL(n+1),
y be Element of REAL n,
w be Element of REAL
st y = x | n & w = x.(n+1)
holds |.x.| <= |.y.| + |.w.|
proof
let x be Element of REAL (n+1),
y be Element of REAL n,
w be Element of REAL;
assume
A1: y = x | n & w = x.(n+1);
len x = n+1 by CARD_1:def 7; then
x = y ^ <*w*> by A1,FINSEQ_3:55; then
sqr x = (sqr y) ^ <* sqrreal.w *> by FINSEQOP:8;
then
A3: Sum (sqr x) = Sum (sqr y) + sqrreal.w by RVSUM_1:74;
A4: 0 <= Sum (sqr y) by RVSUM_1:86;
A5: sqrreal.w = w ^2 by RVSUM_1:def 2;
then 0 <= sqrreal.w by XREAL_1:63;
then sqrt(Sum (sqr x))
<= sqrt(Sum (sqr y)) + sqrt (sqrreal.w) by A3,A4,SQUARE_1:59;
hence thesis by A5,COMPLEX1:72;
end;
theorem Th4:
for x,y be Element of REAL n,
m be Nat
st m <= n
holds (x-y) | m = x|m - y|m
proof
let x,y be Element of REAL n,
m be Nat;
assume
A1: m <= n;
len x = n by CARD_1:def 7;
then
A2: len(x|m) = m by A1,FINSEQ_1:59;
len y = n by CARD_1:def 7;
then
A3: len(y|m) = m by A1,FINSEQ_1:59;
len(x-y) = n by CARD_1:def 7; then
len((x-y) | m) = m by A1,FINSEQ_1:59; then
A5: dom((x-y) | m) = Seg m by FINSEQ_1:def 3;
A6: dom(x|m -y|m)
= dom(x|m) /\ dom(y|m) by VALUED_1:12
.= (Seg m) /\ dom (y|m) by FINSEQ_1:def 3,A2
.= (Seg m) /\ (Seg m) by FINSEQ_1:def 3,A3
.= Seg m;
now let i be object;
assume A7: i in dom((x-y) | m);
then i in dom(x-y) /\ Seg m by RELAT_1:61;
then
A8: i in dom(x-y) & i in Seg m by XBOOLE_0:def 4;
hence ((x-y) | m).i
= (x-y).i by FUNCT_1:49
.= x.i -y.i by A8,VALUED_1:13
.= (x|m).i -y.i by A8,FUNCT_1:49
.= (x|m).i -(y|m).i by A8,FUNCT_1:49
.= ((x|m) - (y|m)).i by A5,A6,A7,VALUED_1:13;
end;
hence (x-y) | m = x|m - y|m by A5,A6,FUNCT_1:2;
end;
::Bolzano-Weierstrass Theorem n dimension
theorem Th5:
for n be Nat,
x be sequence of REAL-NS n
st ex K be Real
st for i be Nat holds ||. x.i .|| < K
holds
ex x0 be subsequence of x
st x0 is convergent
proof
defpred P[Nat] means
for x be sequence of REAL-NS $1
st ex K be Real
st for i be Nat holds ||. x.i .|| < K
holds
ex x0 be subsequence of x
st x0 is convergent;
A1: P[0]
proof
let x be sequence of REAL-NS 0;
assume
ex K be Real
st for i be Nat holds ||. x.i .|| < K;
A2: the carrier of (REAL-NS 0)
= REAL 0 by REAL_NS1:def 4
.= {<*>REAL} by FINSEQ_2:94;
then reconsider z = <*>REAL as Element of (REAL-NS 0) by TARSKI:def 1;
for i be Nat holds x.i = z by A2,TARSKI:def 1;
then
A3: x is constant by VALUED_0:def 18;
A4: x is subsequence of x by VALUED_0:19;
x is convergent by A3,NDIFF_1:18;
hence thesis by A4;
end;
A5: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A6: P[n];
let x be sequence of REAL-NS(n+1);
given K be Real such that
A7: for i be Nat holds ||. x.i .|| < K;
defpred P[object,object] means
ex xi be Element of REAL(n+1)
st xi = x.$1
& $2 = xi | n;
A8: for i be Element of NAT
ex y be Element of the carrier of REAL-NS n
st P[i,y]
proof
let i be Element of NAT;
reconsider xi=x.i as Element of REAL(n+1) by REAL_NS1:def 4;
A9: len xi = n+1 by CARD_1:def 7;
set y = xi| n;
A10: y is Element of (len y) -tuples_on REAL by FINSEQ_2:92;
len y = n by A9,NAT_1:11,FINSEQ_1:59;
then y in REAL n by A10;
then reconsider y as Element of the carrier of REAL-NS n
by REAL_NS1:def 4;
take y;
thus thesis;
end;
consider y be sequence of the carrier of REAL-NS n such that
A11: for i be Element of NAT holds P[i,y.i] from FUNCT_2:sch 3(A8);
reconsider y as sequence of REAL-NS n;
for i be Nat holds ||. y.i .|| < K
proof
let i be Nat;
i is Element of NAT by ORDINAL1:def 12;
then consider xi be Element of REAL (n+1) such that
A12: xi = x.i & y.i = xi | n by A11;
reconsider yi=y.i as Element of REAL n by REAL_NS1:def 4;
A13: |.yi.| <= |.xi.| by A12,Th1;
||. x.i .|| < K by A7;
then |. xi .| < K by A12,REAL_NS1:1;
then |. yi .| < K by A13,XXREAL_0:2;
hence ||. y.i .|| < K by REAL_NS1:1;
end;
then consider y0 be subsequence of y such that
A14: y0 is convergent by A6;
consider N0 be increasing sequence of NAT such that
A15: y0 = y * N0 by VALUED_0:def 17;
defpred P1[object,object] means
ex xi be Element of REAL(n+1)
st xi = (x*N0).$1
& $2 = xi.(n+1);
A16: for i be Element of NAT
ex y be Element of REAL st P1[i,y]
proof
let i be Element of NAT;
reconsider xi = (x*N0).i as Element of REAL(n+1) by REAL_NS1:def 4;
set y = xi.(n+1);
take y;
A17: len xi = n+1 by CARD_1:def 7;
n+1 in Seg (n+1) by FINSEQ_1:4;
then n+1 in dom xi by A17,FINSEQ_1:def 3;
then xi.(n+1) in rng xi by FUNCT_1:3;
hence thesis;
end;
consider w be sequence of REAL such that
A18: for i be Element of NAT holds P1[i,w.i] from FUNCT_2:sch 3(A16);
for i0 be set st i0 in dom w
holds |. w.i0 .| < K
proof
let i0 be set;
assume i0 in dom w; then
reconsider i = i0 as Element of NAT;
consider xi be Element of REAL (n+1) such that
A19: xi = (x*N0).i & w.i = xi.(n+1) by A18;
reconsider wi = w.i as Element of REAL;
A20: |.wi.| <= |.xi.| by A19,Th2;
dom N0 = NAT by FUNCT_2:def 1;
then (x*N0).i =x.(N0.i) by FUNCT_1:13;
then ||. (x*N0).i .|| < K by A7;
then |. xi .| < K by A19,REAL_NS1:1;
hence |. w.i0 .| < K by XXREAL_0:2,A20;
end;
then w is bounded by COMSEQ_2:def 3;
then consider w0 be Real_Sequence such that
A21: w0 is subsequence of w
& w0 is convergent by SEQ_4:40;
consider M0 be increasing sequence of NAT such that
A22: w0 = w * M0 by A21,VALUED_0:def 17;
reconsider N = N0*M0 as increasing sequence of NAT;
reconsider x0 = x*N as subsequence of x;
A23: for i be Nat holds
ex xi be Element of REAL (n+1)
st xi = x0.i
& (y0*M0).i = xi | n
& w0.i = xi.(n+1)
proof
let i be Nat;
A24: dom N0 = NAT & dom M0 = NAT by FUNCT_2:def 1;
A25: (y0*M0).i
= y0.(M0.i) by A24,ORDINAL1:def 12,FUNCT_1:13
.= y.(N0.(M0.i)) by A15,A24,FUNCT_1:13;
consider z be Element of REAL(n+1) such that
A26: z = x.(N0.(M0.i))
& y.(N0.(M0.i)) = z | n by A11;
take z;
thus
A27: x0.i
= ((x*N0)*M0).i by RELAT_1:36
.= (x*N0).(M0.i) by A24,ORDINAL1:def 12,FUNCT_1:13
.= z by A24,A26,FUNCT_1:13;
thus (y0*M0).i = z | n by A25,A26;
consider f be Element of REAL(n+1) such that
A28: f = (x*N0).(M0.i)
& w.(M0.i) = f.(n+1) by A18;
x0.i = ((x*N0)*M0).i by RELAT_1:36
.= f by A24,A28,ORDINAL1:def 12,FUNCT_1:13;
hence w0.i = z.(n+1) by A22,A24,A27,A28,ORDINAL1:def 12,FUNCT_1:13;
end;
A29: y0 * M0 is convergent by A14,LOPBAN_3:7;
set lmy = lim(y0*M0);
set lmw = lim w0;
reconsider lmy0 = lmy as Element of REAL n by REAL_NS1:def 4;
A30: len lmy0 = n by CARD_1:def 7;
then
A31: dom lmy0 = Seg n by FINSEQ_1:def 3;
set lmx = lmy0 ^ <*lmw*>;
A32: lmx is FinSequence of REAL by FINSEQ_1:75;
len lmx = len lmy0 + len <*lmw*> by FINSEQ_1:22
.= n + 1 by A30,FINSEQ_1:40;
then lmx is Element of (n+1) -tuples_on REAL by A32,FINSEQ_2:92;
then lmx in REAL(n+1);
then reconsider lmx as Element of REAL-NS(n+1) by REAL_NS1:def 4;
for r be Real st 0 < r
holds
ex m be Nat
st for i be Nat st m <= i
holds ||.(x0 . i) - lmx.|| < r
proof
let r be Real;
assume 0 < r;
then
A33: 0 < r/2 by XREAL_1:215;
then consider m1 be Nat such that
A34: for i be Nat st m1 <= i holds
||.((y0*M0) . i) - lmy.|| < r/2 by A29,NORMSP_1:def 7;
consider m2 be Nat such that
A35: for i be Nat st m2 <= i holds |. w0.i - lmw.| < r/2
by SEQ_2:def 7,A21,A33;
set m = m1 + m2;
take m;
thus for i be Nat st m <= i holds ||.(x0 . i) - lmx.|| < r
proof
let i be Nat;
assume
A36: m <= i;
m1 <= m by NAT_1:11;
then m1 <= i by A36,XXREAL_0:2;
then
A37: ||.((y0*M0) . i) - lmy.|| < r/2 by A34;
m2 <= m by NAT_1:11;
then m2 <= i by A36,XXREAL_0:2;
then
A38: |. w0.i - lmw.| < r/2 by A35;
reconsider lmx0 = lmx as Element of REAL (n+1) by REAL_NS1:def 4;
reconsider xi =x0 . i as Element of REAL (n+1) by REAL_NS1:def 4;
reconsider yi =(y0*M0) . i as Element of REAL n by REAL_NS1:def 4;
consider z be Element of REAL (n+1) such that
A39: z = x0.i
& (y0*M0).i =z | n
& w0.i = z.(n+1) by A23;
lmx0 | n = lmy0 by FINSEQ_1:21,A31; then
A41: (xi-lmx0) | n = yi -lmy0 by A39,Th4,NAT_1:11;
A42: len <*lmw*> = 1 & <*lmw*> .1 = lmw by FINSEQ_1:40;
A43: (xi-lmx0).(n+1)
= xi.(n+1)- lmx0.(n+1) by RVSUM_1:27
.= w0.i - lmw by A30,A39,A42,FINSEQ_1:65;
A44: ||.(x0 . i) - lmx.|| = |.xi-lmx0.| by REAL_NS1:5,REAL_NS1:1;
A45: ||.((y0*M0) . i) - lmy.|| = |.yi-lmy0.|
by REAL_NS1:5,REAL_NS1:1;
w0.i - lmw is Element of REAL by XREAL_0:def 1;
then
A46: |.xi-lmx0.| <= |.yi-lmy0.| + |.w0.i - lmw.| by A41,A43,Th3;
|.yi-lmy0.| + |.w0.i - lmw.| < r/2 + r/2 by A38,A37,A45,XREAL_1:8;
hence ||.(x0 . i) - lmx.|| < r by XXREAL_0:2,A46,A44;
end;
end;
then x0 is convergent by NORMSP_1:def 6;
hence thesis;
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(A1,A5);
end;
Lm3:
for n be Nat,
X be Subset of REAL-NS n
st X is closed
& ex r be Real
st for y be Point of REAL-NS n
st y in X
holds ||.y.|| < r
holds
X is compact
proof
let n be Nat,
X be Subset of REAL-NS n;
assume that
A1: X is closed and
A2: ex r be Real
st for y be Point of REAL-NS n
st y in X
holds ||.y.|| < r;
for s1 be sequence of REAL-NS n st rng s1 c= X
holds
ex s2 be sequence of REAL-NS n
st s2 is subsequence of s1
& s2 is convergent
& lim s2 in X
proof
let s1 be sequence of REAL-NS n;
assume
A3: rng s1 c= X;
consider r be Real such that
A4: for y be Point of REAL-NS n
st y in X
holds ||.y.|| < r by A2;
for i be Nat holds ||. s1.i .|| < r
proof
let i be Nat;
i in NAT by ORDINAL1:def 12;
then i in dom s1 by FUNCT_2:def 1;
then s1.i in rng s1 by FUNCT_1:3;
hence ||. s1.i .|| < r by A3,A4;
end;
then
consider s2 be subsequence of s1 such that
A5: s2 is convergent by Th5;
take s2;
ex N be increasing sequence of NAT
st s2 = s1 * N by VALUED_0:def 17;
then rng s2 c= rng s1 by RELAT_1:26;
hence thesis by A5,A1,A3,XBOOLE_1:1;
end;
hence X is compact;
end;
theorem Th6:
for Nrm be RealNormSpace,
X be Subset of Nrm
st X is compact
holds
X is closed
& ex r be Real
st for y be Point of Nrm
st y in X
holds ||.y.|| < r
proof
let Nrm be RealNormSpace,
X be Subset of Nrm;
assume
A1: X is compact;
per cases;
suppose
A2: X = {};
reconsider Y = X as Subset of TopSpaceNorm Nrm;
Y is closed by A2;
hence X is closed by NORMSP_2:15;
thus
ex r be Real
st for y be Point of Nrm
st y in X
holds ||.y.|| < r
proof
take 1;
thus for y be Point of Nrm st y in X holds ||.y.|| < 1 by A2;
end;
end;
suppose
A3: X <> {};
thus X is closed
proof
assume not X is closed;
then consider s1 be sequence of Nrm such that
A4: rng s1 c= X and
A5: s1 is convergent & not lim s1 in X;
ex s2 be sequence of Nrm
st s2 is subsequence of s1
& s2 is convergent
& lim s2 in X by A1,A4;
hence contradiction by A5,LOPBAN_3:8;
end;
reconsider Y = X as Subset of MetricSpaceNorm(Nrm);
A6: Y is sequentially_compact by A1,TOPMETR4:18;
reconsider Z = Y as Subset of TopSpaceMetr(MetricSpaceNorm(Nrm));
Z is compact by TOPMETR4:15,A6;
then
consider r0 be Real such that
A7: 0 < r0
& for x, y be Point of MetricSpaceNorm(Nrm)
st x in Y & y in Y
holds dist (x,y) <= r0
by HAUSDORF:18,TBSP_1:def 7;
consider x0 be object such that
A8: x0 in Y by A3,XBOOLE_0:def 1;
reconsider x0 as Point of MetricSpaceNorm(Nrm) by A8;
reconsider x = x0 as Point of Nrm;
set r = 1 + r0 + ||.x.||;
reconsider r as Real;
take r;
thus
for y be Point of Nrm
st y in X
holds ||.y.|| < r
proof
let y be Point of Nrm;
assume
A9: y in X;
reconsider y0 = y as Point of MetricSpaceNorm(Nrm);
y = x+(y-x) by RLVECT_4:1;
then
A10: ||.y.|| <= ||.x.|| + ||.y-x.|| by NORMSP_1:def 1;
||.y-x.|| = dist (y0,x0) by NORMSP_2:def 1;
then ||.y-x.|| + 0 < r0 + 1 by A7,A8,A9,XREAL_1:8;
then ||.x.|| + ||.y-x.|| < ||.x.|| + (r0+1) by XREAL_1:8;
hence ||.y.|| < r by A10,XXREAL_0:2;
end;
end;
end;
theorem
for X be Subset of REAL-NS n
holds
X is compact
iff
X is closed
&
ex r be Real
st for y be Point of REAL-NS n
st y in X
holds ||.y.|| < r by Lm3,Th6;
begin :: L1-norm and Maximum Norm
theorem Th8:
for n be non empty Nat,
x be Element of REAL n
holds
ex xMAX be Real
st xMAX in rng(abs x)
&
for i be Nat
st i in dom x
holds abs(x).i <= xMAX
proof
let n be non empty Nat,
x be Element of REAL n;
set F = rng(abs x);
A1: F is bounded_above
& upper_bound F in F by SEQ_4:133;
set xMAX = upper_bound F;
reconsider xMAX as Real;
take xMAX;
thus xMAX in rng(abs x) by SEQ_4:133;
thus
for i be Nat st i in dom x
holds abs(x).i <= xMAX
proof
let i be Nat;
assume i in dom x;
then i in dom(abs x) by VALUED_1:def 11;
then abs(x).i in F by FUNCT_1:3;
hence abs(x).i <= xMAX by A1,SEQ_4:def 1;
end;
end;
theorem Th9:
for x be real-valued FinSequence
holds 0 <= Sum abs x
proof
let x be real-valued FinSequence;
|.(Sum x).| <= Sum(abs x) by TOPREALC:21;
hence thesis;
end;
::: for x,y be FinSequence of REAL
::: holds abs(x^y) = (abs x)^(abs y) by TOPREAL7:11 goes by FINSEQOP:9;
definition
let n be Nat;
assume
A1: n is non empty;
func max_norm(n) -> Function of REAL n,REAL means
:Def1:
for x be Element of REAL n
holds it.x in rng(abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= it.x;
existence
proof
defpred P[object,Element of REAL] means
ex x be Element of REAL n
st x=$1
&
$2 in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= $2;
A2: for x be Element of REAL n
ex y be Element of REAL st P[x,y]
proof
let x be Element of REAL n;
consider xMAX be Real such that
A3: xMAX in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= xMAX by A1,Th8;
reconsider xMAX as Element of REAL by XREAL_0:def 1;
take xMAX;
thus thesis by A3;
end;
consider w be Function of REAL n,REAL such that
A4: for x be Element of REAL n holds P[x,w.x] from FUNCT_2:sch 3(A2);
take w;
thus
for x be Element of REAL n
holds w.x in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= w.x
proof
let x be Element of REAL n;
ex x0 be Element of REAL n
st x0 = x
&
w.x in rng (abs x0)
&
for i be Nat st i in dom x0
holds abs(x0).i <= w.x by A4;
hence thesis;
end;
end;
uniqueness
proof
let NORM1, NORM2 be Function of REAL n,REAL;
assume that
A5: for x be Element of REAL n
holds NORM1.x in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= NORM1.x
and
A6: for x be Element of REAL n
holds NORM2.x in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= NORM2.x;
for x be Element of REAL n
holds NORM1 . x = NORM2 . x
proof
let x be Element of REAL n;
A7: NORM1.x in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= NORM1.x by A5;
NORM2.x in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= NORM2.x by A6;
then
consider i be object such that
A8: i in dom(abs x) & NORM2.x = abs(x).i by FUNCT_1:def 3;
A9: dom (abs x) = dom x by VALUED_1:def 11;
reconsider i as Nat by A8;
A10: NORM2.x <= NORM1.x by A5,A8,A9;
consider j be object such that
A11: j in dom (abs x) & NORM1.x = abs(x).j by A7,FUNCT_1:def 3;
NORM1.x <= NORM2.x by A6,A9,A11;
hence NORM1.x = NORM2.x by XXREAL_0:1,A10;
end;
hence NORM1 = NORM2 by FUNCT_2:63;
end;
end;
definition
let n be Nat;
assume n is non empty;
func sum_norm(n) -> Function of REAL n,REAL means
:Def2:
for x be Element of REAL n
holds it.x = Sum(abs x);
existence
proof
defpred P[object,Element of REAL] means
ex x be Element of REAL n
st x = $1
&
$2 = Sum (abs x);
A1: for x be Element of REAL n
ex y be Element of REAL
st P[x,y]
proof
let x be Element of REAL n;
reconsider y = Sum(abs x) as Element of REAL;
take y;
thus thesis;
end;
consider w be Function of REAL n,REAL such that
A2: for x be Element of REAL n holds P[x,w.x] from FUNCT_2:sch 3(A1);
take w;
thus for x be Element of REAL n holds w.x = Sum(abs x)
proof
let x be Element of REAL n;
ex x0 be Element of REAL n
st x0 = x
&
w.x = Sum(abs x0) by A2;
hence thesis;
end;
end;
uniqueness
proof
let NORM1, NORM2 be Function of REAL n,REAL;
assume that
A3: for x be Element of REAL n
holds NORM1.x = Sum(abs x)
and
A4: for x be Element of REAL n
holds NORM2.x = Sum(abs x);
for x be Element of REAL n
holds NORM1.x = NORM2.x
proof
let x be Element of REAL n;
thus NORM1.x = Sum(abs x) by A3
.= NORM2.x by A4;
end;
hence NORM1 = NORM2 by FUNCT_2:63;
end;
end;
theorem Th11:
for x be Element of REAL n,
xMAX be Real
st xMAX in rng (abs x)
& for i be Nat st i in dom x
holds abs(x).i <= xMAX
holds
Sum(abs x) <= n * xMAX
& xMAX <= |.x.|
& |.x.| <= Sum(abs x)
proof
let x be Element of REAL n,
xMAX be Real;
assume
A1: xMAX in rng (abs x)
& for i be Nat st i in dom x
holds abs(x).i <= xMAX;
len x = n by CARD_1:def 7;
then
A2: dom x = Seg n by FINSEQ_1:def 3;
A3: dom(abs x) = dom x by VALUED_1:def 11;
set F = n |-> xMAX;
for j be Nat st j in Seg n
holds (abs x) . j <= F . j
proof
let j be Nat;
assume
A4: j in Seg n;
then (abs x) . j <= xMAX by A1,A2;
hence thesis by A4,FINSEQ_2:57;
end;
then
A5: Sum(abs x) <= Sum(F) by RVSUM_1:82;
consider i be object such that
A6: i in dom(abs x) & xMAX = (abs x).i by A1,FUNCT_1:def 3;
reconsider i as Element of NAT by A6;
A7: (abs x).i
= absreal.(x.i) by A3,A6,FUNCT_1:13
.= |.x.i.| by EUCLID:def 2;
reconsider y = x as Point of TOP-REAL n by EUCLID:22;
reconsider y as FinSequence of REAL;
defpred P[Nat] means
for x be Element of REAL $1
holds |.x.|^2 <= (Sum(abs x))^2;
A8: P[0] by RVSUM_1:72;
A9: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A10: P[n];
let x be Element of REAL(n+1);
set y = x | n;
A11: len x = n+1 by CARD_1:def 7;
A12: y is Element of (len y) -tuples_on REAL by FINSEQ_2:92;
reconsider y = x|n as Element of REAL n
by A11,A12,NAT_1:11,FINSEQ_1:59;
n+1 in Seg(n+1) by FINSEQ_1:4;
then n+1 in dom x by A11,FINSEQ_1:def 3;
then x.(n+1) in rng x by FUNCT_1:3;
then reconsider w = x.(n+1) as Element of REAL;
A13: x = y ^ <*w*> by A11,FINSEQ_3:55;
A14: 0 <= Sum(sqr y) by RVSUM_1:86;
A15: 0 <= Sum(sqr x) by RVSUM_1:86;
sqr x = (sqr y) ^ <* sqrreal.w *> by A13,FINSEQOP:8;
then
A16: Sum(sqr x)
= Sum(sqr y) + sqrreal.w by RVSUM_1:74
.= Sum(sqr y) + w^2 by RVSUM_1:def 2
.= |.y.| ^2 + w^2 by A14,SQUARE_1:def 2;
A17: |.x.| ^2 = Sum(sqr x) by A15,SQUARE_1:def 2;
abs x
= (abs y) ^ abs(<*w*>) by A13,FINSEQOP:9
.= (abs y) ^ <*|.w.|*> by JORDAN2B:19;
then
(Sum(abs x))^2
= (Sum(abs y) + |.w.|)^2 by RVSUM_1:74
.= (Sum(abs y))^2 + 2 * Sum(abs y) * |.w.| + |.w.| ^2
.= (Sum(abs y))^2 + 2 * Sum(abs y) * |.w.| + w^2 by COMPLEX1:75;
then
A18: (Sum(abs x)) ^2 - |.x.| ^2
= (Sum(abs y)) ^2- |.y.| ^2 + 2 * Sum(abs y) * |.w.| by A16,A17;
A19: 0 <= (Sum(abs y))^2 - |.y.| ^2 by A10,XREAL_1:48;
0 <= |.w.| & 0 <= Sum(abs y) by Th9;
hence |.x.|^2 <= (Sum(abs x))^2 by A18,A19,XREAL_1:49;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A8,A9);
then
A20: |.x.|^2 <= (Sum(abs x))^2;
n is Element of NAT by ORDINAL1:def 12;
then |. y /. i.| <= |.x.| by A2,A3,A6,PDIFF_8:1;
hence thesis by A3,A5,A6,A7,A20,Th9,
PARTFUN1:def 6,RVSUM_1:80,SQUARE_1:16;
end;
theorem Th12:
for n be non empty Nat,
x,y be Element of REAL n,
a be Real
holds
0 <= (max_norm(n)).x
& ((max_norm(n)).x = 0 iff x = 0*n)
& (max_norm(n)).(a * x) = |.a.| * (max_norm(n)).x
& (max_norm(n)).(x + y) <= (max_norm(n)).x + (max_norm(n)).y
proof
let n be non empty Nat,
x, y be Element of REAL n,
a be Real;
set xMAX = (max_norm(n)).x;
set yMAX = (max_norm(n)).y;
set axMAX = (max_norm(n)).(a*x);
set xyMAX = (max_norm(n)).(x+y);
A1: xMAX in rng (abs x)
& for i be Nat st i in dom x
holds abs(x).i <= xMAX by Def1;
A2: axMAX in rng (abs(a*x))
& for i be Nat st i in dom (a*x)
holds abs(a*x).i <= axMAX by Def1;
A3: xyMAX in rng (abs(x+y))
& for i be Nat st i in dom (x+y)
holds abs(x+y).i <= xyMAX by Def1;
A4: dom x = dom (abs x) by VALUED_1:def 11;
A5: dom y = dom (abs y) by VALUED_1:def 11;
A6: len x = n by CARD_1:def 7;
then
A7: dom x = Seg n by FINSEQ_1:def 3;
len y = n by CARD_1:def 7;
then
A8: dom y = Seg n by FINSEQ_1:def 3;
len (x+y) = n by CARD_1:def 7;
then
A9: dom (x+y) = Seg n by FINSEQ_1:def 3;
xMAX in rng (abs x) by Def1;
then consider j0 be object such that
A10: j0 in dom (abs x) & xMAX = (abs x).j0 by FUNCT_1:def 3;
reconsider j0 as Nat by A10;
(abs x).j0 = |. x.j0 .| by A10,VALUED_1:def 11;
hence 0 <= (max_norm(n)).x by A10;
yMAX in rng (abs y) by Def1;
then consider k0 be object such that
A11: k0 in dom (abs y) & yMAX =(abs y).k0 by FUNCT_1:def 3;
reconsider k0 as Nat by A11;
thus (max_norm(n)).x = 0 iff x=0*n
proof
hereby
assume
A12: (max_norm(n)).x = 0;
for i be object st i in dom x holds x.i = 0
proof
let i0 be object;
assume
A13: i0 in dom x;
then reconsider i = i0 as Nat;
abs(x).i <= 0 by A12,A13,Def1;
then |.x.i.| <= 0 by A4,A13,VALUED_1:def 11;
hence x.i0 = 0;
end;
hence
x = (dom x) --> 0 by FUNCOP_1:11
.= (Seg n) --> (In (0,REAL)) by A6,FINSEQ_1:def 3
.= 0* n by FINSEQ_2:def 2;
end;
assume
A14: x = 0*n;
consider j be object such that
A15: j in dom (abs x)
& xMAX = (abs x).j by A1,FUNCT_1:def 3;
reconsider j as Nat by A15;
(abs x).j
= |. x.j .| by A15,VALUED_1:def 11
.= 0 by A14;
hence xMAX = 0 by A15;
end;
thus
(max_norm(n)).(a*x) = |.a.| * (max_norm(n)).x
proof
set L = |.a.| * (max_norm(n)).x;
A16: dom(abs(a*x)) = dom(a*x) by VALUED_1:def 11;
A17: dom(a*x) = dom x by VALUED_1:def 5;
A18: j0 in dom(a*x) by A4,A10,VALUED_1:def 5;
then
(abs (a*x)).j0
= |. (a*x).j0 .| by A16,VALUED_1:def 11
.= |. a*(x.j0) .| by A18,VALUED_1:def 5
.= |.a.| * |.x.j0.| by COMPLEX1:65
.= L by A10,VALUED_1:def 11;
then
A19: L <= (max_norm(n)).(a*x) by Def1,A18;
consider k0 be object such that
A20: k0 in dom (abs (a*x))
& axMAX =(abs (a*x)).k0 by FUNCT_1:def 3,A2;
reconsider j0 as Nat;
A21: (abs (a*x)).k0
= |. (a*x).k0 .| by A20,VALUED_1:def 11
.= |.a*(x.k0).| by A16,A20,VALUED_1:def 5
.= |.a.| * |.x.k0.| by COMPLEX1:65;
A22: abs(x).k0 <= xMAX by A16,A17,A20,Def1;
abs(x).k0 = |. x.k0 .| by A4,A16,A17,A20,VALUED_1:def 11;
then axMAX <= L by A20,A21,A22,XREAL_1:64;
hence (max_norm(n)).(a*x) = L by A19,XXREAL_0:1;
end;
thus (max_norm(n)).(x+y) <= (max_norm(n)).x+(max_norm(n)).y
proof
A23: dom (abs(x+y)) = dom (x+y) by VALUED_1:def 11;
consider h0 be object such that
A24: h0 in dom (abs(x+y))
& xyMAX = (abs (x+y)).h0 by A3,FUNCT_1:def 3;
A25: h0 in Seg n by A9,A24,VALUED_1:def 11;
reconsider j0 as Nat;
A26: (abs (x+y)).h0
= |. (x+y).h0 .| by A24,VALUED_1:def 11
.= |.x.h0 + y.h0.| by A23,A24,VALUED_1:def 1;
A27: |.x.h0 + y.h0.| <= |.x.h0.| + |.y.h0.| by COMPLEX1:56;
abs(x).h0 <= xMAX by A7,A25,Def1;
then
A28: |. x.h0 .| <= xMAX by A4,A25,A7,VALUED_1:def 11;
abs(y).h0 <= yMAX by A8,A25,Def1;
then |. y.h0 .| <= yMAX by A5,A8,A25,VALUED_1:def 11;
then |. x.h0 .| + |. y.h0 .| <= xMAX +yMAX by A28,XREAL_1:7;
hence thesis by A24,A26,A27,XXREAL_0:2;
end;
end;
theorem Th13:
for n be non empty Nat,
x, y be Element of REAL n,
a be Real
holds
0 <= (sum_norm(n)).x
& ((sum_norm(n)).x = 0 iff x = 0*n)
& (sum_norm(n)).(a*x) = |.a.| * (sum_norm(n)).x
& (sum_norm(n)).(x+y) <= (sum_norm(n)).x + (sum_norm(n)).y
proof
let n be non empty Nat,
x, y be Element of REAL n,
a be Real;
set xSUM = (sum_norm(n)).x;
set ySUM = (sum_norm(n)).y;
set axSUM = (sum_norm(n)).(a*x);
set xySUM = (sum_norm(n)).(x+y);
A2: (sum_norm(n)).y = Sum (abs y) by Def2;
0 <= Sum (abs x) by Th9;
hence 0 <= (sum_norm(n)).x by Def2;
A3: (sum_norm(n)).x = Sum (abs x) by Def2;
thus (sum_norm(n)).x = 0 iff x = 0*n
proof
hereby
assume (sum_norm(n)).x = 0; then
A5: Sum (abs x) = 0 by Def2;
A6: len x = n by CARD_1:def 7;
A7: len (n |-> 0) = n by CARD_1:def 7;
assume x <> 0*n;
then consider j be Nat such that
A8: j in dom x and
A9: x . j <> (n |-> 0) . j by A6,A7,FINSEQ_2:9;
A10: dom x = dom (abs x) by VALUED_1:def 11;
A11: dom x = Seg (len x) by FINSEQ_1:def 3;
0 < |.x . j .| by A9;
then
A12: 0 < (abs x) . j by A8,A10,VALUED_1:def 11;
A13:
now
let k be Nat;
assume
A14: k in dom (abs x);
set r = (abs x) . k;
set z = x . k;
0 <= |.x . k.|;
hence 0 <= (abs x) . k by A14,VALUED_1:def 11;
end;
dom(abs x) = Seg(len(abs x)) by FINSEQ_1:def 3;
then j in dom(abs x) by A8,A11,FINSEQ_2:33;
hence contradiction by A5,A12,A13,RVSUM_1:85;
end;
assume x = 0*n;
then abs x= n |-> 0 by EUCLID:4;
hence (sum_norm(n)).x = 0 by A3,RVSUM_1:81;
end;
thus
(sum_norm(n)).(a*x)
= Sum (abs (a*x)) by Def2
.= Sum (|.a.| * (abs x)) by RFUNCT_1:25
.= |.a.| * Sum (abs x) by RVSUM_1:87
.= |.a.| * (sum_norm(n)).x by Def2;
for j be Nat st j in Seg n
holds (abs(x+y)).j <= (abs(x)+abs(y)).j
proof
let j be Nat;
assume A15:j in Seg n;
A16: dom x = dom (abs x) by VALUED_1:def 11;
A17: dom x
= Seg (len x) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
A18: dom y = dom (abs y) by VALUED_1:def 11;
A19: dom y
= Seg (len y) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
A20: dom (x+y) = dom (abs (x+y)) by VALUED_1:def 11;
A22: dom ((abs x)+(abs y))
= dom((abs x)) /\ dom((abs y)) by VALUED_1:def 1
.= Seg n by A16,A17,A18,A19;
A21: dom (x+y)
= Seg (len (x+y)) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7; then
A23: (abs(x+y)).j
= |.(x+y).j.| by A15,A20,VALUED_1:def 11
.= |.x.j+y.j.| by A15,A21,VALUED_1:def 1;
|.x.j+y.j.| <= |.x.j.| + |.y.j.| by COMPLEX1:56;
then (abs(x+y)).j <= (abs x).j + |.y.j.|
by A15,A16,A17,A23,VALUED_1:def 11;
then (abs(x+y)).j <= (abs x).j + (abs y).j
by A15,A18,A19,VALUED_1:def 11;
hence (abs(x+y)).j <=((abs x)+(abs y)).j
by A15,A22,VALUED_1:def 1;
end;
then Sum (abs(x+y)) <= Sum (abs(x) + abs(y)) by RVSUM_1:82;
then Sum (abs(x+y)) <= Sum (abs(x)) + Sum (abs(y)) by RVSUM_1:89;
hence
(sum_norm(n)).(x+y) <= (sum_norm(n)).(x) +(sum_norm(n)).(y) by A2,A3,Def2;
end;
theorem Th14:
for n be non empty Nat,
x be Element of REAL n
holds
(sum_norm(n)).x <= n * (max_norm(n)).x
& (max_norm(n)).x <= |.x.|
& |.x.| <= (sum_norm(n)).x
proof
let n be non empty Nat,
x be Element of REAL n;
set xMAX = (max_norm(n)).x;
xMAX in rng (abs x)
&
for i be Nat st i in dom x
holds abs(x).i <= xMAX by Def1;
then
Sum (abs x) <= n* xMAX
&
xMAX <= |.x.|
&
|.x.| <= Sum (abs x) by Th11;
hence thesis by Def2;
end;
theorem Th15:
the RLSStruct of REAL-NS(n) = RealVectSpace(Seg n)
proof
thus the RLSStruct of REAL-NS(n)
= the RLSStruct of TOP-REAL(n) by REAL_NS2:1
.= RealVectSpace(Seg n) by EUCLID:def 8;
end;
theorem Th16:
for a be Real,
x,y be Element of REAL-NS(n),
x0,y0 be Element of RealVectSpace(Seg n)
st x = x0 & y = y0
holds
the carrier of REAL-NS(n) = the carrier of RealVectSpace(Seg n)
& 0. REAL-NS(n) = 0.RealVectSpace(Seg n)
& x + y = x0 + y0
& a * x = a * x0
& -x = -x0
& x - y = x0 - y0
proof
let a be Real,
x,y be Element of REAL-NS(n),
x0,y0 be Element of RealVectSpace(Seg n);
assume
A1: x = x0 & y = y0;
A2: the RLSStruct of REAL-NS(n) = RealVectSpace(Seg n) by Th15;
set V = REAL-NS(n);
set W = RealVectSpace(Seg n);
thus the carrier of REAL-NS (n) = the carrier of RealVectSpace(Seg n)
&
0. REAL-NS (n) = 0.RealVectSpace(Seg n) by A2;
thus x + y = x0 + y0 by A1,A2;
thus a * x = a * x0 by A1,A2;
thus
-x = (-1) * x by RLVECT_1:16
.= (-1) * x0 by A1,A2
.= -x0 by RLVECT_1:16;
-y = (-1) * y by RLVECT_1:16
.= (-1) * y0 by A1,A2
.= -y0 by RLVECT_1:16;
hence x-y = x0 - y0 by A1,A2;
end;
registration
let X be finite-dimensional RealLinearSpace;
cluster RLSp2RVSp(X) -> finite-dimensional;
correctness by REAL_NS2:82;
end;
theorem Th17:
for X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
y be Element of RLSp2RVSp(X)
holds y |-- b is Element of REAL(dim X)
proof
let X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
y be Element of RLSp2RVSp(X);
set z = y |-- b;
len z = len b by MATRLIN:def 7
.= dim(RLSp2RVSp(X)) by MATRLIN2:21
.= dim X by REAL_NS2:81;
hence thesis by FINSEQ_2:92;
end;
definition
let X be finite-dimensional RealLinearSpace;
let b be OrdBasis of RLSp2RVSp(X);
func max_norm(X,b) -> Function of X,REAL means
:Def3:
for x be Element of X
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& it.x = (max_norm(dim X)).z;
existence
proof
defpred P[object,Element of REAL] means
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = $1
& z = y |-- b
& $2 = (max_norm(dim X)).z;
A1: for x be Element of the carrier of X
ex r be Element of REAL
st P[x,r]
proof
let x be Element of the carrier of X;
reconsider y = x as Element of RLSp2RVSp(X);
reconsider z = y |-- b as Element of REAL(dim X) by Th17;
reconsider r = (max_norm(dim X)).z
as Element of REAL;
take r;
thus P[x,r];
end;
consider w be Function of the carrier of X,REAL such that
A2: for x be Element of the carrier of X holds P[x,w.x]
from FUNCT_2:sch 3(A1);
take w;
thus thesis by A2;
end;
uniqueness
proof
let NORM1, NORM2 be Function of X,REAL;
assume that
A3: for x be Element of X holds
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y & z = y |-- b
& NORM1.x = (max_norm(dim X)).z
and
A4: for x be Element of X holds
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y & z = y |-- b
& NORM2.x = (max_norm(dim X)).z;
for x be Element of X
holds NORM1 . x = NORM2 . x
proof
let x be Element of X;
A5: ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = x & z = y |-- b
& NORM1.x = (max_norm(dim X)).z by A3;
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = x
& z = y |-- b
& NORM2.x = (max_norm(dim X)).z by A4;
hence thesis by A5;
end;
hence NORM1 = NORM2 by FUNCT_2:63;
end;
end;
definition
let X be finite-dimensional RealLinearSpace;
let b be OrdBasis of RLSp2RVSp(X);
func sum_norm(X,b) -> Function of X,REAL means
:Def4:
for x be Element of X
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& it.x = (sum_norm(dim X)).z;
existence
proof
defpred P[object,Element of REAL] means
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = $1
& z = y |-- b
& $2 = (sum_norm(dim X)).z;
A1: for x be Element of the carrier of X
ex r be Element of REAL
st P[x,r]
proof
let x be Element of the carrier of X;
reconsider y = x as Element of RLSp2RVSp(X);
reconsider z = y |-- b as Element of REAL(dim X) by Th17;
reconsider r = (sum_norm(dim X)).z as Element of REAL;
take r;
thus P[x,r];
end;
consider w be Function of the carrier of X,REAL such that
A2: for x be Element of the carrier of X holds P[x,w.x]
from FUNCT_2:sch 3(A1);
take w;
thus thesis by A2;
end;
uniqueness
proof
let NORM1, NORM2 be Function of X,REAL;
assume that
A3: for x be Element of X holds
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& NORM1.x = (sum_norm(dim X)).z
and
A4: for x be Element of X holds
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& NORM2.x = (sum_norm(dim X)).z;
for x be Element of X
holds NORM1 . x = NORM2 . x
proof
let x be Element of X;
A5: ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = x
& z = y |-- b
& NORM1.x = (sum_norm(dim X)).z by A3;
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = x
& z = y |-- b
& NORM2.x = (sum_norm(dim X)).z by A4;
hence thesis by A5;
end;
hence NORM1 = NORM2 by FUNCT_2:63;
end;
end;
definition
let X be finite-dimensional RealLinearSpace;
let b be OrdBasis of RLSp2RVSp (X);
func euclid_norm(X,b) -> Function of X,REAL means
:Def5:
for x be Element of X
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& it.x = |.z.|;
existence
proof
defpred P[object,Element of REAL] means
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st y = $1
& z = y |-- b
& $2= |.z.|;
A1: for x be Element of the carrier of X
ex r be Element of REAL
st P[x,r]
proof
let x be Element of the carrier of X;
reconsider y = x as Element of RLSp2RVSp(X);
reconsider z = y |-- b as Element of REAL(dim X) by Th17;
reconsider r = |.z.| as Element of REAL by XREAL_0:def 1;
take r;
thus P[x,r];
end;
consider w be Function of the carrier of X,REAL such that
A2: for x be Element of the carrier of X holds P[x,w.x]
from FUNCT_2:sch 3(A1);
take w;
thus thesis by A2;
end;
uniqueness
proof
let NORM1, NORM2 be Function of X,REAL;
assume that
A3: for x be Element of X holds
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& NORM1.x = |.z.|
and
A4: for x be Element of X holds
ex y be Element of RLSp2RVSp(X),
z be Element of REAL(dim X)
st x = y
& z = y |-- b
& NORM2.x = |.z.|;
for x be Element of X holds NORM1 . x = NORM2 . x
proof
let x be Element of X;
A5: ex y be Element of RLSp2RVSp (X),
z be Element of REAL (dim X)
st y = x
& z = y |-- b
& NORM1.x = |.z.| by A3;
ex y be Element of RLSp2RVSp (X),
z be Element of REAL (dim X)
st y = x
& z = y |-- b
& NORM2.x = |.z.| by A4;
hence thesis by A5;
end;
hence NORM1 = NORM2 by FUNCT_2:63;
end;
end;
theorem
for n be Nat,
a be Element of REAL,
a1 be Element of F_Real,
x,y be Element of REAL n,
x1,y1 be Element of n-tuples_on the carrier of F_Real
st a = a1 & x = x1 & y = y1
holds a * x = a1 * x1
& x + y = x1 + y1;
theorem Th19:
for X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
x,y be Element of X,
a be Real
st dim X <> 0
holds
0 <= (max_norm(X,b)).x
& ((max_norm(X,b)).x = 0 iff x = 0.X)
& (max_norm(X,b)).(a*x) = |.a.| * (max_norm(X,b)).x
& (max_norm(X,b)).(x+y) <= (max_norm(X,b)).x + (max_norm(X,b)).y
proof
let X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp (X),
x, y be Element of X,
a be Real;
assume
A1: dim X <> 0;
set xSUM = (max_norm(X,b)).x;
set ySUM = (max_norm(X,b)).y;
set axSUM = (max_norm(X,b)).(a*x);
set xySUM = (max_norm(X,b)).(x+y);
consider x1 be Element of RLSp2RVSp (X),
z1 be Element of REAL (dim X) such that
A2: x = x1
& z1 = x1 |-- b
& xSUM = (max_norm(dim X)).z1 by Def3;
consider x2 be Element of RLSp2RVSp(X),
z2 be Element of REAL(dim X) such that
A3: y = x2
& z2 = x2 |-- b
& ySUM = (max_norm(dim X)).z2 by Def3;
consider xy be Element of RLSp2RVSp(X),
z3 be Element of REAL(dim X) such that
A4: x + y = xy
& z3 = xy |-- b
& xySUM = (max_norm(dim X)).z3 by Def3;
consider ax be Element of RLSp2RVSp(X),
z4 be Element of REAL(dim X) such that
A5: a*x = ax
& z4 = ax |-- b
& axSUM = (max_norm(dim X)).z4 by Def3;
thus 0 <= xSUM by A1,A2,Th12;
0* (dim X)
= dim(RLSp2RVSp(X)) |-> (0. F_Real) by REAL_NS2:81
.= len(b) |-> (0. F_Real) by MATRLIN2:21
.= (0. RLSp2RVSp(X)) |-- b by MATRLIN2:20;
hence xSUM = 0 iff x = 0.X by A1,A2,Th12,MATRLIN:34;
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
ax = a1 * x1 by A2,A5; then
z4 = a1 * (x1 |-- b) by A5,MATRLIN2:18
.= a * z1 by A2;
hence axSUM = |.a.| * xSUM by A1,A2,A5,Th12;
xy = x1 + x2 by A2,A3,A4; then
z3 = (x1 |-- b) + (x2 |-- b) by A4,MATRLIN2:17
.= z1 + z2 by A2,A3;
hence xySUM <= xSUM+ySUM by A1,A2,A3,A4,Th12;
end;
theorem
for X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
x,y be Element of X,
a be Real
st dim X <> 0
holds
0 <= (sum_norm(X,b)).x
& ((sum_norm(X,b)).x = 0 iff x=0.X)
& (sum_norm(X,b)).(a*x) = |.a.| * (sum_norm(X,b)).x
& (sum_norm(X,b)).(x+y) <= (sum_norm(X,b)).x + (sum_norm(X,b)).y
proof
let X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
x, y be Element of X,
a be Real;
assume
A1: dim X <> 0;
set xSUM = (sum_norm(X,b)).x;
set ySUM = (sum_norm(X,b)).y;
set axSUM = (sum_norm(X,b)).(a * x);
set xySUM = (sum_norm(X,b)).(x + y);
consider x1 be Element of RLSp2RVSp(X),
z1 be Element of REAL(dim X) such that
A2: x = x1
& z1 = x1 |-- b
& xSUM = (sum_norm(dim X)).z1 by Def4;
consider x2 be Element of RLSp2RVSp(X),
z2 be Element of REAL(dim X) such that
A3: y = x2
& z2 = x2 |-- b
& ySUM = (sum_norm(dim X)).z2 by Def4;
consider xy be Element of RLSp2RVSp (X),
z3 be Element of REAL (dim X) such that
A4: x + y = xy
& z3 = xy |-- b
& xySUM = (sum_norm(dim X)).z3 by Def4;
consider ax be Element of RLSp2RVSp (X),
z4 be Element of REAL (dim X) such that
A5: a * x = ax
& z4 = ax |-- b
& axSUM = (sum_norm(dim X)).z4 by Def4;
thus 0 <= xSUM by A2,Th13,A1;
0* (dim X)
= (dim(RLSp2RVSp(X))) |-> (0. F_Real) by REAL_NS2:81
.= (len(b)) |-> (0. F_Real) by MATRLIN2:21
.= (0. RLSp2RVSp(X)) |-- b by MATRLIN2:20;
hence xSUM = 0 iff x = 0.X by A1,A2,Th13,MATRLIN:34;
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
ax = a1 * x1 by A2,A5; then
z4 = a1 * (x1 |-- b) by A5,MATRLIN2:18
.= a * z1 by A2;
hence axSUM = |.a.| * xSUM by A1,A2,A5,Th13;
xy = x1 + x2 by A2,A3,A4; then
z3 = (x1 |-- b) + (x2 |-- b) by A4,MATRLIN2:17
.= z1 + z2 by A2,A3;
hence xySUM <= xSUM + ySUM by A1,A2,A3,A4,Th13;
end;
theorem
for X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
x, y be Element of X,
a be Real
holds
0 <= (euclid_norm(X,b)).x
& ((euclid_norm(X,b)).x = 0 iff x = 0.X)
& (euclid_norm(X,b)).(a*x) = |.a.| * (euclid_norm(X,b)).x
& (euclid_norm(X,b)).(x+y) <= (euclid_norm(X,b)).x + (euclid_norm(X,b)).y
proof
let X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(X),
x, y be Element of X,
a be Real;
set xSUM = (euclid_norm(X,b)).x;
set ySUM = (euclid_norm(X,b)).y;
set axSUM = (euclid_norm(X,b)).(a*x);
set xySUM = (euclid_norm(X,b)).(x+y);
consider x1 be Element of RLSp2RVSp(X),
z1 be Element of REAL(dim X) such that
A1: x = x1
& z1 = (x1 |-- b)
& xSUM = |.z1.| by Def5;
consider x2 be Element of RLSp2RVSp(X),
z2 be Element of REAL(dim X) such that
A2: y = x2
& z2 = (x2 |-- b)
& ySUM = |.z2.| by Def5;
consider xy be Element of RLSp2RVSp(X),
z3 be Element of REAL(dim X) such that
A3: x + y = xy
& z3 = (xy |-- b)
& xySUM = |.z3.| by Def5;
consider ax be Element of RLSp2RVSp(X),
z4 be Element of REAL(dim X) such that
A4: a * x = ax
& z4 = (ax |-- b)
& axSUM = |.z4.| by Def5;
thus 0 <= xSUM by A1;
0* (dim X)
= (dim (RLSp2RVSp (X))) |-> (0. F_Real) by REAL_NS2:81
.= (len (b)) |-> (0. F_Real) by MATRLIN2:21
.= (0. RLSp2RVSp (X)) |-- b by MATRLIN2:20;
hence xSUM = 0 iff x = 0.X by A1,EUCLID:7,EUCLID:8,MATRLIN:34;
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
ax = a1 * x1 by A1,A4; then
z4 = a1 * (x1 |-- b) by A4,MATRLIN2:18
.= a * z1 by A1;
hence axSUM = |.a.| * xSUM by A1,A4,EUCLID:11;
xy = x1 + x2 by A1,A2,A3;
then
z3 = (x1 |-- b) + (x2 |-- b) by A3,MATRLIN2:17
.= z1 + z2 by A1,A2;
hence xySUM <= xSUM + ySUM by A1,A2,A3,EUCLID:12;
end;
theorem Th22:
for X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp (X),
x be Element of X
st dim X <> 0
holds
(sum_norm(X,b)).x <= (dim X)* (max_norm(X,b)).x
& (max_norm(X,b)).x <= (euclid_norm(X,b)).x
& (euclid_norm(X,b)).x <= (sum_norm(X,b)).x
proof
let X be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp (X),
x be Element of X;
assume
A1: dim X <> 0;
consider x1 be Element of RLSp2RVSp (X),
z1 be Element of REAL (dim X) such that
A2: x = x1
& z1 = (x1 |-- b)
& (max_norm(X,b)).x = (max_norm(dim X)).z1 by Def3;
consider x2 be Element of RLSp2RVSp (X),
z2 be Element of REAL (dim X) such that
A3: x = x2
& z2 = (x2 |-- b)
& (sum_norm(X,b)).x = (sum_norm(dim X)).z2 by Def4;
consider x3 be Element of RLSp2RVSp (X),
z3 be Element of REAL dim X such that
A4: x = x3
& z3 = (x3 |-- b)
& (euclid_norm(X,b)).x = |.z3.| by Def5;
thus thesis by A1,A2,A3,A4,Th14;
end;
theorem Th23:
for V be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(V)
st dim V <> 0
holds
ex S be LinearOperator of V, REAL-NS(dim V)
st S is bijective
& for x be Element of RLSp2RVSp(V)
holds S.x = x |-- b
proof
let V be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(V);
assume
A1: dim V <> 0;
A2: dim RLSp2RVSp(V) = dim V by REAL_NS2:81;
set W = RLSp2RVSp(V);
consider T be linear-transformation of W,(dim V) -VectSp_over F_Real
such that
A3: T is bijective
& for x be Element of W
holds T.x = x |-- b by A2,REAL_NS2:63;
(dim V) -VectSp_over F_Real = RLSp2RVSp(RealVectSpace(Seg(dim V)))
by A1,REAL_NS2:83;
then
reconsider S = T as LinearOperator of V,RealVectSpace(Seg(dim V))
by REAL_NS2:84;
A4: the carrier of RealVectSpace(Seg(dim V))
= the carrier of RLSp2RVSp(RealVectSpace(Seg(dim V)))
.= the carrier of ((dim V) -VectSp_over F_Real) by A1,REAL_NS2:83;
A5: the RLSStruct of REAL-NS(dim V)
= the RLSStruct of TOP-REAL(dim V) by REAL_NS2:1
.= RealVectSpace(Seg(dim V)) by EUCLID:def 8;
then reconsider K = S as Function of the carrier of V,
the carrier of REAL-NS (dim V);
for x, y be Element of V
holds K.(x+y) = K.x + K.y
proof
let x, y be Element of V;
S is additive;
hence K.(x+y) = S.x + S.y
.= K.x + K.y by Th16;
end; then
A7: K is additive;
for a be Real,
x be VECTOR of V
holds K.(a*x) = a * K.x
proof
let a be Real;
let x be VECTOR of V;
thus K.(a*x) = a * S.x by LOPBAN_1:def 5
.= a * K.x by Th16;
end;
then K is homogeneous;
then reconsider K as LinearOperator of V,REAL-NS(dim V) by A7;
take K;
thus thesis by A3,A4,A5;
end;
theorem Th24:
for V be finite-dimensional RealNormSpace
st dim V <> 0
holds
ex S be LinearOperator of V, REAL-NS(dim V),
W be finite-dimensional VectSp of F_Real,
b be OrdBasis of W
st W = RLSp2RVSp(V)
& S is bijective
& for x be Element of W
holds S.x = x |-- b
proof
let V be finite-dimensional RealNormSpace;
assume
A1: dim V <> 0;
A2: RLSp2RVSp(V) is finite-dimensional
& dim RLSp2RVSp(V) = dim V by REAL_NS2:81;
reconsider W = RLSp2RVSp (V) as finite-dimensional VectSp of F_Real;
set b = the OrdBasis of W;
consider T be linear-transformation of W,(dim V) -VectSp_over F_Real
such that
A3: T is bijective
& for x be Element of W
holds T.x = x |-- b by A2,REAL_NS2:63;
(dim V) -VectSp_over F_Real
= RLSp2RVSp(RealVectSpace(Seg(dim V))) by A1,REAL_NS2:83;
then
reconsider S = T as LinearOperator of V,RealVectSpace(Seg(dim V))
by REAL_NS2:84;
A4: the carrier of RealVectSpace(Seg(dim V))
= the carrier of RLSp2RVSp(RealVectSpace(Seg(dim V)))
.= the carrier of ((dim V) -VectSp_over F_Real) by A1,REAL_NS2:83;
A5: the RLSStruct of REAL-NS(dim V)
= the RLSStruct of TOP-REAL(dim V) by REAL_NS2:1
.= RealVectSpace(Seg(dim V)) by EUCLID:def 8;
then
reconsider K = S as Function of the carrier of V,
the carrier of REAL-NS(dim V);
for x, y be Element of V
holds K.(x + y) = K.x + K.y
proof
let x, y be Element of V;
S is additive;
hence K.(x + y)
= S.x + S.y
.= K.x + K.y by Th16;
end; then
A7: K is additive;
for a be Real,
x be VECTOR of V
holds K.(a * x) = a * (K . x)
proof
let a be Real;
let x be VECTOR of V;
thus K.(a * x)
= a * S.x by LOPBAN_1:def 5
.= a * K.x by Th16;
end;
then K is homogeneous;
then reconsider K as LinearOperator of V,REAL-NS (dim V) by A7;
take K,W,b;
thus thesis by A3,A4,A5;
end;
theorem Th25:
for V be RealNormSpace,
W be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp(W)
st V is finite-dimensional
& dim V <> 0
& the RLSStruct of V = the RLSStruct of W
holds
ex k1,k2 be Real
st 0 < k1 & 0 < k2
& for x be Point of V
holds
||.x.|| <= k1 * max_norm(W,b).x
& max_norm(W,b).x <= k2 * ||.x.||
proof
let V be RealNormSpace,
W be finite-dimensional RealLinearSpace,
b be OrdBasis of RLSp2RVSp (W);
assume that
A1: V is finite-dimensional & dim V <> 0
and
A2: the RLSStruct of V = the RLSStruct of W;
A4: (Omega).V = the RLSStruct of V by RLSUB_1:def 4
.= (Omega).W by A2,RLSUB_1:def 4;
A5: dim V
= dim((Omega).V) by A1,RLVECT_5:30
.= dim W by A4,RLVECT_5:30;
reconsider e = b as FinSequence of W;
reconsider e1 = e as FinSequence of V by A2;
deffunc F3(Nat) = In(||.e1/.$1.||,REAL);
consider k be FinSequence of REAL such that
A6: len k = len b
& for i be Nat
st i in dom k
holds k.i = F3(i) from FINSEQ_2:sch 1;
set k1 = Sum(k);
for i be Nat st i in dom k holds 0 <= k.i
proof
let i be Nat;
assume i in dom k;
then
k.i = In(||.e1/.i.||,REAL) by A6
.= ||.e1/.i.||;
hence 0 <= k.i;
end;
then
A7: 0 <= k1 by RVSUM_1:84;
A8: for x be Point of V
holds ||.x.|| <= (k1 + 1) * max_norm(W,b).x
proof
let x0 be Point of V;
reconsider x = x0 as Point of W by A2;
consider y be Element of RLSp2RVSp(W),
z be Element of REAL(dim W) such that
A9: x = y
& z = y |-- b
& max_norm(W,b).x = (max_norm(dim W)).z by Def3;
reconsider yb = y |-- b as FinSequence of REAL;
A10:
now let i be Nat;
assume
A11: i in dom(yb);
then i in dom(abs(z)) by A9,VALUED_1:def 11;
then abs(z).i = |.z.i.| by VALUED_1:def 11
.= |.yb/.i.| by A9,A11,PARTFUN1:def 6;
hence |.yb/.i.| <= max_norm(W,b).x by A1,A5,A9,A11,Def1;
end;
A12: len(y |-- b) = len b by MATRLIN:def 7;
then
dom(y |-- b)
= Seg len b by FINSEQ_1:def 3
.= dom b by FINSEQ_1:def 3;
then
A13: dom(lmlt(y |-- b,b))
= dom(y |-- b) by MATRLIN:12
.= Seg len b by A12,FINSEQ_1:def 3;
reconsider f = (the Mult of W) .: (yb,e)
as FinSequence of the carrier of W;
reconsider f1 = f as FinSequence of V by A2;
A14: x = Sum(lmlt(y |-- b,b)) by A9,MATRLIN:35
.= Sum f1 by A2;
A15: len f = len b by A13,FINSEQ_1:def 3;
deffunc F4(Nat) = In(||.f1/.$1.||,REAL);
consider g be FinSequence of REAL such that
A16: len g = len f
& for i be Nat st i in dom g
holds g . i = F4(i) from FINSEQ_2:sch 1;
A17: for i be Element of NAT st i in dom f1
holds g.i = ||. f1 /. i .||
proof
let i be Element of NAT;
assume i in dom f1;
then i in Seg(len f) by FINSEQ_1:def 3;
then i in dom g by A16,FINSEQ_1:def 3;
then g.i = In(||.f1/.i.||,REAL) by A16;
hence thesis;
end;
then
A18: ||.x0.|| <= Sum (g) by NDIFF_5:7,A14,A16;
A19: for i be Nat st i in Seg len b
holds g.i <= ((max_norm(W,b).x)*k).i
proof
let i be Nat;
assume
A20: i in Seg len b;
A21: dom e = Seg(len b) by FINSEQ_1:def 3;
A22: dom yb = Seg(len b) by A12,FINSEQ_1:def 3; then
A23: yb.i = yb/.i by PARTFUN1:def 6,A20;
f1/. i
= f1.i by A13,A20,PARTFUN1:def 6
.= (the Mult of W).(yb.i,e.i) by A13,A20,FUNCOP_1:22
.= (yb/.i) * (e1/.i) by A2,A20,A21,A23,PARTFUN1:def 6;
then
A24: g.i
= ||.(yb/.i) * (e1/.i) .|| by A13,A20,A17
.= |.(yb/.i).| * ||.e1/.i.|| by NORMSP_1:def 1;
A25: |.(yb/.i).|* ||.e1/.i.||
<= (max_norm(W,b).x) * ||.e1/.i.||
by XREAL_1:64,A10,A20,A22;
i in dom k by A6,A20,FINSEQ_1:def 3;
then k.i = In(||.e1/.i.||,REAL) by A6
.= ||.e1/.i.||;
hence
g.i <= ((max_norm(W,b).x) * k).i by A24,A25,RVSUM_1:45;
end;
A26: g is (len b)-element by A15,A16,CARD_1:def 7;
dom((max_norm(W,b).x) * k)
= dom k by VALUED_1:def 5
.= Seg len b by A6,FINSEQ_1:def 3;
then len((max_norm(W,b).x) * k) = len b by FINSEQ_1:def 3;
then (max_norm(W,b).x) * k is (len b)-element by CARD_1:def 7;
then Sum(g) <= Sum((max_norm(W,b).x) * k) by A19,A26,RVSUM_1:82;
then Sum(g) <= (max_norm(W,b).x) * Sum(k) by RVSUM_1:87;
then
A27: ||.x0.|| <= k1 * (max_norm(W,b).x0) by A18,XXREAL_0:2;
A28: 0 <= max_norm(W,b).x by A1,A5,Th19;
k1 + 0 < k1 + 1 by XREAL_1:8;
then k1*(max_norm(W,b).x0) <= (k1+1)*(max_norm(W,b).x0)
by A28,XREAL_1:64;
hence ||.x0.|| <= (k1+1)*(max_norm(W,b).x0)
by A27,XXREAL_0:2;
end;
consider S0 be LinearOperator of W, REAL-NS(dim W) such that
A29: S0 is bijective
& for x be Element of RLSp2RVSp(W)
holds S0.x = x |-- b by A1,A5,Th23;
reconsider S = S0
as Function of the carrier of V, the carrier of REAL-NS (dim W) by A2;
for x, y be Element of V
holds S.(x + y) = S.x + S.y
proof
let x, y be Element of V;
reconsider x0 = x, y0 = y as Element of W by A2;
A30: x + y = x0 + y0 by A2;
S0 is additive;
hence S.(x + y) = S.x + S.y by A30;
end;
then
A32: S is additive;
for a be Real,
x be VECTOR of V
holds S.(a * x) = a * S.x
proof
let a be Real;
let x be VECTOR of V;
reconsider x0 = x as Element of W by A2;
a * x = a * x0 by A2;
hence S.(a * x) = a * S.x by LOPBAN_1:def 5;
end;
then S is homogeneous;
then reconsider S as LinearOperator of V,REAL-NS (dim W) by A32;
consider T be LinearOperator of REAL-NS (dim W),V such that
A34: T = S " & T is one-to-one onto by A29,REAL_NS2:85;
A35: for x be Element of V
holds ||.x.|| <= (k1+1) * ||.S.x.||
proof
let x0 be Element of V;
reconsider x = x0 as Element of W by A2;
reconsider Sx = S.x0 as Element of REAL dim(W) by REAL_NS1:def 4;
consider x1 be Element of RLSp2RVSp (W),
z1 be Element of REAL (dim W) such that
A36: x = x1
& z1 = x1 |-- b
& (euclid_norm(W,b)).x = |.z1.| by Def5;
(euclid_norm(W,b)).x = ||.S.x0.|| by A29,A36,REAL_NS1:1; then
A38: (k1 + 1) * (max_norm(W,b)).x <= (k1 + 1) * ||.S.x0.||
by A1,A5,A7,Th22,XREAL_1:64;
||.x0.|| <= (k1 + 1) * max_norm(W,b).x0 by A8;
hence ||.x0.|| <= (k1 + 1) * ||.S.x0.|| by A38,XXREAL_0:2;
end;
for y be Element of REAL-NS(dim W)
holds ||.T.y.|| <= (k1 + 1) * ||.y.||
proof
let y be Element of REAL-NS(dim W);
the carrier of REAL-NS(dim W) = rng S by A29,FUNCT_2:def 3;
then
consider x be Element of the carrier of V such that
A39: y = S.x by FUNCT_2:113;
T.y = x by A29,A34,A39,FUNCT_2:26;
hence ||.T.y.|| <= (k1 + 1) * ||.y.|| by A35,A39;
end;
then
A41: T is Lipschitzian by A7;
set CW = {y where y is Element of V : max_norm(W,b).y = 1 };
set CR = {x where x is Element of REAL-NS (dim W)
: (max_norm(dim W)).x = 1 };
for z be object
st z in CW
holds z in the carrier of V
proof
let z be object;
assume z in CW; then
ex y be Element of V
st z = y & max_norm(W,b).y = 1;
hence z in the carrier of V;
end;
then reconsider CW as Subset of V by TARSKI:def 3;
for z be object
st z in CR
holds z in the carrier of REAL-NS(dim W)
proof
let z be object;
assume z in CR; then
ex y be Element of REAL-NS(dim W)
st z = y & (max_norm(dim W)).y = 1;
hence z in the carrier of REAL-NS(dim W);
end;
then
reconsider CR as Subset of REAL-NS(dim W) by TARSKI:def 3;
REAL-NS(dim W) is non trivial by A1,A5;
then
consider zn be Point of REAL-NS(dim W) such that
A42: zn <> 0.(REAL-NS(dim W));
reconsider znn = zn as Element of REAL(dim W) by REAL_NS1:def 4;
zn <> 0*(dim W) by A42,REAL_NS1:def 4;
then
A43: (max_norm(dim W)).znn <> 0 by A1,A5,Th12; then
A44:0 < (max_norm(dim W)).zn by A1,A5,Th12;
set yn = (1 / (max_norm(dim W)).zn) * zn;
set a = 1 / (max_norm(dim W)).zn;
A45: (max_norm(dim W)).yn
= (max_norm(dim W)).(a * znn) by REAL_NS1:3
.= |.a.| * (max_norm(dim W)).znn by A1,A5,Th12;
|.a.| * (max_norm(dim W)).znn
= a * (max_norm(dim W)).zn by A44,COMPLEX1:43
.= 1 by XCMPLX_1:106,A43;
then
A46: yn in CR by A45;
A47: for y be object holds y in T.:CR iff y in CW
proof
let y be object;
hereby
assume y in T.:CR; then
consider x be object such that
A48: x in dom T & x in CR
& y = T.x by FUNCT_1:def 6;
reconsider x as Element of REAL-NS(dim W) by A48;
A49: ex x0 be Element of REAL-NS(dim W)
st x = x0 & (max_norm(dim W)).x0 = 1 by A48;
consider w be Element of RLSp2RVSp(W),
z be Element of REAL(dim W) such that
A50: T . x = w
& z = w |-- b
& max_norm(W,b).(T.x) = (max_norm(dim W)).z by A2,Def3;
w in the carrier of V by A50;
then
A51: w in dom S by FUNCT_2:def 1;
S.w = z by A29,A50;
then
A52: T.z = w by A29,A34,A51,FUNCT_1:34;
z in REAL(dim W); then
A53: z in the carrier of REAL-NS(dim W) by REAL_NS1:def 4;
dom T = the carrier of REAL-NS(dim W) by FUNCT_2:def 1;
then z = x by A34,A50,A52,A53,FUNCT_1:def 4;
hence y in CW by A48,A49,A50;
end;
assume
A54: y in CW;
then reconsider y0 = y as Element of V;
A55: ex y0 be Element of V
st y = y0 & max_norm(W,b).y0 = 1 by A54;
consider w be Element of RLSp2RVSp(W),
z be Element of REAL(dim W) such that
A56: y0 = w
& z = w |-- b
& max_norm(W,b).y0 = (max_norm(dim W)).z by A2,Def3;
w in the carrier of V by A56; then
A57: w in dom S by FUNCT_2:def 1;
z in REAL(dim W); then
A58: z in the carrier of REAL-NS(dim W) by REAL_NS1:def 4;
then
A59: z in dom T by FUNCT_2:def 1;
S.w = z by A29,A56;
then
A60: T.z = w by A29,A34,A57,FUNCT_1:34;
z in CR by A56,A55,A58;
hence y in T.:CR by A56,A59,A60,FUNCT_1:def 6;
end;
the carrier of REAL-NS(dim W) = REAL(dim W) by REAL_NS1:def 4;
then reconsider g = max_norm(dim W)
as Function of the carrier of REAL-NS(dim W),REAL;
set D = the carrier of REAL-NS(dim W);
A63: dom g = D by FUNCT_2:def 1;
A64: |.-1 .|
= |. 1 .| by COMPLEX1:52
.= 1 by COMPLEX1:43;
for x0 be Point of REAL-NS(dim W)
for r be Real st x0 in D & 0 < r
holds
ex s be Real st 0 < s
&
for x1 be Point of REAL-NS(dim W)
st x1 in D & ||.x1 - x0.|| < s
holds |.((g /. x1) - (g /. x0)).| < r
proof
let x0 be Point of REAL-NS(dim W);
let r be Real;
assume
A65: x0 in D & 0 < r;
set s = r;
take s;
thus 0 < s by A65;
let x1 be Point of REAL-NS(dim W);
assume
A66: x1 in D & ||.x1 - x0.|| < s;
A67: dom g = D by FUNCT_2:def 1;
reconsider y0 = x0 as Element of REAL(dim W)
by REAL_NS1:def 4;
reconsider y1 = x1 as Element of REAL(dim W) by REAL_NS1:def 4;
A68: ||.x1 - x0.|| = |.y1 - y0.| by REAL_NS1:1,REAL_NS1:5;
A69: (max_norm(dim W)).(y1 - y0) <= |.y1 - y0.| by A1,A5,Th14;
A70: x1 - x0 = y1 - y0 by REAL_NS1:5;
then
A71: y0 + (y1 - y0) = x0 + (x1 - x0) by REAL_NS1:2
.= y1 by RLVECT_4:1;
A72: x0 - x1 = y0 - y1 by REAL_NS1:5; then
A73: y1 + (y0 - y1) = x1 + (x0 - x1) by REAL_NS1:2
.= y0 by RLVECT_4:1;
y0 - y1
= -(x1 - x0) by A72,RLVECT_1:33
.= (-1) * (x1-x0) by RLVECT_1:16
.= (-1) * (y1-y0) by A70,REAL_NS1:3;
then
A74: (max_norm(dim W)).(y0-y1)
= |.-1 .| * (max_norm(dim W)).(y1-y0) by Th12,A1,A5
.= (max_norm(dim W)).(y1-y0) by A64;
A75: g.(y1-y0) = g/.(y1-y0) by A67,A70,PARTFUN1:def 6;
A76: g/.y1 = g.y1 by A67,PARTFUN1:def 6;
A77: g/.y0 = g.y0 by A67,PARTFUN1:def 6;
A78:(max_norm(dim W)).y1 - (max_norm(dim W)).y0
<= (max_norm(dim W)).y0 + (max_norm(dim W)).(y1-y0)
-(max_norm(dim W)).y0 by A1,A5,A71,Th12,XREAL_1:9;
(max_norm(dim W)).y1
- ((max_norm(dim W)).y1 + (max_norm(dim W)).(y0-y1))
<= (max_norm(dim W)).y1 - (max_norm(dim W)).y0
by A1,A5,A73,Th12,XREAL_1:10; then
- (max_norm(dim W)).(y1-y0)
<= (max_norm(dim W)).y1 - (max_norm(dim W)).y0 by A74;
then |. g/.y1 - g/.y0 .| <= g/.(y1 - y0) by A75,A76,A77,A78,ABSVALUE:5;
then |. g/.x1 - g/.x0 .| <= ||.x1 - x0.|| by A68,A69,A75,XXREAL_0:2;
hence |. g/.x1 - g/.x0 .| < s by A66,XXREAL_0:2;
end;
then
A79: g is_continuous_on the carrier of REAL-NS(dim W) by A63,NFCONT_1:20;
for s1 be sequence of REAL-NS(dim W)
st rng s1 c= CR & s1 is convergent
holds lim s1 in CR
proof
let s1 be sequence of REAL-NS (dim W);
assume
A80: rng s1 c= CR & s1 is convergent;
set D = the carrier of REAL-NS(dim W);
A82: g is_continuous_in (lim s1) by A79;
A83: dom s1=NAT by FUNCT_2:def 1;
A81: D = dom g by FUNCT_2:def 1; then
A84: rng s1 c= dom g;
then
A85: g/*s1 = g*s1 by FUNCT_2:def 11;
then
A86: dom(g/*s1) = dom s1 by A84,RELAT_1:27;
for x, y be object
st x in dom(g/*s1) & y in dom(g/*s1)
holds (g/*s1) . x = (g/*s1) . y
proof
let x, y be object;
assume
A87: x in dom(g/*s1) & y in dom(g/*s1);
then reconsider i = x, j = y as Element of NAT;
i in dom s1 by A84,A85,A87,RELAT_1:27;
then s1.i in rng s1 by FUNCT_1:3;
then s1.i in CR by A80;
then
ex x be Element of REAL-NS (dim W)
st s1.i = x & (max_norm(dim W)).x = 1;
then
A88: (g/*s1).x = 1 by A84,FUNCT_2:108;
j in dom s1 by A87,A85,A84,RELAT_1:27;
then s1.j in rng s1 by FUNCT_1:3;
then s1.j in CR by A80;
then
ex x be Element of REAL-NS (dim W)
st s1.j = x & (max_norm(dim W)).x = 1;
hence thesis by A84,FUNCT_2:108,A88;
end;
then
A89: g/*s1 is constant by FUNCT_1:def 10;
A90: (g/*s1).1 in rng (g/*s1)
& (g/*s1).1 = g.(s1.1)
by A83,A84,A86,FUNCT_1:3,FUNCT_2:108;
s1.1 in rng s1 by A83,FUNCT_1:3;
then s1.1 in CR by A80;
then
A92: ex x be Element of REAL-NS (dim W)
st s1.1 = x & (max_norm(dim W)).x = 1;
(max_norm(dim W)).(lim s1)
= lim (g/*s1) by A80,A81,A82
.= 1 by A89,A90,A92,SEQ_4:25;
hence lim s1 in CR;
end;
then
A93: CR is closed;
A95: 0 + dim W < 1 + dim W by XREAL_1:8;
A94: ex r be Real
st for y be Point of REAL-NS(dim W)
st y in CR
holds ||.y.|| < r
proof
set r = 1 + dim W;
take r;
let y be Point of REAL-NS(dim W);
assume y in CR;
then
A96: ex z be Element of REAL-NS(dim W)
st y = z & (max_norm(dim W)).z = 1;
reconsider y0 = y as Element of REAL(dim W) by REAL_NS1:def 4;
(sum_norm(dim W)).y0 <= (dim W) * (max_norm(dim W)).y0
&
(max_norm(dim W)).y0 <= |.y0.|
&
|.y0.| <= (sum_norm(dim W)).y0 by A1,A5,Th14;
then |.y0.| <= (dim W) * (max_norm(dim W)).y0 by XXREAL_0:2;
then ||.y.|| <= (dim W) by A96,REAL_NS1:1;
hence ||.y.|| < r by A95,XXREAL_0:2;
end;
A97: T is_continuous_on CR by A41,LOPBAN_5:4,NFCONT_1:23;
CW = T.:CR by A47,TARSKI:2; then
A98: CW is compact by A93,A94,A97,Lm3,NFCONT_1:32;
reconsider f = id CW as PartFunc of V,V;
dom f = CW;
then
A99: f is_continuous_on CW by NFCONT_1:50;
dom T = the carrier of REAL-NS(dim W) by FUNCT_2:def 1;
then
A100: CW <> {} by A47,TARSKI:2,A46;
A101: dom f = dom ||.f.|| by NORMSP_0:def 3;
then
A102: rng ||.f.|| is compact by A98,A99,NFCONT_1:28,NFCONT_1:31;
rng ||.f.|| <> {} by A101,A100,RELAT_1:42;
then consider y0 be Element of V such that
A104: y0 in dom ||.f.||
& lower_bound(rng ||.f.||) = ||.f.|| . y0
by A102,PARTFUN1:3,RCOMP_1:14;
A107: ||.f.|| . y0 = ||.f/.y0.|| by A104,NORMSP_0:def 3;
rng ||.f.|| is real-bounded by A102,RCOMP_1:10;
then rng ||.f.|| is bounded_below by XXREAL_2:def 11;
then
A105: for r be Real st r in (rng ||.f.||)
holds ||.f.|| . y0 <= r by A104,SEQ_4:def 2;
set k2 = ||.f/.y0.||;
A108: for x be Element of V
st x in CW
holds k2 <= ||.x.||
proof
let x be Element of V;
assume
A109: x in CW; then
f/.x = f.x by A101,PARTFUN1:def 6
.= x by A109,FUNCT_1:18; then
||.f.|| . x = ||.x.|| by A101,A109,NORMSP_0:def 3;
hence k2 <= ||.x.|| by A101,A105,A107,A109,FUNCT_1:3;
end;
A113: k2 <> 0
proof
assume k2=0; then
consider x be Element of V such that
A114: x in dom ||.f.|| & 0 = ||.f.||.x by A104,A107;
||.f.||.x = ||.f/.x.|| by NORMSP_0:def 3,A114;
then f/.x = 0.V by A114,NORMSP_0:def 5;
then f.x = 0.V by A101,A114,PARTFUN1:def 6;
then 0.V in CW by A101,A114,FUNCT_1:18;
then
A115: ex y be Element of V st y= 0.V & max_norm(W,b).y = 1;
max_norm(W,b).(0.V)
= max_norm(W,b).(0.W) by A2
.= 0 by A1,A5,Th19;
hence contradiction by A115;
end;
then
A116: 0 < 1/k2 by XREAL_1:139;
for x be Point of V
holds max_norm(W,b).x <= (1/k2)*||.x.||
proof
let x be Element of V;
reconsider xn = x as Element of W by A2;
per cases;
suppose
x = 0.V; then
max_norm(W,b).x
= max_norm(W,b).(0.W) by A2
.= 0 by A1,A5,Th19;
hence max_norm(W,b).x <= (1/k2)*||.x.||;
end;
suppose
x<> 0.V;
then xn <> 0.W by A2;
then
A118: (max_norm(W,b)).xn <> 0 by A1,A5,Th19; then
A119: 0 < (max_norm(W,b)).xn by A1,A5,Th19;
set y = (1/max_norm(W,b).x) * x;
set a = 1/(max_norm(W,b)).x;
a * x = a * xn by A2;
then
A120: (max_norm(W,b)).y = |.a.| *(max_norm(W,b)).xn by A1,A5,Th19;
|.a.| * (max_norm(W,b)).xn
= a* (max_norm(W,b)).xn by A119,COMPLEX1:43
.= 1 by A118,XCMPLX_1:106; then
y in CW by A120; then
A123: k2 * (max_norm(W,b).x) <= ||.y.|| * (max_norm(W,b).x)
by A108,XREAL_1:64,A119;
||.y.|| = |.1 / (max_norm(W,b).x).| * ||.x.|| by NORMSP_1:def 1
.= 1 / (max_norm(W,b).x) * ||.x.|| by A119,COMPLEX1:43; then
||.y.|| * (max_norm(W,b).x)
= (1/ (max_norm(W,b).x))*(max_norm(W,b).x) *||.x.||
.= 1 * ||.x.|| by A118,XCMPLX_1:106
.= ||.x.||;
then (1/k2) * (k2 * (max_norm(W,b).x)) <= (1/k2) * ||.x.||
by A123,XREAL_1:64;
then (1/k2) * k2 * ((max_norm(W,b)).x) <= (1/k2) * ||.x.||;
then 1 * (max_norm(W,b).x) <= (1/k2) * ||.x.||
by A113,XCMPLX_1:106;
hence (max_norm(W,b).x) <= (1/k2)*||.x.||;
end;
end;
hence thesis by A7,A8,A116;
end;
theorem
for X, Y be RealNormSpace
st the RLSStruct of X = the RLSStruct of Y
& X is finite-dimensional
& dim X <> 0
holds
ex k1,k2 be Real
st 0 < k1
& 0 < k2
& for x be Element of X,
y be Element of Y
st x = y
holds
||.x.|| <= k1 * ||.y.||
& ||.y.|| <= k2 * ||.x.||
proof
let X, Y be RealNormSpace;
assume
A1: the RLSStruct of X = the RLSStruct of Y
& X is finite-dimensional
& dim X <> 0;
set X0 = (Omega).X;
set Y0 = (Omega).Y;
A2: X0 = the RLSStruct of X by RLSUB_1:def 4;
reconsider X0 as finite-dimensional RealLinearSpace by A1;
A3: dim X = dim X0 by A1,RLVECT_5:30;
Y0 = the RLSStruct of Y by RLSUB_1:def 4; then
A4: Y is finite-dimensional by A1,RLAFFIN3:3,A2;
reconsider Y0 as finite-dimensional RealLinearSpace
by A1,A2,RLSUB_1:def 4;
X0 = Y0 by A1,A2,RLSUB_1:def 4; then
A6: dim X = dim Y by A3,A4,RLVECT_5:30;
set b = the OrdBasis of RLSp2RVSp(X0);
reconsider e = b as OrdBasis of RLSp2RVSp(Y0) by A1,A2,RLSUB_1:def 4;
consider k1,k2 be Real such that
A7: 0 < k1 & 0 < k2
& for x be Point of X
holds
||.x.|| <= k1 * max_norm(X0,b).x
& max_norm(X0,b).x <= k2 * ||.x.|| by A1,A2,Th25;
Y0 = the RLSStruct of Y by RLSUB_1:def 4; then
consider j1,j2 be Real such that
A8: 0 < j1 & 0 < j2
& for x be Point of Y
holds
||.x.|| <= j1 * max_norm(Y0,e).x
& max_norm(Y0,e).x <= j2 * ||.x.|| by A1,A4,A6,Th25;
A9:
now let x be Element of X,
y be Element of Y;
assume x = y; then
A12: max_norm(X0,b).x = max_norm(Y0,e).y by A1,A2,RLSUB_1:def 4;
A11: ||.x.|| <= k1 * max_norm(X0,b).x
& max_norm(X0,b).x <= k2 * ||.x.||
& ||.y.|| <= j1 * max_norm(Y0,e).y
& max_norm(Y0,e).y <= j2 * ||.y.|| by A7,A8;
k1 * max_norm(Y0,e).y <= k1 * (j2 * ||.y.||) by A7,A8,XREAL_1:64;
hence ||.x.|| <= k1 * j2 * ||.y.|| by A11,A12,XXREAL_0:2;
j1 * max_norm(X0,b).x <= j1 * (k2 * ||.x.||) by A7,A8,XREAL_1:64;
hence ||.y.|| <= j1 * k2 * ||.x.|| by A11,A12,XXREAL_0:2;
end;
set h1 = k1 * j2;
set h2 = j1 * k2;
take h1,h2;
thus 0 < h1 & 0 < h2 by A7,A8,XREAL_1:129;
thus thesis by A9;
end;
theorem Th27:
for V be RealNormSpace
st V is finite-dimensional & dim V <> 0
holds
ex k1,k2 be Real,
S be LinearOperator of V, REAL-NS(dim V)
st S is bijective
& 0 <= k1
& 0 <= k2
& for x be Element of V
holds
||.S.x.|| <= k1 * ||.x.||
& ||.x.|| <= k2 * ||.S.x.||
proof
let V be RealNormSpace;
assume
A1: V is finite-dimensional & dim V <> 0;
then
consider S be LinearOperator of V, REAL-NS(dim V),
W be finite-dimensional VectSp of F_Real,
b be OrdBasis of W such that
A2: W = RLSp2RVSp(V)
& S is bijective
& for x be Element of W
holds S.x = x |-- b by Th24;
reconsider V0 = V as finite-dimensional RealLinearSpace by A1;
reconsider b0 = b as OrdBasis of RLSp2RVSp(V0) by A2;
the RLSStruct of V0 = the RLSStruct of V; then
consider k1,k2 be Real such that
A4: 0 < k1 & 0 < k2
& for x be Point of V
holds ||.x.|| <= k1 * max_norm(V0,b0).x
& max_norm(V0,b0).x <= k2 * ||.x.|| by Th25,A1;
A5:
now
let x be Element of V;
reconsider Sx = S.x as Element of REAL dim(V) by REAL_NS1:def 4;
consider x1 be Element of RLSp2RVSp(V0),
z1 be Element of REAL(dim V0) such that
A6: x = x1
& z1 = x1 |-- b0
& (euclid_norm(V0,b0)).x = |.z1.| by Def5;
A8: (euclid_norm(V0,b0)).x = ||.S.x.|| by A2,A6,REAL_NS1:1;
(sum_norm(V0,b0)).x <= (dim V) * (max_norm(V0,b0)).x
&
(max_norm(V0,b0)).x <= (euclid_norm(V0,b0)).x
&
(euclid_norm(V0,b0)).x <= (sum_norm(V0,b0)).x by Th22,A1;
then
A9: ||.S.x.|| <= (dim V0) * (max_norm(V0,b0)).x by A8,XXREAL_0:2;
(dim V0) * max_norm(V0,b0).x <= (dim V0) * (k2 * ||.x.||)
by A4,XREAL_1:64;
hence ||.S.x.|| <= (dim V0) * k2 * ||.x.|| by A9,XXREAL_0:2;
A10: k1 * (max_norm(V0,b0)).x <= k1 * ||.S.x.||
by A1,A4,A8,Th22,XREAL_1:64;
||.x.|| <= k1 * max_norm(V0,b0).x by A4;
hence ||.x.|| <= k1 * ||.S.x.|| by A10,XXREAL_0:2;
end;
set h1 = (dim V0) * k2;
take h1,k1,S;
thus S is bijective by A2;
thus 0 <= h1 & 0 <= k1 by A4;
thus thesis by A5;
end;
begin :: Linear Isometry and Its Topological Properties
definition
let V,W be RealNormSpace,
L be LinearOperator of V,W;
attr L is isometric-like means
ex k1,k2 be Real
st 0 <= k1 & 0 <= k2
& for x be Element of V
holds
||.L.x.|| <= k1 * ||.x.||
& ||.x.|| <= k2 * ||.L.x.||;
end;
theorem Th28:
for V be finite-dimensional RealNormSpace
st dim V <> 0
holds
ex L be LinearOperator of V,REAL-NS(dim V)
st L is one-to-one onto isometric-like
proof
let V be finite-dimensional RealNormSpace;
assume dim V <> 0; then
consider k1,k2 be Real,
S be LinearOperator of V, REAL-NS(dim V) such that
A1: S is bijective
& 0 <= k1
& 0 <= k2
& for x be Element of V
holds
||.S.x.|| <= k1 * ||.x.||
& ||.x.|| <= k2 * ||.S.x.|| by Th27;
take S;
thus S is one-to-one onto by A1;
thus S is isometric-like by A1;
end;
theorem Th29:
for V,W be RealNormSpace,
L be LinearOperator of V,W
st L is one-to-one onto isometric-like
holds
ex K be LinearOperator of W,V
st K = L"
& K is one-to-one onto isometric-like
proof
let V,W be RealNormSpace,
L be LinearOperator of V,W;
assume
A1: L is one-to-one onto isometric-like;
consider K be LinearOperator of W,V such that
A2: K = L" & K is one-to-one onto by A1,REAL_NS2:85;
take K;
thus K = L" by A2;
thus K is one-to-one onto by A2;
consider k1,k2 be Real such that
A3: 0 <= k1 & 0 <= k2
& for x be Element of V
holds ||.L.x.|| <= k1 * ||.x.||
& ||.x.|| <= k2 * ||.L.x.|| by A1;
for y be Element of W
holds ||.K.y.|| <= k2 * ||.y.||
& ||.y.|| <= k1 * ||.K.y.||
proof
let y be Element of W;
the carrier of W = rng L by A1,FUNCT_2:def 3;
then
consider x be Element of the carrier of V such that
A4: y = L.x by FUNCT_2:113;
A5: K.y = x by A1,A2,A4,FUNCT_2:26;
hence ||.K.y.|| <= k2 * ||.y.|| by A3,A4;
thus ||.y.|| <= k1 * ||.K.y.|| by A3,A4,A5;
end;
hence K is isometric-like by A3;
end;
theorem Th30:
for V,W be RealNormSpace,
L be LinearOperator of V,W
st L is one-to-one onto isometric-like
holds L is Lipschitzian;
theorem
for V,W be RealNormSpace,
L be LinearOperator of V,W
st L is one-to-one onto isometric-like
holds L is_continuous_on the carrier of V by Th30,LOPBAN_7:6;
theorem Th32:
for S, T be RealNormSpace,
I be LinearOperator of S,T,
x be Point of S
st I is one-to-one onto isometric-like
holds I is_continuous_in x
proof
let S, T be RealNormSpace,
I be LinearOperator of S,T,
x be Point of S;
assume I is one-to-one onto isometric-like;
then I is_continuous_on the carrier of S by Th30,LOPBAN_7:6;
hence thesis;
end;
theorem Th33:
for S, T be RealNormSpace,
I be LinearOperator of S,T,
Z be Subset of S
st I is one-to-one onto isometric-like
holds I is_continuous_on Z
proof
let S, T be RealNormSpace;
let I be LinearOperator of S,T,
Z be Subset of S;
assume
A1: I is one-to-one onto isometric-like;
A2: dom I = the carrier of S by FUNCT_2:def 1;
for x be Point of S st x in dom I holds
I | (dom I) is_continuous_in x by A1,Th32;
hence thesis by A2,NFCONT_1:23,NFCONT_1:def 7;
end;
theorem Th34:
for S, T be RealNormSpace,
I be LinearOperator of S, T,
s1 be sequence of S
st I is one-to-one onto isometric-like
& s1 is convergent
holds
I * s1 is convergent
&
lim (I*s1) = I.lim s1
proof
let S, T be RealNormSpace;
let I be LinearOperator of S, T, s1 be sequence of S;
assume
A1: I is one-to-one onto isometric-like
& s1 is convergent;
dom I = the carrier of S by FUNCT_2:def 1; then
A3: rng s1 c= dom I;
I is_continuous_in lim s1 by A1,Th32;
then I/*s1 is convergent & I/.lim s1 = lim (I/*s1) by A1,A3;
hence thesis by A3,FUNCT_2:def 11;
end;
theorem Th35:
for S, T be RealNormSpace,
I be LinearOperator of S, T,
s1 be sequence of S
st I is one-to-one onto isometric-like holds
(s1 is convergent iff I*s1 is convergent)
proof
let S, T be RealNormSpace;
let I be LinearOperator of S, T,
s1 be sequence of S;
assume A1: I is one-to-one onto isometric-like;
then
consider J be LinearOperator of T, S such that
A2: J = I" & J is one-to-one onto isometric-like by Th29;
A3: rng I = the carrier of T by A1,FUNCT_2:def 3;
thus s1 is convergent implies I*s1 is convergent by Th34,A1;
assume A4: I*s1 is convergent;
A5: rng s1 c= the carrier of S;
J*(I*s1) = (J*I)*s1 by RELAT_1:36
.= (id (the carrier of S))*s1 by A1,A2,A3,FUNCT_2:29
.= s1 by RELAT_1:53,A5;
hence s1 is convergent by A2,A4,Th34;
end;
Lm4:
for S,T be RealNormSpace,
I be LinearOperator of S,T,
Z be Subset of S
st I is one-to-one onto isometric-like
& Z is closed
holds I.:Z is closed
proof
let S, T be RealNormSpace;
let I be LinearOperator of S,T,
Z be Subset of S;
assume that
A1: I is one-to-one onto
and
A2: I is isometric-like
and
A3: Z is closed;
A4: dom I = the carrier of S by FUNCT_2:def 1;
consider J be LinearOperator of T, S such that
A5: J = I" & J is one-to-one onto isometric-like by A1,A2,Th29;
A6: rng I = the carrier of T by A1,FUNCT_2:def 3;
now
let t1 be sequence of T;
assume
A7: rng t1 c= I.:Z &
t1 is convergent; then
A8: J * t1 is convergent by A5,Th35;
A9: rng(J * t1) = J.: rng t1 by RELAT_1:127;
J.: (I.:Z)
= I"(I.:Z) by A1,A5,FUNCT_1:85
.= Z by A1,A4,FUNCT_1:94;
then lim (J*t1) in Z by A3,A7,A8,A9,RELAT_1:123;
then J.(lim t1) in Z by A5,A7,Th34;
then I.(J.(lim t1)) in I.: Z by FUNCT_2:35;
hence lim t1 in I.: Z by A1,A5,A6,FUNCT_1:35;
end;
hence I.:Z is closed;
end;
theorem Th36:
for S,T be RealNormSpace,
I be LinearOperator of S,T,
Z be Subset of S
st I is one-to-one onto isometric-like
holds
Z is closed iff I.:Z is closed
proof
let S,T be RealNormSpace;
let I be LinearOperator of S,T,
Z be Subset of S;
assume that
A1: I is one-to-one onto
and
A2: I is isometric-like;
A3: dom I = the carrier of S by FUNCT_2:def 1;
consider J be LinearOperator of T, S such that
A4: J = I" & J is one-to-one onto isometric-like by A1,A2,Th29;
thus Z is closed iff I.:Z is closed
proof
thus Z is closed implies I.:Z is closed by A1,A2,Lm4;
assume
A5: I.:Z is closed;
J.: (I.:Z) = I"(I.:Z) by A1,A4,FUNCT_1:85
.= Z by A1,A3,FUNCT_1:94;
hence Z is closed by A4,A5,Lm4;
end;
end;
theorem
for S,T be RealNormSpace,
I be LinearOperator of S,T,
Z be Subset of S
st I is one-to-one onto isometric-like
holds Z is open iff I.:Z is open
proof
let S, T be RealNormSpace;
let I be LinearOperator of S,T,
Z be Subset of S;
assume that
A1: I is one-to-one onto
and
A2: I is isometric-like;
consider J be LinearOperator of T, S such that
A3: J = I" & J is one-to-one onto isometric-like by A1,A2,Th29;
A4: I = J" by A1,A3,FUNCT_1:43;
A5: J"Z
= (J").:Z by A3,FUNCT_1:85
.= I.:Z by A1,A3,FUNCT_1:43;
I.:(Z`)
= J"(Z`) by A4,A3,FUNCT_1:85
.= (I.:Z)` by A5,FUNCT_2:100;
hence Z is open iff I.:Z is open by A1,A2,Th36;
end;
Lm5:
for S, T be RealNormSpace,
I be LinearOperator of S, T,
Z be Subset of S
st I is one-to-one onto isometric-like
& Z is compact
holds I.:Z is compact
proof
let S, T be RealNormSpace;
let I be LinearOperator of S, T,
Z be Subset of S;
assume
A1: I is one-to-one onto isometric-like
& Z is compact;
dom I = the carrier of S by FUNCT_2:def 1;
hence I.:Z is compact by A1,Th33,NFCONT_1:32;
end;
theorem Th38:
for S,T be RealNormSpace,
I be LinearOperator of S,T,
Z be Subset of S
st I is one-to-one onto isometric-like
holds Z is compact iff I.:Z is compact
proof
let S, T be RealNormSpace;
let I be LinearOperator of S,T,
Z be Subset of S;
assume that
A1: I is one-to-one onto
and
A2: I is isometric-like;
consider J be LinearOperator of T, S such that
A3: J = I" & J is one-to-one onto isometric-like by A1,A2,Th29;
A4: dom I = the carrier of S by FUNCT_2:def 1;
thus Z is compact implies I.:Z is compact by A1,Lm5,A2;
thus I.:Z is compact implies Z is compact
proof
assume
A5: I.:Z is compact;
J.:(I.:Z) = I"(I.:Z) by A1,A3,FUNCT_1:85
.= Z by A1,A4,FUNCT_1:94;
hence Z is compact by A3,A5,Lm5;
end;
end;
theorem
for V be finite-dimensional RealNormSpace,
X be Subset of V
st dim V <> 0
holds
X is compact
iff
X is closed
&
ex r be Real
st for y be Point of V st y in X
holds ||.y.|| < r
proof
let V be finite-dimensional RealNormSpace;
let X be Subset of V;
assume
A1: dim V <> 0;
thus X is compact implies X is closed
&
ex r be Real
st for y be Point of V st y in X
holds ||.y.|| < r by Th6;
assume
A2: X is closed
&
ex r be Real
st for x be Point of V st x in X
holds ||.x.|| < r;
then consider r be Real such that
A3: for x be Point of V st x in X
holds ||.x.|| < r;
consider S be LinearOperator of V,REAL-NS(dim V) such that
A4: S is one-to-one onto isometric-like by A1,Th28;
consider k1,k2 be Real such that
A5: 0 <= k1
& 0 <= k2
& for x be Element of V
holds ||.S.x.|| <= k1 * ||.x.||
& ||.x.|| <= k2*||.S.x.|| by A4;
A6: S.:X is closed by A2,A4,Th36;
reconsider r2 = k1 * r + 1 as Real;
for y be Point of REAL-NS(dim V) st y in S.:X
holds ||.y.|| < r2
proof
let y be Point of REAL-NS(dim V);
assume y in S.:X;
then consider x be object such that
A7: x in dom S
& x in X
& y = S.x by FUNCT_1:def 6;
reconsider x as Point of V by A7;
A8: ||.S.x.|| <= k1 * ||.x.|| by A5;
||.x.|| < r by A3,A7;
then k1 * ||.x.|| <= k1 * r by XREAL_1:64,A5;
then ||.S.x.|| <= k1 * r by XXREAL_0:2,A8;
then ||.S.x.|| + 0 < k1 * r + 1 by XREAL_1:8;
hence ||.y.|| < r2 by A7;
end; then
S.:X is compact by A6,Lm3;
hence X is compact by A4,Th38;
end;