:: Continuity of Multilinear Operator on Normed Linear Spaces
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received February 27, 2019
:: Copyright (c) 2019-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 LOPBAN10, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC,
PARTFUN1, FUNCT_1, ORDINAL4, ORDINAL1, NEWTON, NAT_1, SUBSET_1, SEQ_1,
RSSPACE3, FINSEQ_2, RELAT_1, LOPBAN_1, SQUARE_1, TARSKI, ARYTM_3,
VALUED_1, GROUP_2, FUNCT_4, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1,
STRUCT_0, CARD_1, SEQ_4, METRIC_1, XXREAL_0, XBOOLE_0, FINSEQ_1,
CFCONT_1, PRVECT_1, RVSUM_1, PRVECT_2, CARD_3, PDIFF_1, REWRITE1, POWER,
COMPLEX1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCT_7, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1,
CARD_3, NAT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_1, NAT_D, SEQ_1,
SEQ_2, SEQ_4, NEWTON, POWER, STRUCT_0, PRE_TOPC, RLVECT_1, RSSPACE3,
NORMSP_0, NORMSP_1, RVSUM_1, EUCLID, LOPBAN_1, LOPBAN_5, NFCONT_1,
PRVECT_1, PRVECT_2, NDIFF_5, LOPBAN10;
constructors SQUARE_1, SEQ_2, SEQ_4, NFCONT_1, COMSEQ_2, RELSET_1, NAT_D,
SERIES_1, RSSPACE3, NDIFF_5, NEWTON, ABIAN, NDIFF_8, MONOID_0, SEQ_1,
LOPBAN_5, REAL_1, PARTFUN3, LOPBAN10, FOMODEL0;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0,
VALUED_1, FINSEQ_1, FINSEQ_2, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1,
ORDINAL1, INT_1, PRVECT_2, XXREAL_0, NORMSP_0, NAT_1, NORMSP_1, SQUARE_1,
RLVECT_1, MONOID_0, RVSUM_1, XCMPLX_0, PARTFUN3, SEQ_2, POWER, LOPBAN10,
NEWTON, PRVECT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions LOPBAN10;
equalities RLVECT_1, NORMSP_0, EUCLID, SQUARE_1, FINSEQ_1, XCMPLX_0, FINSEQ_2,
STRUCT_0, LOPBAN_5, LOPBAN10;
expansions FINSEQ_1, LOPBAN_1, NFCONT_1, LOPBAN10;
theorems TARSKI, RLVECT_1, RELAT_1, FUNCT_1, SQUARE_1, FUNCT_2, ORDINAL1,
FINSEQ_1, LOPBAN_1, PARTFUN1, NFCONT_1, VECTSP_1, SEQ_2, COMPLEX1, POWER,
XXREAL_0, INT_1, NAT_1, XCMPLX_1, FINSEQ_2, ABSVALUE, NORMSP_0, SEQ_1,
RSSPACE3, RLVECT_4, NDIFF_8, FUNCOP_1, XCMPLX_0, XREAL_0, SEQ_4,
NORMSP_1, VALUED_1, XREAL_1, RVSUM_1, PRVECT_2, FUNCT_7, CARD_3, NAT_4,
PREPOWER, LOPBAN10, NAT_D, RVSUM_3, RSSPACE2, FINSEQ_9, PRVECT_1;
schemes FUNCT_2, SEQ_1, NAT_1, FINSEQ_1, FINSEQ_4;
begin :: Completeness of the Space of Multilinear Operators
theorem NDIFF825: :::: preliminaries
for n be Nat, r be Real st 0 < r
ex s be Real st 0 < s & s < r & sqrt((s*s) * n) < r
proof
let n be Nat, r be Real;
assume
A1: 0 < r;
per cases;
suppose
A2: 0 = n;
set s = r/2;
take s;
thus 0 < s & s < r & sqrt((s*s)*n) < r
by A1,A2,XREAL_1:216;
end;
suppose
A3: 0 <> n;
set s = r/(n+1);
take s;
set s = r/(n+1);
A4: n + 0 < n + 1 by XREAL_1:8;
thus 0 < s by A1;
0+1 <= n by A3,NAT_1:13; then
1*n <= n*n by XREAL_1:66; then
A6: (s*s)*n <= s*s*(n*n) by XREAL_1:66;
0 < 1 & 0 + 1 < n + 1 by A3,XREAL_1:8; then
1/(n+1) < 1 by XREAL_1:191; then
1/(n+1) * r < r*1 by A1,XREAL_1:68;
hence s < r;
sqrt((s*s)*n) <= sqrt((s*n)^2) by A6,SQUARE_1:26; then
A8: sqrt((s*s)*n) <= s*n by A1,SQUARE_1:22;
n/(n+1) < 1 by A4,XREAL_1:191; then
n/(n+1) * r < r*1 by A1,XREAL_1:68;
hence sqrt((s*s)*n) < r by A8,XXREAL_0:2;
end;
end;
theorem LM03:
for R1,R2 be FinSequence of REAL,
n,i be Nat,
r be Real st i in dom R1
& R1 = n |-> (1 qua Real)
& R2 = R1 +* (i,r)
holds Product R2 = r
proof
let R1,R2 be FinSequence of REAL,
n,i be Nat,
r be Real;
assume that
A1: i in dom R1 and
A2: R1 = n |-> (1 qua Real) and
A3: R2 = R1 +* (i,r);
i in Seg n by A1,A2,FUNCT_2:def 1; then
A4: R1.i = 1 by A2,FUNCOP_1:7;
A5: Product R1 = 1 by A2,RVSUM_1:102;
thus Product R2 = ((Product R1) * r) / (R1 . i) by A1,A2,A3,RVSUM_3:25
.= r by A4,A5;
end;
theorem ::::
for F being FinSequence of REAL st (for k being Element of NAT
st k in dom F holds 0 <= F.k) holds 0 <= Product F
proof
defpred P[Nat] means for F being FinSequence of REAL st (for k
being Element of NAT st k in dom F holds 0 <= F.k)
& len F = $1 holds 0 <= Product F;
let F be FinSequence of REAL;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
for F being FinSequence of REAL st (for k being Element of NAT st k in
dom F holds 0 <= F.k) & len F = n+1 holds 0 <= Product F
proof
let F be FinSequence of REAL;
assume
A3: for k being Element of NAT st k in dom F holds 0 <= F.k;
assume
A4: len F = n+1; then
consider F1,F2 being FinSequence of REAL such that
A5: len F1 = n and
A6: len F2 = 1 and
A7: F = F1^F2 by FINSEQ_2:23;
1 in Seg 1; then
1 in dom F2 by A6,FINSEQ_1:def 3; then
A8: F.(n+1) = F2.1 by A5,A7,FINSEQ_1:def 7;
for k being Element of NAT st k in dom F1 holds 0 <= F1.k
proof
let k be Element of NAT;
assume
A9: k in dom F1; then
0 <= F.k by A3,A7,FINSEQ_2:15;
hence thesis by A7,A9,FINSEQ_1:def 7;
end; then
A10: 0 <= Product F1 by A2,A5;
set x = F2.1;
Seg (n+1) = dom F by A4,FINSEQ_1:def 3; then
A11: 0 <= x by A3,A8,FINSEQ_1:3;
Product F = Product (F1^<*x*>) by A6,A7,FINSEQ_1:40
.= Product F1 * x by RVSUM_1:96;
hence thesis by A10,A11;
end;
hence thesis;
end;
A12: P[0]
proof let F be FinSequence of REAL such that
for k being Element of NAT st k in dom F holds 0 <= F.k;
assume len F = 0; then
F = <*>REAL;
hence thesis by RVSUM_1:94;
end;
A13: for n being Nat holds P[n] from NAT_1:sch 2(A12,A1);
A14: ex n being Element of NAT st n = len F;
assume for k being Element of NAT st k in dom F holds 0 <= F.k;
hence thesis by A13,A14;
end;
::: generalize NAT_4:54 in FINSEQ_9:34
reserve X,G for RealNormSpace-Sequence,
Y for RealNormSpace;
reserve f for MultilinearOperator of X,Y;
theorem DCARXX: ::: should be proven before
dom carr X = dom X
proof
dom carr X = Seg len carr X by FINSEQ_1:def 3;
hence dom carr X = Seg len X by PRVECT_1:def 11
.= dom X by FINSEQ_1:def 3;
end;
theorem ZERXI:
for z be Element of product X st z = 0.product X
holds for i be Element of dom X holds z.i = 0.(X.i)
proof
let z be Element of product X;
assume
A1: z = 0.product X;
let i be Element of dom X;
A2: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
reconsider j = i as Element of dom carr X by DCARXX;
(zeros X).j = 0.(X.j) by PRVECT_1:def 14;
hence z.i = 0.(X.i) by A1,A2;
end;
theorem FXZER:
f.(0.product X) = 0.Y
proof
A1: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
reconsider z = 0.product X as Element of product carr X by A1;
set i = the Element of dom X;
z.i = 0.(X.i) by ZERXI;
hence f.(0.product X) = 0.Y by LOPBAN10:36;
end;
theorem PSPROD: ::: LOPBAN10 lemma; NAT_4:42
for F be FinSequence of REAL
st for i be Element of dom F holds F.i > 0
holds Product F > 0
proof
let F be FinSequence of REAL;
assume for i be Element of dom F holds F.i > 0; then
for j be Element of NAT st j in dom F holds F.j > 0;
hence Product F > 0 by NAT_4:42;
end;
theorem Th42:
for X be RealNormSpace-Sequence, Y be RealNormSpace st Y is complete
for seq be sequence of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
st seq is Cauchy_sequence_by_Norm
holds seq is convergent
proof
let X be RealNormSpace-Sequence,Y be RealNormSpace such that
A1: Y is complete;
let vseq be sequence of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
such that
A2: vseq is Cauchy_sequence_by_Norm;
defpred P[set, set] means ex xseq be sequence of Y st
(for n be Nat holds xseq.n = modetrans((vseq.n),X,Y).$1) &
xseq is convergent & $2 = lim xseq;
A3: for x be Element of product X ex y be Element of Y st P[x,y]
proof
let x be Element of product X;
deffunc F(Nat) = modetrans((vseq.$1),X,Y).x;
consider xseq be sequence of Y such that
A4: for n be Element of NAT holds xseq.n = F(n) from FUNCT_2:sch 4;
A5: for n be Nat holds xseq.n = F(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A4;
end;
take lim xseq;
A6: for m,k be Nat holds
||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| * NrProduct x
proof
let m,k be Nat;
reconsider h1 = vseq.m-vseq.k
as Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
k in NAT by ORDINAL1:def 12; then
A7: xseq.k = modetrans((vseq.k),X,Y).x by A4;
a8: vseq.m is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
a9: vseq.k is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
m in NAT by ORDINAL1:def 12; then
xseq.m = modetrans((vseq.m),X,Y).x by A4;
then xseq.m - xseq.k = h1.x by A7,a8,a9,LOPBAN10:52;
hence thesis by LOPBAN10:45;
end;
now
let e be Real such that
A10: e > 0;
now
per cases;
case
A11: ex i be Element of dom X st x.i = 0.(X.i);
reconsider k = 0 as Nat;
take k;
thus for n, m be Nat st n >= k & m >= k
holds ||.xseq.n - xseq.m.|| < e
proof
let n, m be Nat such that
n >= k and m >= k;
m in NAT by ORDINAL1:def 12; then
A12: xseq.m = modetrans((vseq.m),X,Y).x by A4
.= 0.Y by A11,LOPBAN10:36;
n in NAT by ORDINAL1:def 12; then
xseq.n = modetrans((vseq.n),X,Y).x by A4
.= 0.Y by A11,LOPBAN10:36;
hence thesis by A10,A12;
end;
end;
case
not ex i be Element of dom X st x.i = 0.(X.i); then
A13: NrProduct x > 0 by LOPBAN10:27; then
consider k be Nat such that
A15: for n, m be Nat st n >= k & m >= k
holds ||.(vseq.n) - (vseq.m).|| < e / (NrProduct x)
by A2,A10,RSSPACE3:8;
take k;
thus for n, m be Nat st n >= k & m >= k
holds ||.xseq.n - xseq.m.|| < e
proof
let n,m be Nat such that
A16: n >=k and
A17: m >= k;
||.(vseq.n) - (vseq.m).|| < e / (NrProduct x)
by A15,A16,A17; then
A18: ||.(vseq.n) - (vseq.m).|| * (NrProduct x)
< e / (NrProduct x) * (NrProduct x) by A13,XREAL_1:68;
A19: e / (NrProduct x) * (NrProduct x)
= e * ((NrProduct x)"* (NrProduct x))
.= e * 1 by A13,XCMPLX_0:def 7
.= e;
||.xseq.n - xseq.m.||
<= ||.(vseq.n) - (vseq.m).|| * ( NrProduct x ) by A6;
hence thesis by A18,A19,XXREAL_0:2;
end;
end;
end;
hence ex k be Nat st for n, m be Nat
st n >= k & m >= k holds ||.xseq.n -xseq.m.|| < e;
end; then
xseq is Cauchy_sequence_by_Norm by RSSPACE3:8;
hence thesis by A1,A5;
end;
consider f be Function of the carrier of product X,
the carrier of Y such that
A20: for x be Element of product X holds P[x,f.x] from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of product X,Y;
A21: for u be Point of product X,
i be Element of dom X,
x be Point of X.i holds
ex xseqi be sequence of Y
st (for n be Nat holds
xseqi.n = ( modetrans((vseq.n),X,Y) * reproj(i,u)).x)
& xseqi is convergent
& (tseq*reproj (i,u)).x = lim xseqi
proof
let u be Point of product X,
i be Element of dom X,
x be Point of X.i;
reconsider v = reproj (i,u).x as Point of product X;
consider xseq be sequence of Y such that
A22: (for n be Nat holds xseq.n = modetrans((vseq.n),X,Y).v) &
xseq is convergent & tseq.v = lim xseq by A20;
A23: dom reproj (i,u) = the carrier of (X.i) by FUNCT_2:def 1;
take xseq;
thus for n be Nat holds xseq.n
= (modetrans((vseq.n),X,Y) * reproj(i,u)).x
proof
let n be Nat;
thus xseq.n = modetrans((vseq.n),X,Y).v by A22
.= (vseq.n).(reproj(i,u).x) by LOPBAN10:def 13
.= ((vseq.n) * reproj(i,u)).x by A23,FUNCT_1:13
.= (modetrans((vseq.n),X,Y) * reproj(i,u)).x by LOPBAN10:def 13;
end;
thus xseq is convergent by A22;
thus (tseq * reproj(i,u)).x = lim xseq by A22,A23,FUNCT_1:13;
end;
now
let i be Element of dom X,u be Point of product X;
set tseqiu = tseq * reproj(i,u);
deffunc H(Nat) = modetrans((vseq.$1),X,Y) * reproj (i,u);
A24: now
let x,y be Point of X.i;
consider xseq be sequence of Y such that
A25: for n be Nat holds xseq.n = H(n).x and
A26: xseq is convergent and
A27: tseqiu.x = lim xseq by A21;
consider zseq be sequence of Y such that
A28: for n be Nat holds zseq.n = H(n).(x+y) and
zseq is convergent and
A29: tseqiu.(x+y) = lim zseq by A21;
consider yseq be sequence of Y such that
A30: for n be Nat holds yseq.n = H(n).y and
A31: yseq is convergent and
A32: tseqiu.y = lim yseq by A21;
now
let n be Nat;
A33: H(n) is LinearOperator of X.i,Y by LOPBAN10:def 6;
thus zseq.n = H(n).(x+y) by A28
.= H(n).x+H(n).y by A33,VECTSP_1:def 20
.= xseq.n + H(n).y by A25
.= xseq.n +yseq.n by A30;
end; then
zseq = xseq + yseq by NORMSP_1:def 2;
hence tseqiu.(x+y) = tseqiu.x+tseqiu.y
by A26,A27,A29,A31,A32,NORMSP_1:25;
end;
now
let x be Point of X.i;
let a be Real;
consider xseq be sequence of Y such that
A34: for n be Nat holds xseq.n = H(n).x and
A35: xseq is convergent and
A36: tseqiu.x = lim xseq by A21;
consider zseq be sequence of Y such that
A37: for n be Nat holds zseq.n = H(n).(a*x) and
zseq is convergent and
A38: tseqiu.(a*x) = lim zseq by A21;
now
let n be Nat;
A39: H(n) is LinearOperator of X.i,Y by LOPBAN10:def 6;
thus zseq.n = H(n).(a*x) by A37
.= a * H(n).x by A39,LOPBAN_1:def 5
.= a * xseq.n by A34;
end; then
zseq = a * xseq by NORMSP_1:def 5;
hence tseqiu.(a*x) = a * tseqiu.x by A35,A36,A38,NORMSP_1:28;
end;
hence tseq * reproj(i,u) is LinearOperator of X.i,Y
by A24,LOPBAN_1:def 5,VECTSP_1:def 20;
end; then
reconsider tseq as MultilinearOperator of X,Y by LOPBAN10:def 6;
B39: now
let e1 be Real such that
A40: e1 > 0;
reconsider e = e1 as Real;
consider k be Nat such that
A41: for n, m be Nat st n >= k & m >= k
holds ||.(vseq.n) - (vseq.m).|| < e by A2,A40,RSSPACE3:8;
reconsider k as Nat;
take k;
now
let m be Nat;
assume m >= k; then
A42: ||.(vseq.m) - (vseq.k).|| < e by A41;
A43: ||.vseq.m.|| = ||.vseq.||.m by NORMSP_0:def 4;
A44: ||.vseq.k.|| = ||.vseq.||.k by NORMSP_0:def 4;
|. ||.vseq.m.|| - ||.vseq.k.|| .| <= ||.(vseq.m) - (vseq.k).||
by NORMSP_1:9;
hence |. ||.vseq.||.m - ||.vseq.||.k .| < e1
by A42,A43,A44,XXREAL_0:2;
end;
hence for m be Nat st m >= k holds |.||.vseq.||.m - ||.vseq.||.k .| < e1;
end; then
A45: ||.vseq.|| is convergent by SEQ_4:41;
A46: tseq is Lipschitzian
proof
take lim (||.vseq.||);
A47: now
let x be Point of product X;
consider xseq be sequence of Y such that
A48: for n be Nat holds xseq.n = modetrans((vseq.n),X,Y).x and
A49: xseq is convergent and
A50: tseq.x = lim xseq by A20;
A51: ||.tseq.x.|| = lim ||.xseq.|| by A49,A50,LOPBAN_1:20;
A52: for m be Nat holds ||.xseq.m.|| <= ||.vseq.m.|| * ( NrProduct x )
proof
let m be Nat;
A53: xseq.m = modetrans((vseq.m),X,Y).x by A48;
vseq.m is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
hence thesis by A53,LOPBAN10:45;
end;
A54: for n be Nat holds ||.xseq.||.n <= ((NrProduct x)(#)||.vseq.||).n
proof
let n be Nat;
A55: ||.xseq.||.n = ||.(xseq.n).|| by NORMSP_0:def 4;
A56: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4;
||.(xseq.n).|| <= ||.vseq.n.|| * (NrProduct x) by A52;
hence thesis by A55,A56,SEQ_1:9;
end;
A58: lim ( (NrProduct x)(#)||.vseq.|| )
= lim (||.vseq.||) * (NrProduct x) by B39,SEQ_2:8,SEQ_4:41;
||.xseq.|| is convergent by A49,A50,LOPBAN_1:20;
hence ||.tseq.x.|| <= lim (||.vseq.||) * (NrProduct x)
by A45,A51,A54,A58,SEQ_2:18;
end;
now
let n be Nat;
||.vseq.n.|| >=0;
hence ||.vseq.||.n >=0 by NORMSP_0:def 4;
end;
hence thesis by B39,A47,SEQ_2:17,SEQ_4:41;
end;
A59: for e be Real st e > 0
ex k be Nat st for n be Nat st n >= k holds
for x be Point of product X holds
||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e * (NrProduct x)
proof
let e be Real;
assume e > 0; then
consider k be Nat such that
A60: for n, m be Nat st n >= k & m >= k
holds ||.(vseq.n) - (vseq.m).|| < e by A2,RSSPACE3:8;
take k;
now
let n be Nat such that
A61: n >= k;
now
let x be Point of product X;
consider xseq be sequence of Y such that
A62: for n be Nat holds xseq.n = modetrans((vseq.n),X,Y). x and
A63: xseq is convergent and
A64: tseq.x = lim xseq by A20;
A65: for m,k be Nat holds
||.xseq.m - xseq.k.|| <= ||.vseq.m - vseq.k.|| * (NrProduct x)
proof
let m,k be Nat;
reconsider h1 = vseq.m - vseq.k
as Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
A66: xseq.k = modetrans((vseq.k),X,Y).x by A62;
a67: vseq.m is Lipschitzian MultilinearOperator of X,Y
by LOPBAN10:def 11;
a68: vseq.k is Lipschitzian MultilinearOperator of X,Y
by LOPBAN10:def 11;
xseq.m = modetrans((vseq.m),X,Y).x by A62; then
xseq.m - xseq.k =h1.x by A66,a67,a68,LOPBAN10:52;
hence thesis by LOPBAN10:45;
end;
A69: for m be Nat st m >= k holds
||.xseq.n-xseq.m.|| <= e * (NrProduct x)
proof
let m be Nat;
assume m >= k; then
A70: ||.vseq.n - vseq.m.|| < e by A60,A61;
A71: ||.xseq.n-xseq.m.||
<= ||.vseq.n - vseq.m.|| * ( NrProduct x ) by A65;
||.vseq.n - vseq.m.|| * (NrProduct x)
<= e * (NrProduct x) by A70,XREAL_1:64;
hence thesis by A71,XXREAL_0:2;
end;
||.xseq.n - tseq.x.|| <= e * (NrProduct x)
proof
deffunc F(Nat) = ||.xseq.$1 - xseq.n.||;
consider rseq be Real_Sequence such that
A72: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
now
let x be object;
assume x in NAT; then
reconsider k = x as Nat;
thus rseq.x = ||.xseq.k - xseq.n.|| by A72
.= ||.(xseq - xseq.n).k.|| by NORMSP_1:def 4
.= ||.(xseq - xseq.n).||.x by NORMSP_0:def 4;
end; then
A73: rseq = ||.xseq - xseq.n.|| by FUNCT_2:12;
A74: xseq - xseq.n is convergent by A63,NORMSP_1:21;
lim (xseq-xseq.n)= tseq.x - xseq.n by A63,A64,NORMSP_1:27; then
A75: lim rseq = ||.tseq.x-xseq.n.|| by A73,A74,LOPBAN_1:41;
for m be Nat st m >= k holds rseq.m <= e * (NrProduct x)
proof
let m be Nat such that
A76: m >=k;
rseq.m = ||.xseq.m-xseq.n.|| by A72
.= ||.xseq.n-xseq.m.|| by NORMSP_1:7;
hence thesis by A69,A76;
end; then
lim rseq <= e * (NrProduct x)
by A73,A74,LOPBAN_1:41,RSSPACE2:5;
hence thesis by A75,NORMSP_1:7;
end;
hence ||.modetrans((vseq.n),X,Y).x - tseq.x.||
<= e * (NrProduct x) by A62;
end;
hence for x be Point of product X holds
||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e * (NrProduct x);
end;
hence thesis;
end;
reconsider tseq as Lipschitzian MultilinearOperator of X,Y by A46;
reconsider tv = tseq as Point of
R_NormSpace_of_BoundedMultilinearOperators(X,Y) by LOPBAN10:def 11;
A77: for e be Real st e > 0
ex k be Nat st for n be Nat st n >= k holds ||.vseq.n - tv.|| <= e
proof
let e be Real such that
A78: e > 0;
consider k be Nat such that
A79: for n be Nat st n >= k holds for x be Point of product X
holds ||.modetrans((vseq.n),X,Y).x - tseq.x.||
<= e * (NrProduct x) by A59,A78;
now
set g1 = tseq;
let n be Nat such that
A80: n >= k;
reconsider h1 = vseq.n - tv as Lipschitzian
MultilinearOperator of X,Y by LOPBAN10:def 11;
set f1 = modetrans((vseq.n),X,Y);
A81: now
let t be Point of product X;
assume for i be Element of dom X holds
||.t.i.|| <= 1; then
0 <= NrProduct t & NrProduct t <= 1 by LOPBAN10:35; then
A82: e * (NrProduct t) <= e * 1 by A78,XREAL_1:64;
A83: ||.f1.t-g1.t.|| <= e * (NrProduct t) by A79,A80;
vseq.n is Lipschitzian MultilinearOperator of X,Y
by LOPBAN10:def 11; then
||.h1.t.|| = ||.f1.t-g1.t.|| by LOPBAN10:52;
hence ||.h1.t.|| <= e by A82,A83,XXREAL_0:2;
end;
A84: now
let r be Real;
assume r in PreNorms(h1); then
ex t be Point of product X
st r = ||.h1.t.||
& for i be Element of dom X holds ||.t.i.|| <= 1;
hence r <= e by A81;
end;
(for s be Real st s in PreNorms(h1) holds s <= e) implies
upper_bound PreNorms(h1) <= e by SEQ_4:45;
hence ||.vseq.n-tv.|| <= e by A84,LOPBAN10:43;
end;
hence thesis;
end;
for e be Real st e > 0
ex m be Nat st for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A86: e > 0;
consider m be Nat such that
A87: for n be Nat st n >= m holds
||.(vseq.n) - tv.|| <= e/2 by A77,A86;
A88: e/2 < e by A86,XREAL_1:216;
now
let n be Nat;
assume n >= m; then
||.(vseq.n) - tv.|| <= e/2 by A87;
hence ||.(vseq.n) - tv.|| < e by A88,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by NORMSP_1:def 6;
end;
theorem Th43:
for X be RealNormSpace-Sequence for Y be RealBanachSpace holds
R_NormSpace_of_BoundedMultilinearOperators(X,Y) is RealBanachSpace
proof
let X be RealNormSpace-Sequence;
let Y be RealBanachSpace;
for seq be sequence of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
st seq is Cauchy_sequence_by_Norm
holds seq is convergent by Th42;
hence thesis by LOPBAN_1:def 15;
end;
registration
let X be RealNormSpace-Sequence;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedMultilinearOperators (X,Y) -> complete;
coherence by Th43;
end;
begin :: Equivalence of Continuity Definition of Multilinear Operator
theorem NDIFF823:
for n be Nat, F be Element of REAL n, s be Real
st for i be Nat st i in dom F holds 0 <= F.i & F.i <= s
holds |.F.| <= sqrt((s*s) * len F)
proof
let n be Nat,
F be Element of REAL n,
s be Real;
assume
A1: for i be Nat st i in dom F holds 0 <= F.i & F.i <= s;
A2: 0 <= Sum sqr F by RVSUM_1:86;
set G = len F |-> s;
A3: sqr G = len F |-> s^2 by RVSUM_1:56;
len F is natural Number & s is Element of REAL by XREAL_0:def 1; then
reconsider G as Element of len F -tuples_on REAL by FINSEQ_2:112;
reconsider F0 = F as Element of len F -tuples_on REAL by FINSEQ_2:92;
for j being Nat st j in Seg len F0 holds
(sqr F0).j <= (sqr G).j
proof
let j be Nat;
assume
A4: j in Seg len F0; then
A5: j in dom F by FINSEQ_1:def 3;
A6: (sqr F0).j = (F.j)^2 by VALUED_1:11;
A7: (sqr G).j = (G.j)^2 by VALUED_1:11;
A8: 0 <= F0.j by A1,A5;
F0.j <= s by A1,A5; then
F0.j <= G.j by A4,FINSEQ_2:57;
hence thesis by A6,A7,A8,SQUARE_1:15;
end; then
Sum(sqr F0) <= Sum(sqr G) by RVSUM_1:82; then
Sum sqr F <= (s*s) * len F by A3,RVSUM_1:80;
hence thesis by A2,SQUARE_1:26;
end;
theorem LM02:
for X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be MultilinearOperator of X,Y,
K being Real
st
( 0 <= K & for x be Point of product X
holds ||. f.x .|| <= K * NrProduct x )
holds
for v0,v1 being Point of product X,
Cv0,Cv1 be FinSequence,
i be Element of dom X
st Cv0 = v0 & Cv1 = v1
& ||.v1-v0.|| <= 1
& for j be Element of dom X st i <> j holds Cv1.j = Cv0.j
holds ||. f/.v1 - f/.v0 .||
<= (||.v0.|| + 1) |^ len X * K * ||.(v1-v0).i.||
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be MultilinearOperator of X,Y,
K be Real;
assume
A1: 0 <= K
& for x be Point of product X
holds ||. f.x .|| <= K * NrProduct x;
let v0,v1 be Point of product X,
Cv0,Cv1 be FinSequence,
i be Element of dom X;
assume
A2: Cv0 = v0 & Cv1 = v1
& ||.v1-v0.|| <= 1
& for j be Element of dom X
st i <> j holds Cv1.j = Cv0.j;
f is Function of product X,Y & f is Multilinear; then
A3: f * reproj(i,v0) is LinearOperator of X.i,Y;
A4: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6; then
A5: ex g be Function st Cv1 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A2,CARD_3:def 5;
A6: ex g be Function
st reproj(i,v0).(v1.i) = g
& dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A4,CARD_3:def 5;
for x be object st x in dom v1
holds v1.x = (reproj(i,v0).(v1.i)).x
proof
let x be object;
assume x in dom v1; then
reconsider j = x as Element of dom X by A2,A5,DCARXX;
per cases;
suppose
j = i;
hence v1.x = (reproj(i,v0).(v1.i)).x by LOPBAN10:15;
end;
suppose
A8: j <> i; then
(reproj(i,v0).(v1.i)).j = v0.j by LOPBAN10:16
.= v1.j by A2,A8;
hence v1.x = (reproj(i,v0).(v1.i)).x;
end;
end; then
A10: v1 = reproj(i,v0).(v1.i) by A2,A5,A6,FUNCT_1:2;
reconsider v3 = reproj(i,v0). (v1.i - v0.i) as Point of product X;
f/.v1 - f/.v0
= f.(reproj(i,v0). (v1.i)) - f.(reproj(i,v0).(v0.i)) by A10,LOPBAN10:17
.= (f*reproj(i,v0)). (v1.i) - f.( reproj(i,v0).(v0.i) ) by FUNCT_2:15
.= (f*reproj(i,v0)). (v1.i) - (f*reproj(i,v0)).(v0.i) by FUNCT_2:15
.= (f*reproj(i,v0)). (v1.i) + (-1)* (f*reproj(i,v0)).(v0.i) by RLVECT_1:16
.= (f*reproj(i,v0)). (v1.i) + (f*reproj(i,v0)).((-1)*(v0.i))
by A3,LOPBAN_1:def 5
.= (f*reproj(i,v0)).((v1.i) + (-1)*(v0.i)) by A3,VECTSP_1:def 20
.= (f*reproj(i,v0)).( (v1.i) - (v0.i)) by RLVECT_1:16
.= f.v3 by FUNCT_2:15; then
A12: ||.f/.v1 - f/.v0.|| <= K * NrProduct v3 by A1;
1 is Element of REAL by XREAL_0:def 1; then
reconsider R1 = len X |-> (1 qua Real)
as FinSequence of REAL by FINSEQ_2:63;
A13: dom R1 = Seg len X by FUNCT_2:def 1;
i in dom X; then
A14: i in dom R1 by A13,FINSEQ_1:def 3;
reconsider Nv1v0 = ||.(v1-v0).i.|| as Element of REAL;
reconsider R2 = R1 +* (i,Nv1v0) as FinSequence of REAL;
||.v0.||+1 is Element of REAL by XREAL_0:def 1; then
reconsider R3 = len X |-> ( ||.v0.||+1)
as FinSequence of REAL by FINSEQ_2:63;
set R4 = mlt (R2,R3);
dom R2 = dom R1 by FUNCT_7:30; then
dom R2 = Seg len X & dom R3 = Seg len X by FUNCT_2:def 1; then
A15: len R2 = len X & len R3 = len X by FINSEQ_1:def 3; then
R2 is Element of len X -tuples_on REAL
& R3 is Element of len X -tuples_on REAL by FINSEQ_2:92; then
A16: Product R4 = (Product R2)*(Product R3) by RVSUM_1:107;
A17: (Product R2) = ||.(v1-v0).i.|| by A14,LM03;
A18: (Product R3) = (||.v0.||+1) to_power len X by NAT_4:55
.= (||.v0.||+1) |^ len X;
consider Nx be FinSequence of REAL such that
A19: dom Nx = dom X
& ( for i be Element of dom X holds Nx.i = ||.v3.i.|| )
& NrProduct v3 = Product Nx by LOPBAN10:def 9;
dom Nx = Seg len X by A19,FINSEQ_1:def 3; then
A20: len Nx = len X by FINSEQ_1:def 3;
dom R4 = dom R2 /\ dom R3 by VALUED_1:def 4
.= Seg len R2 /\ dom R3 by FINSEQ_1:def 3
.= Seg len R2 /\ Seg len R3 by FINSEQ_1:def 3
.= Seg len X by A15; then
A21: len R4 = len X by FINSEQ_1:def 3;
for k being Element of NAT st k in dom Nx holds
Nx.k <= R4.k & 0 <= Nx.k
proof
let k be Element of NAT;
assume k in dom Nx; then
A22: k in Seg len Nx by FINSEQ_1:def 3; then
reconsider j = k as Element of dom X by A20,FINSEQ_1:def 3;
A24: Nx.k = ||. v3.j.|| by A19;
A26: R4.k = R2.k * R3.j by RVSUM_1:60
.= R2.k * (||.v0.||+1) by A20,A22,FUNCOP_1:7;
now
per cases;
suppose
A27: j = i;
v3.j = v1.i - v0.i by A27,LOPBAN10:15
.= (v1-v0).i by LOPBAN10:26; then
A29: Nx.k = ||.(v1-v0).i.|| by A19,A27;
1+0 <= ||.v0.|| + 1 by XREAL_1:7; then
||.(v1-v0).i.|| * 1
<= ||.(v1-v0).i.|| * (||.v0.||+1) by XREAL_1:66;
hence Nx.k <= R4.k by A13,A20,A22,A26,A27,A29,FUNCT_7:31;
end;
suppose
A30: j <> i; then
A31: R2.k = R1.j by FUNCT_7:32
.= 1 by A20,A22,FUNCOP_1:7;
||.v0.j.|| <= ||.v0.|| by A4,PRVECT_2:10; then
||.v0.j.|| + 0 <= ||.v0.|| + 1 by XREAL_1:7;
hence Nx.k <= R4.k by A24,A26,A30,A31,LOPBAN10:16;
end;
end;
hence thesis by A24;
end; then
NrProduct v3 <= ( ||.(v1-v0).i.|| * ( ||.v0.||+1) |^ len X )
by A16,A17,A18,A19,A20,A21,FINSEQ_9:34; then
K * NrProduct v3 <= K * ((||.v0.||+1) |^ len X * ||.(v1-v0).i.||)
by A1,XREAL_1:66;
hence thesis by A12,XXREAL_0:2;
end;
theorem LM01:
for X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be MultilinearOperator of X,Y,
K being Real
st (0 <= K &
for x being Point of product X
holds ||. f.x .|| <= K * NrProduct x) holds
for v0 being Point of product X
ex M be Real
st 0 <= M
& for v1 be Point of product X
st ||.v1-v0.|| <= 1
holds
ex F be FinSequence of REAL
st dom F = dom X
& ||.f/.v1 - f/.v0.|| <= M * K * Sum F
& for i be Element of dom X
holds F.i = ||.(v1-v0).i.||
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be MultilinearOperator of X,Y,
K be Real;
assume that
A1: 0 <= K and
A2: for x being Point of product X
holds ||. f.x .|| <= K * NrProduct x;
A3: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
let v0 be Point of product X;
consider g be Function such that
A4: v0 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5;
dom g = Seg len (carr X) by A4,FINSEQ_1:def 3; then
reconsider Cv0 = v0 as FinSequence by A4,FINSEQ_1:def 2;
set L = ||.v0.|| + 3;
set M = L |^ len X;
take M;
thus 0 <= M by POWER:3;
defpred P[Nat] means
for v0, v1 be Point of product X,
Cv0,Cv1 be FinSequence
st ||.v1-v0.|| <= 1
& v0 = Cv0 & v1 = Cv1 & $1 <=len X
& Cv1 | (len X -'$1 ) = Cv0 | (len X -'$1 ) holds
ex F be FinSequence of REAL
st dom F = Seg $1
& ||.f/.v1 - f/.v0.|| <= (||.v0.|| + 3) |^ len X * K * Sum F
& for n be Nat st n in Seg $1 holds
ex i be Element of dom X
st i = len X -'$1 + n & F.n = ||.(v1-v0).i.||;
A6: P[0]
proof
let v0,v1 be Point of product X,
Cv0,Cv1 be FinSequence;
assume
A7: ||.v1-v0.|| <= 1
& v0 = Cv0 & v1 = Cv1 & 0 <=len X
& Cv1 | (len X -'0 ) = Cv0 | (len X -'0 );
A8: len X -'0 = (len X + 0) -'0
.= len X by NAT_D:34;
reconsider F = <*>REAL as FinSequence of REAL;
take F;
thus dom F = Seg 0;
consider g be Function such that
A9: v0 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5;
A10: dom g = Seg len (carr X) by A9,FINSEQ_1:def 3; then
reconsider Cv0 = v0 as FinSequence by A9,FINSEQ_1:def 2;
A11: len Cv0 = len carr X by A9,A10,FINSEQ_1:def 3
.= len X by PRVECT_1:def 11;
consider g be Function such that
A12: v1 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5;
dom Cv1 = Seg len carr X by A7,A12,FINSEQ_1:def 3; then
A14: len Cv1 = len carr X by FINSEQ_1:def 3
.= len X by PRVECT_1:def 11;
Cv1 = Cv0 | len X by A7,A8,A14,FINSEQ_1:58
.= Cv0 by A11,FINSEQ_1:58; then
f/.v1 - f/.v0 = 0.Y by A7,RLVECT_1:15;
hence ||.f/.v1 - f/.v0.|| <= (||.v0.||+3) |^len X * K * Sum F
by RVSUM_1:72;
thus for n be Nat st n in Seg 0 holds
ex i be Element of dom X
st i = len X -'0 + n & F.n = ||.(v1-v0).i.||;
end;
A16: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A17: P[k];
let v0,v1 be Point of product X,
Cv0,Cv1 be FinSequence;
assume
A18: ||.v1-v0.|| <= 1
& v0 = Cv0 & v1 = Cv1 & k+1 <=len X
& Cv1 | (len X -'(k+1) ) = Cv0 | (len X -'(k+1) );
consider g be Function such that
A19: v0 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5;
dom g = Seg len (carr X) by A19,FINSEQ_1:def 3; then
reconsider Cv0 = v0 as FinSequence by A19,FINSEQ_1:def 2;
dom Cv0 = Seg len carr X by A19,FINSEQ_1:def 3; then
A21: len Cv0 = len carr X by FINSEQ_1:def 3
.= len X by PRVECT_1:def 11; then
A22: dom Cv0 = Seg len X by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
consider g1 be Function such that
A23: v1 = g1 & dom g1 = dom carr X
& for i be object st i in dom carr X
holds g1.i in (carr X).i by A3,CARD_3:def 5;
dom g1 = Seg len (carr X) by A23,FINSEQ_1:def 3; then
reconsider Cv1 = v1 as FinSequence by A23,FINSEQ_1:def 2;
1 <= 1+k by NAT_1:11; then
1 <= len X by A18,XXREAL_0:2; then
len X in Seg len X; then
reconsider i = len X as Element of dom X by FINSEQ_1:def 3;
per cases;
suppose
A25: k = 0; then
A26: len X -'(k+1) = len X - 1 by A18,XREAL_0:def 2;
for j be Element of dom X st i <> j holds Cv1.j = Cv0.j
proof
let j be Element of dom X;
j in dom X; then
j in Seg len X by FINSEQ_1:def 3; then
A27: 1 <= j & j <= len X by FINSEQ_1:1;
assume i <> j; then
j < len X by A27,XXREAL_0:1; then
j+1 <= len X by NAT_1:13; then
j +1 -1 <= len X - 1 by XREAL_1:9; then
A28: j in Seg ( len X -'(k+1)) by A26,A27;
thus Cv1.j = (Cv0 | (len X -'(k+1))).j by A18,A28,FUNCT_1:49
.= Cv0.j by A28,FUNCT_1:49;
end; then
A29: ||.f/.v1 - f/.v0.|| <= (||.v0.||+1) |^ len X
* K * ||.(v1-v0).i.|| by A1,A2,A18,LM02;
set F = <* ||. (v1-v0).i .|| *>;
rng F c= REAL; then
reconsider F as FinSequence of REAL by FINSEQ_1:def 4;
take F;
thus dom F = Seg len F by FINSEQ_1:def 3
.= Seg (k+1) by A25,FINSEQ_1:40;
A31: ||.f/.v1 - f/.v0.|| <= (||.v0.||+1) |^ len X
* K * Sum F by A29,RVSUM_1:73;
||.v0.|| + 1 + 0 <= ||.v0.|| + 1 + 2 by XREAL_1:7; then
A32: ( ||.v0.||+1) |^ len X <= ( ||.v0.||+3) |^ len X
by PREPOWER:9;
0 <= Sum F by RVSUM_1:73; then
( ||.v0.||+1) |^ len X * (K * Sum F)
<= ( ||.v0.||+3) |^ len X * (K * Sum F) by A1,A32,XREAL_1:64;
hence ||.f/.v1 -f/.v0 .|| <= (||.v0.||+3) |^len X * K * Sum F
by A31,XXREAL_0:2;
thus for n be Nat st n in Seg (k+1) holds
ex j be Element of dom X st j = len X -'(k+1) + n
& F.n = ||.(v1-v0).j.||
proof
let n be Nat;
assume
A33: n in Seg (k+1); then
A34: len X -'(k+1) + n
= len X -1 + 1 by A25,A26,FINSEQ_1:2,TARSKI:def 1
.= i;
take i;
n = 1 by A25,A33,FINSEQ_1:2,TARSKI:def 1;
hence thesis by A34;
end;
end;
suppose k <> 0;
A35: k+1 - k <= len X - k by A18,XREAL_1:13;
A36: len X - k <= len X - 0 by XREAL_1:13;
len X-k in NAT by A35,INT_1:3; then
len X-k in Seg len X by A35,A36; then
reconsider k1 =len X -k as Element of dom X by FINSEQ_1:def 3;
Cv0.k1 = v0.k1; then
reconsider Cv0k1 = Cv0.k1 as Point of X.k1;
k <= k+1 by NAT_1:11; then
A38: k <= len X by A18,XXREAL_0:2;
reconsider v2= (reproj (k1,v1)). Cv0k1 as Point of product X;
consider g be Function such that
A39: v2 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5;
A40: dom g =Seg len (carr X) by A39,FINSEQ_1:def 3; then
reconsider Cv2 = v2 as FinSequence by A39,FINSEQ_1:def 2;
A41: len Cv2 = len carr X by A39,A40,FINSEQ_1:def 3
.= len X by PRVECT_1:def 11;
reconsider w12 = v1-v2 as Element of product carr X by A3;
reconsider w02 = v2-v0 as Element of product carr X by A3;
reconsider w10 = v1-v0 as Element of product carr X by A3;
||.v2-v0.|| <= ||.v1-v0.||
proof
A42: ||.v2-v0.|| = |. normsequence (X,w02) .| by A3,PRVECT_2:def 12;
A43: ||.v1-v0.|| = |. normsequence (X,w10) .| by A3,PRVECT_2:def 12;
A44: 0 <= Sum(sqr normsequence (X,w02)) by RVSUM_1:86;
for j being Nat st j in Seg len X holds
(sqr normsequence (X,w02)).j <= (sqr normsequence (X,w10)).j
proof
let j be Nat;
assume
A45: j in Seg len X;
reconsider i = j as Element of dom X by A45,FINSEQ_1: def 3;
A46: (sqr normsequence(X,w02)).j
= (normsequence(X,w02).j) ^2 by VALUED_1:11
.= (||.(v2-v0).i.||) ^2 by PRVECT_2:def 11;
A47: (sqr normsequence (X,w10)).j
= (normsequence (X,w10).j) ^2 by VALUED_1:11
.= (||.(v1-v0).i.||) ^2 by PRVECT_2:def 11;
A48: (v2-v0).i = v2.i - v0.i by LOPBAN10:26;
A49: (v1-v0).i = v1.i - v0.i by LOPBAN10:26;
||.(v2-v0).i.|| <=||.(v1-v0).i.||
proof
per cases;
suppose
A50: i = k1;
v2.i = v0.i by A50,LOPBAN10:15; then
v2.i - v0.i = 0.(X.i) by RLVECT_1:15;
hence ||.(v2-v0).i.|| <= ||.(v1-v0).i.|| by A48;
end;
suppose
i <> k1;
hence ||.(v2-v0).i.|| <= ||.(v1-v0).i.||
by A48,A49,LOPBAN10:16;
end;
end;
hence thesis by A46,A47,SQUARE_1:15;
end;
hence thesis by A42,A43,A44,SQUARE_1:26,RVSUM_1:82;
end; then
A51: ||.v2-v0.|| <= 1 by A18,XXREAL_0:2;
A52: len X -'k = k1 by XREAL_0:def 2;
len ( Cv0 | (len X -'k) ) = k1 by A21,A36,A52,FINSEQ_1:59; then
A53: dom ( Cv0 | (len X -'k) ) = Seg k1 by FINSEQ_1:def 3;
len ( Cv2 | (len X -'k) ) = k1 by A36,A41,A52,FINSEQ_1:59; then
A54: dom ( Cv2 | (len X -'k) ) = Seg k1 by FINSEQ_1:def 3;
A55: len X -'(k+1) = len X -(k+1) by A18,XREAL_0:def 2,XREAL_1:48;
for j be Nat st j in dom (Cv0 | (len X -'k)) holds
( Cv0 | (len X -'k )).j = (Cv2 | (len X -'k)).j
proof
let j be Nat;
assume
A56: j in dom(Cv0 | (len X -'k)); then
A57: (Cv0 | (len X -'k)).j = Cv0.j by FUNCT_1:47;
A59: 1 <= j & j <= k1 by A53,A56,FINSEQ_1:1;
per cases;
suppose
j = k1; then
Cv0.j = Cv2.j by LOPBAN10:15;
hence (Cv0 | (len X -'k)).j = (Cv2 | (len X -'k)).j
by A53,A54,A56,A57,FUNCT_1:47;
end;
suppose
A61: j <> k1; then
j < k1 by A59,XXREAL_0:1; then
j+1 <= k1 by NAT_1:13; then
j + 1 - 1 <= k1 - 1 by XREAL_1:13; then
A62: j in Seg (len X -'(k+1)) by A55,A59;
j in dom X by A22,A56,RELAT_1:60,TARSKI:def 3; then
v2.j = Cv1.j by A61,LOPBAN10:16
.= (Cv0 | (len X -'(k+1))).j by A18,A62,FUNCT_1:49
.= v0.j by A62,FUNCT_1:49;
hence (Cv0 | (len X -'k)).j = (Cv2 | (len X -'k)).j
by A53,A54,A56,A57,FUNCT_1:47;
end;
end; then
A63: Cv0 | (len X -'k) = Cv2 | (len X -'k) by A53,A54,FINSEQ_1:13;
consider F1 be FinSequence of REAL such that
A64: dom F1 = Seg k
& ||.f/.v2 - f/.v0.|| <= (||.v0.|| + 3) |^len X * K * Sum F1
& for n be Nat st n in Seg k
holds ex i be Element of dom X
st i = len X -'k + n & F1.n = ||.(v2-v0).i.|| by A17,A38,A51,A63;
||.v1-v2.|| <= ||.v1-v0.||
proof
A65: ||.v1-v2.|| = |. normsequence(X,w12) .| by A3,PRVECT_2:def 12;
A66: ||.v1-v0.|| = |. normsequence(X,w10) .| by A3,PRVECT_2:def 12;
A67: 0 <= Sum(sqr normsequence(X,w12)) by RVSUM_1:86;
for j being Nat st j in Seg len X holds
(sqr normsequence(X,w12)).j <= (sqr normsequence(X,w10)).j
proof
let j be Nat;
assume
A68: j in Seg len X;
reconsider i = j as Element of dom X by A68,FINSEQ_1: def 3;
A69: (sqr normsequence(X,w12)).j
= (normsequence (X,w12).j ) ^2 by VALUED_1:11
.= (||.(v1-v2).i.||) ^2 by PRVECT_2:def 11;
A70: ( sqr normsequence (X,w10)).j
= (normsequence(X,w10).j) ^2 by VALUED_1:11
.= (||.(v1-v0).i.||) ^2 by PRVECT_2:def 11;
A71: (v1-v2).i = v1.i - v2.i by LOPBAN10:26;
||.(v1-v2).i.|| <= ||.(v1-v0).i.||
proof
per cases;
suppose
i = k1; then
v2.i = v0.i by LOPBAN10:15;
hence ||.(v1-v2).i.|| <= ||.(v1-v0).i.|| by A71,LOPBAN10:26;
end;
suppose
i <> k1; then
v2.i = v1.i by LOPBAN10:16; then
v1.i - v2.i = 0.(X.i) by RLVECT_1:15;
hence ||.(v1-v2).i.|| <= ||.(v1-v0).i.|| by A71;
end;
end;
hence thesis by A69,A70,SQUARE_1:15;
end;
hence thesis by A65,A66,A67,RVSUM_1:82,SQUARE_1:26;
end; then
A74: ||.v1-v2.|| <= 1 by A18,XXREAL_0:2;
for j be Element of dom X st k1 <> j
holds Cv1.j = Cv2.j by LOPBAN10:16; then
A75: ||.f/.v1 -f/.v2 .||
<= ( ||.v2.||+1) |^ len X * K * ||.(v1-v2).k1.||
by A1,A2,A74,LM02;
v2 = v1+(v2-v1) by RLVECT_4:1; then
A76: ||.v2.|| <= ||.v1.|| + ||.v2-v1.|| by NORMSP_1:def 1;
||.v2-v1.|| <= 1 by A74,NORMSP_1:7; then
||.v1.|| + ||.v2-v1.|| <= ||.v1.|| + 1 by XREAL_1:7; then
A77: ||.v2.|| <= ||.v1.|| + 1 by A76,XXREAL_0:2;
v1 = (v1-v0) + v0 by RLVECT_4:1; then
||.v1.|| <= ||.v0.|| + ||.v1-v0.|| by NORMSP_1:def 1; then
A78: ||.v1.|| <= ||.v0.|| + ||.v0-v1.|| by NORMSP_1:7;
||.v0-v1.|| <= 1 by A18,NORMSP_1:7; then
||.v0.|| + ||.v0-v1.|| <= ||.v0.|| + 1 by XREAL_1:7; then
||.v1.|| <= ||.v0.|| + 1 by A78,XXREAL_0:2; then
||.v1.|| + 1 <= ||.v0.|| + 1 + 1 by XREAL_1:7; then
||.v2.|| <= ||.v0.|| + 2 by A77,XXREAL_0:2; then
A79: ||.v2.|| + 1 <= ||.v0.|| + 2 + 1 by XREAL_1:7;
A80: ( ||.v2.||+1) |^ len X <= ( ||.v0.||+3) |^ len X
by A79,PREPOWER:9;
A81: 0 < ( ||.v2.||+1) |^ len X by PREPOWER:6;
(v1-v2).k1 = v1.k1 - v2.k1 by LOPBAN10:26
.= v1.k1 - v0.k1 by LOPBAN10:15
.= (v1-v0).k1 by LOPBAN10:26; then
( ||.v2.||+1) |^ len X * (K* ||.(v1-v2).k1.||)
<= ( ||.v0.||+3) |^ len X * (K * ||.(v1-v0).k1.||)
by A1,A80,A81,XREAL_1:66; then
A84: ||.f/.v1 -f/.v2 .||
<= ( ||.v0.||+3) |^ len X * K * ||.(v1-v0).k1.||
by A75,XXREAL_0:2;
set F = <* ||. (v1-v0).k1 .|| *> ^ F1;
rng F c= REAL; then
reconsider F as FinSequence of REAL by FINSEQ_1:def 4;
k is Element of NAT by ORDINAL1:def 12; then
A85: len F1 = k by A64,FINSEQ_1:def 3;
len F = len F1 + len <* ||. (v1-v0).k1 .|| *> by FINSEQ_1:22
.= k + 1 by A85,FINSEQ_1:40; then
A86: dom F = Seg (k+1) by FINSEQ_1:def 3;
A87: for n be Nat st n in Seg (k+1) holds
ex i be Element of dom X
st i = len X -'(k+1) + n & F.n = ||.(v1-v0).i.||
proof
let n be Nat;
assume n in Seg(k+1); then
A88: 1 <= n & n <= k+1 by FINSEQ_1:1;
per cases;
suppose
A89: n = 1; then
A90:len X -'(k+1) + n
= len X -(k+1) + 1 by A18,XREAL_0:def 2,XREAL_1:48
.= k1;
take k1;
thus thesis by A89,A90,FINSEQ_1:41;
end;
suppose
n <> 1; then
1 < n by A88,XXREAL_0:1; then
A91: 1+1 <= n by NAT_1:13;
A93: len X -(k+1) + n <= len X -(k+1) + (k+1) by A88,XREAL_1:7;
A94: len X -(k+1) +2 <= len X -(k+1) + n by A91,XREAL_1:7;
1 + 0 <= 1 + (len X - k) by A35,XREAL_1:7; then
1 <= len X -'(k+1) + n by A55,A94,XXREAL_0:2; then
len X -'(k+1) + n in Seg len X by A55,A93; then
reconsider i = len X -'(k+1) + n as Element of dom X
by FINSEQ_1:def 3;
take i;
thus i = len X -'(k+1) + n;
A95: 2 -1 <= n -1 by A91,XREAL_1:9;
A96: n-1 <= k+1 -1 by A88,XREAL_1:9;
reconsider n1 = n-1 as Element of NAT by A88,INT_1:3;
A97: n1 in Seg k by A95,A96;
A98: len <* ||. (v1-v0).k1 .|| *> = 1 by FINSEQ_1:40;
A100: F.n = F.(1+n1)
.= F1.n1 by A85,A95,A96,A98,FINSEQ_1:65;
consider i1 be Element of dom X such that
A101: i1 = len X -'k + n1 & F1.n1 = ||.(v2-v0).i1.|| by A64,A97;
A102: i1 = len X -(k+1) + n by A52,A101
.= i by A18,XREAL_0:def 2,XREAL_1:48;
A105: k1 + 0 < k1 + 1 by XREAL_1:8;
A106: k1 + 1 <= k1+n1 by A95,XREAL_1:7;
(v2-v0).i = v2.i-v0.i by LOPBAN10:26
.= v1.i -v0.i by A52,A101,A102,A105,A106,LOPBAN10:16
.= (v1-v0).i by LOPBAN10:26;
hence F.n = ||.(v1-v0).i.|| by A100,A101,A102;
end;
end;
f/.v1 -f/.v0 = f/.v1 -f/.v2 + f/.v2 - f/.v0 by RLVECT_4:1
.= (f/.v1 -f/.v2) + (f/.v2 - f/.v0) by RLVECT_1:28; then
A107: ||. f/.v1 -f/.v0 .||
<= ||.f/.v1 -f/.v2.|| + ||.f/.v2 - f/.v0.|| by NORMSP_1:def 1;
A108: ||.f/.v1 -f/.v2.|| + ||.f/.v2 - f/.v0.||
<= ((||.v0.||+3) |^ len X * K * ||.(v1-v0).k1.||)
+ ((||.v0.||+3) |^len X * K * Sum F1) by A64,A84,XREAL_1:7;
((||.v0.||+3) |^ len X * K * ||.(v1-v0).k1.||)
+ ((||.v0.||+3) |^len X * K * Sum F1)
= ((||.v0.||+3) |^ len X * K) * (||.(v1-v0).k1.|| + Sum F1)
.= ((||.v0.||+3) |^ len X * K) * Sum F by RVSUM_1:76;
hence ex F be FinSequence of REAL
st dom F = Seg (k+1)
& ||.f/.v1 -f/.v0 .|| <= (||.v0.||+3) |^len X * K * Sum F
& for n be Nat st n in Seg (k+1)
holds ex i be Element of dom X
st i = len X -'(k+1) + n
& F.n = ||.(v1-v0).i.|| by A86,A87,A107,A108,XXREAL_0:2;
end;
end;
A109: for n be Nat holds P[n] from NAT_1:sch 2(A6,A16);
let v1 be Point of product X;
assume
A110: ||.v1-v0.|| <= 1;
consider g be Function such that
A111: v1 = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5;
dom g = Seg len (carr X) by A111,FINSEQ_1:def 3; then
reconsider Cv1 = v1 as FinSequence by A111,FINSEQ_1:def 2;
A112: len X -' len X = ( 0 + len X ) -' len X
.= 0 by NAT_D:34;
Cv1 | (len X -' len X) = {} by A112
.= Cv0 | (len X -' len X ) by A112; then
consider F be FinSequence of REAL such that
A113: dom F = Seg len X
& ||.f/.v1 - f/.v0.|| <= (||.v0.||+3) |^len X * K * Sum F
& for n be Nat st n in Seg len X holds
ex i be Element of dom X
st i = len X -'len X + n & F.n = ||.(v1-v0).i.|| by A109,A110;
for i be Element of dom X holds F.i = ||.(v1-v0).i.||
proof
let i be Element of dom X;
i in dom X; then
A116: i in Seg len X by FINSEQ_1:def 3;
reconsider n = i as Nat;
consider j be Element of dom X such that
A117: j = len X -'len X + n & F.n = ||.(v1-v0).j.|| by A113,A116;
thus thesis by A112,A117;
end;
hence thesis by A113,FINSEQ_1:def 3;
end;
theorem NDIFF824:
for x be Point of product X,
r be Real
st 0 < r
ex s be FinSequence of REAL,
Y be non empty non-empty FinSequence
st dom s = dom X & dom Y = dom X
& product Y c= Ball(x,r)
& for i be Element of dom X holds 0 < s.i & s.i < r
& Y.i = Ball(x.i,s.i)
proof
let x be Point of product X, r be Real;
assume
A1: 0 < r;
A2: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],
[:(multop X):],(productnorm X) #) by PRVECT_2:6;
consider s0 be Real such that
A3: 0 < s0 & s0 < r and
A4: sqrt((s0 * s0) * len X) < r by A1,NDIFF825;
set CST = len X |-> s0;
len X is natural Number & s0 is Element of REAL by XREAL_0:def 1; then
reconsider CST as Element of len X -tuples_on REAL by FINSEQ_2:112;
A5: for i be Element of dom X holds 0 < CST.i & CST.i < r
proof
let i be Element of dom X;
i in dom X; then
i in Seg len X by FINSEQ_1:def 3;
hence thesis by A3,FINSEQ_2:57;
end;
defpred P1[object, object] means
ex i be Element of dom X
st $1 = i & $2 = Ball(x.i,CST.i);
A6: for n being Nat st n in Seg len X holds
ex d being object st P1[n,d]
proof
let n be Nat;
assume n in Seg len X; then
reconsider i = n as Element of dom X by FINSEQ_1:def 3;
set d = Ball(x.i,CST.i);
take d;
thus thesis;
end;
consider Y being FinSequence such that
A7: dom Y = Seg len X
& for n being Nat st n in Seg len X holds
P1[n,Y . n] from FINSEQ_1:sch 1(A6);
not {} in rng Y
proof
assume {} in rng Y; then
consider z be object such that
A9: z in dom Y & {} = Y.z by FUNCT_1:def 3;
reconsider n = z as Nat by A9;
consider i be Element of dom X such that
A10: n = i & Y.n = Ball(x.i,CST.i) by A7,A9;
0 < CST.i by A5;
hence contradiction by A9,A10,NDIFF_8:14;
end; then
reconsider Y as non empty non-empty FinSequence
by A7,FINSEQ_1:def 3,RELAT_1:def 9;
take CST,Y;
thus dom CST = Seg len X by FUNCT_2:def 1
.= dom X by FINSEQ_1:def 3;
thus
A12: dom Y = dom X by A7,FINSEQ_1:def 3;
A14: for i be Element of dom X holds Y.i = Ball(x.i,CST.i)
proof
let i be Element of dom X;
A13: i in dom X;
reconsider n = i as Nat;
n in Seg len X by A13,FINSEQ_1:def 3; then
ex i be Element of dom X
st n = i & Y.n = Ball(x.i,CST.i) by A7;
hence Y.i = Ball(x.i, CST.i);
end;
for z be object st z in product Y holds z in Ball(x,r)
proof
let z be object;
assume z in product Y; then
consider g be Function such that
A15: z = g & dom g = dom Y
& for i be object st i in dom Y holds g.i in Y.i by CARD_3:def 5;
A16: dom carr X = dom X by DCARXX;
A17: dom g = dom carr X by A12,A15,DCARXX;
A18: for i0 be object st i0 in dom (carr X) holds
( g.i0 in (carr X).i0 &
ex i be Element of dom X
st i0 = i
& g.i in Ball(x.i,CST.i)
& g.i in the carrier of (X.i) )
proof
let i0 be object;
assume i0 in dom (carr X); then
reconsider i = i0 as Element of dom X by DCARXX;
g.i in Y.i by A12,A15; then
A19: g.i in Ball(x.i,CST.i) by A14; then
g.i in the carrier of (X.i);
hence thesis by A19,PRVECT_1:def 11;
end; then
A20: for i0 be object st i0 in dom (carr X)
holds g.i0 in (carr X).i0; then
reconsider x1 = g as Point of product X by A2,A17,CARD_3:def 5;
reconsider y1 = g as Element of product carr X by A20,A17,CARD_3:def 5;
reconsider xx1 = x-x1 as Element of product carr X by A2;
A21: ||.x-x1.|| = |. normsequence (X,xx1) .| by A2,PRVECT_2:def 12;
A22: len normsequence (X,xx1) = len X by PRVECT_2:def 11; then
A23: dom normsequence (X,xx1) = Seg len X by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
now
let i0 be Nat;
assume i0 in dom normsequence (X,xx1); then
reconsider i = i0 as Element of dom X by A23;
reconsider xx1i = xx1.i as Point of X.i;
reconsider yi = x.i as Point of X.i;
reconsider y1i = y1.i as Point of X.i;
i in dom X; then
A24: i in Seg len X by FINSEQ_1:def 3;
A25: normsequence (X,xx1).i = ||. xx1i .|| by PRVECT_2:def 11;
hence 0 <= normsequence(X,xx1).i0;
A26: xx1.i = x.i - y1.i by LOPBAN10:26;
ex j be Element of dom X
st i = j
& g.j in Ball(x.j,CST.j)
& g.j in the carrier of (X.j) by A16,A18; then
ex y be Point of X.i st
y = y1i & ||.x.i - y.|| < CST.i;
hence normsequence (X,xx1).i0 <= s0 by A24,A25,A26,FINSEQ_2:57;
end; then
|.normsequence (X,xx1).|
<= sqrt ( (s0*s0)*len X ) by A22,NDIFF823; then
||.x-x1.|| < r by A4,A21,XXREAL_0:2;
hence z in Ball(x,r) by A15;
end;
hence thesis by A5,A14,TARSKI:def 3;
end;
theorem
for X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be MultilinearOperator of X,Y
holds
( f is_continuous_on the carrier of product X
iff
f is_continuous_in 0.( product X ) )
&
( f is_continuous_on the carrier of product X
iff
f is Lipschitzian )
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be MultilinearOperator of X,Y;
A1: dom f = the carrier of product X by FUNCT_2:def 1;
A2: f/. 0. product X = 0.Y by FXZER;
A3: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
A4: f is_continuous_in 0.product X
implies f is Lipschitzian
proof
assume f is_continuous_in 0. product X; then
consider s be Real such that
A5: 0 < s
& for z be Point of product X st z in dom f &
||. z - 0. product X .|| < s
holds ||. f/.z - f/. 0. product X .|| < 1 by NFCONT_1:7;
set z = 0. product X;
consider s1 be FinSequence of REAL,
Balls be non empty non-empty FinSequence such that
A6: dom s1 = dom X & dom X = dom Balls
& product Balls c= Ball(0. product X,s)
& for i be Element of dom X
holds 0 < s1.i & s1.i < s & Balls.i = Ball(z.i,s1.i)
by A5,NDIFF824;
defpred P1[object , object] means
ex i be Element of dom X
st $1 = i & $2 = s1.i / 2;
A7: for n being Nat st n in Seg len X holds
ex d being Element of REAL st P1[n,d]
proof
let n be Nat;
assume n in Seg len X; then
reconsider i = n as Element of dom X by FINSEQ_1:def 3;
reconsider si = s1.i /2 as Element of REAL by XREAL_0:def 1;
take si;
thus P1[n,si];
end;
consider s2 being FinSequence of REAL such that
A8: len s2 = len X
& for n being Nat st n in Seg len X holds P1[n, s2 /. n]
from FINSEQ_4:sch 1(A7);
A9: dom s2 = Seg len X by A8,FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
A11: for i be Element of dom X holds s2.i = s1.i/2
proof
let i be Element of dom X;
i in dom X; then
i in Seg len X by FINSEQ_1:def 3; then
ex j be Element of dom X
st i = j & s2 /. i = s1.j / 2 by A8;
hence s2.i = s1.i / 2 by A9,PARTFUN1:def 6;
end;
A12: for i be Element of dom X holds 0 < s2.i & s2.i < s1.i
proof
let i be Element of dom X;
s2.i = s1.i / 2 & 0 < s1.i by A6,A11;
hence 0 < s2.i & s2.i < s1.i by XREAL_1:216;
end;
dom s2 = Seg len X by A9,FINSEQ_1:def 3; then
A13: len s2 = len X by FINSEQ_1:def 3;
A14: now
let x be Point of product X;
assume
A15: for i be Element of dom X holds ||.x.i.|| <= s2.i;
ex g be Function
st x = g & dom g = dom carr X
& for i be object st i in dom carr X
holds g.i in (carr X).i by A3,CARD_3:def 5; then
A16: dom x = dom X by DCARXX;
now
let i0 be object;
assume i0 in dom X; then
reconsider i = i0 as Element of dom X;
A18: z.i = 0.(X.i) by ZERXI;
||.x.i- 0.(X.i).|| <= s2.i by A15; then
A19: ||.0.(X.i) - x.i.|| <= s2.i by NORMSP_1:7;
s2.i = s1.i / 2 & 0 < s1.i by A6,A11; then
0 < s2.i & s2.i < s1.i by XREAL_1:216; then
||.0.(X.i) - x.i.|| < s1.i by A19,XXREAL_0:2; then
x.i in Ball(0.(X.i),s1.i);
hence x.i0 in Balls.i0 by A6,A18;
end; then
x in product Balls by A6,A16,CARD_3:def 5; then
x in Ball(0. product X,s) by A6; then
ex p be Point of product X
st x = p & ||. 0. product X - p .|| < s; then
A20: ||. x - 0. product X .|| < s by NORMSP_1:7;
||. f /. x - f /. 0. product X .|| < 1 by A1,A5,A20;
hence ||. f /. x .|| < 1 by A2;
end;
A21: 0 < Product s2 by A9,A12,PSPROD;
set K = 1/(Product s2);
now
let x be Point of product X;
consider F be FinSequence of REAL such that
A23: dom F = dom X
& ( for i be Element of dom X holds F.i = ||. x.i .|| )
& NrProduct x = Product F by LOPBAN10:def 9;
thus ||. f.x .|| <= K * NrProduct x
proof
per cases;
suppose
A24: for i be Element of dom X holds x.i <> 0.(X.i); then
A25: 0 < NrProduct x by LOPBAN10:27;
consider d be FinSequence of REAL such that
A26: dom d = dom X
& for i be Element of dom X holds d.i = ||.x.i.||"
by LOPBAN10:37;
dom d = Seg len X by A26,FINSEQ_1:def 3; then
A27: len d = len X by FINSEQ_1:def 3;
set F1 = mlt(s2,d);
A28: for i being Element of dom F holds d.i = (F.i)"
proof
let i be Element of dom F;
reconsider j = i as Element of dom X by A23;
d.j = ||.x.j.||" by A26;
hence thesis by A23;
end;
A32: dom F1 = dom X /\ dom X by A9,A26,VALUED_1:def 4
.= dom X;
s2 is Element of (len X) -tuples_on REAL
& d is Element of (len X) -tuples_on REAL
by A13,A27,FINSEQ_2:92; then
A33: Product F1 = (Product s2) * Product d by RVSUM_1:107
.= (Product s2) * (Product F)" by A23,A26,LOPBAN10:40,A28;
consider x1 be Element of product X such that
A34: for i be Element of dom X holds
x1.i = F1/.i * x.i by LOPBAN10:38;
A35: for i be Element of dom X holds ||. x1.i .|| <= s2.i
proof
let i be Element of dom X;
A36: x1.i = F1/.i * x.i by A34;
A37: F1/.i = F1.i by A32,PARTFUN1:def 6
.= s2.i * d.i by RVSUM_1:60
.= s2.i * (F.i)" by A23,A28;
A39: x1.i = s2.i * (||.x.i.||)" * x.i by A23,A36,A37;
A41: 0 <= s2.i by A12;
A42: |. s2.i * (||.x.i.||)".| = s2.i * ||.x.i.||"
by A41,COMPLEX1:43;
x.i <> 0.(X.i) by A24; then
A43: ||.x.i.|| <> 0 by NORMSP_0:def 5;
||.x1.i.||
= s2.i * ||.x.i.||" * ||.x.i.|| by A39,A42,NORMSP_1:def 1
.= s2.i * (||.x.i.||" * ||.x.i.|| )
.= s2.i * 1 by A43,XCMPLX_0:def 7;
hence thesis;
end;
A44: ||. f/. x1 .|| < 1 by A14,A35;
A45: |. (Product F)".| = (Product F)" by A23,ABSVALUE:def 1;
A46: |. (Product s2) * (Product F)" .|
= |. Product s2.| * |. (Product F) " .| by COMPLEX1:65
.= Product s2 * (Product F)" by A21,A45,COMPLEX1:43;
f.x1 = (Product s2) * (Product F)" * f.x
by A32,A33,A34,LOPBAN10:39; then
||.f. x1.|| = (Product s2) * (Product F)" * ||.f.x.||
by A46,NORMSP_1:def 1; then
(Product s2) * ((Product F)" * ||.f.x.||) / (Product s2)
< 1 / (Product s2) by A21,A44,XREAL_1:74; then
(Product F)" * ||.f.x.|| < K by A21,XCMPLX_1:89; then
Product F * ( (Product F)" * ||.f.x.|| ) < K * Product F
by A23,A25,XREAL_1:68; then
( Product F * (Product F)") * ||.f.x.|| < K * Product F; then
1 * ||.f.x.|| < K * Product F by A23,A25,XCMPLX_0:def 7;
hence ||.f.x .|| <= K * NrProduct x by A23;
end;
suppose
A47: ex i be Element of dom X st x.i = 0.(X.i); then
A48: f.x = 0.Y by LOPBAN10:36;
consider i be Element of dom X such that
A49: x.i = 0.(X.i) by A47;
A50: F.i = ||. x.i .|| by A23;
F.i = 0 by A49,A50; then
Product F = 0 by A23,RVSUM_1:103;
hence ||.f. x .|| <= K * NrProduct x by A23,A48;
end;
end;
end;
hence f is Lipschitzian by A21;
end;
f is Lipschitzian implies
f is_continuous_on the carrier of product X
proof
assume f is Lipschitzian; then
consider K being Real such that
A52: 0 <= K and
A53: for x being Point of product X
holds ||. f.x .|| <= K * NrProduct x;
for v0 being Point of product X
for r being Real st v0 in the carrier of product X & 0 < r
holds
ex s being Real
st 0 < s
& for v1 being Point of product X
st v1 in the carrier of product X
& ||. v1 - v0 .|| < s holds ||. f /. v1 - f /. v0 .|| < r
proof
let v0 being Point of product X, r0 being Real;
assume
A54: v0 in the carrier of product X & 0 < r0;
set r = r0 / 2;
A58: 0 < r & r < r0 by A54,XREAL_1:216;
set L = ||.v0.|| + 1;
consider M be Real such that
A59: 0 <= M
& for v1 be Point of product X st ||.v1-v0.|| <= 1 holds
ex F be FinSequence of REAL
st dom F = dom X
& ||. f/.v1 - f/.v0 .|| <= M * K * Sum F
& for i be Element of dom X
holds F.i = ||.(v1-v0).i.|| by A52,A53,LM01;
set BL = M * K * len X + 1;
set s = min(r/BL,1);
A64: 0 < s & s <= 1 & s <= r / BL by A52,A54,A59,XXREAL_0:17,21;
0 + M * K * len X <= BL by XREAL_1:7; then
(M * K * len X) * s <= (r / BL) * BL by A52,A59,A64,XREAL_1:66; then
A65: (M * K * len X) * s <= r by A52,A59,XCMPLX_1:87;
take s;
thus 0 < s by A52,A54,A59,XXREAL_0:21;
let v1 be Point of product X;
assume
A66: v1 in the carrier of product X & ||. v1 - v0 .|| < s;
reconsider w1 = v1 - v0 as Element of product X;
consider H be FinSequence of REAL such that
A67: dom H = dom X
& ||.f/.v1 - f/.v0.|| <= M * K * Sum H
& for i be Element of dom X holds H.i = ||.w1.i.||
by A59,A64,A66,XXREAL_0:2;
for i be Nat st i in dom H holds 0 <= H.i
proof
let i be Nat;
assume i in dom H; then
reconsider j = i as Element of dom X by A67;
H.j = ||.w1.j.|| by A67;
hence thesis;
end; then
A68: 0 <= Sum H by RVSUM_1:84;
A69: for i be Element of dom X holds ||.w1.i.|| < s
proof
let i be Element of dom X;
||.w1.i.|| <= ||.v1-v0.|| by A3,PRVECT_2:10;
hence ||.w1.i.|| < s by A66,XXREAL_0:2;
end;
set CST = len H |-> s;
A71: H is Element of len H -tuples_on REAL by FINSEQ_2:92;
len H is natural Number & s is Element of REAL by XREAL_0:def 1; then
reconsider CST as Element of len H -tuples_on REAL by FINSEQ_2:112;
dom H = Seg len X by A67,FINSEQ_1:def 3; then
A72: len H = len X by FINSEQ_1:def 3;
for i be Nat st i in Seg len H holds H.i <= CST.i
proof
let i0 be Nat;
assume
A73: i0 in Seg len H; then
reconsider i = i0 as Element of dom X by A67,FINSEQ_1:def 3;
A74: ||.w1.i.|| < s by A69;
H.i <= s by A67,A74;
hence thesis by A73,FINSEQ_2:57;
end; then
Sum H <= Sum CST by A71,RVSUM_1:82; then
Sum H <= s * len X by A72,RVSUM_1:80; then
(M * K) * Sum H <= (M * K) * (s * len X)
by A52,A59,A68,XREAL_1:66; then
||.f/.v1 - f/.v0.|| <= M * K * (s * len X) by A67,XXREAL_0:2; then
||.f/.v1 -f/.v0 .|| <= r by A65,XXREAL_0:2;
hence ||.f/.v1 -f/.v0 .|| < r0 by A58,XXREAL_0:2;
end;
hence f is_continuous_on the carrier of product X by A1,NFCONT_1:19;
end;
hence thesis by A4;
end;