:: Continuity of Bounded Linear Operators on Normed Linear Spaces
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received September 29, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
NAT_1, SUBSET_1, RELAT_1, LOPBAN_1, MSSUBFAM, TARSKI, ARYTM_3, VALUED_1,
FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1,
NFCONT_1, NFCONT_2, DUALSP01, FUNCT_5, UNIALG_1, FUNCOP_1, SEQ_4,
XXREAL_2, XXREAL_0, XBOOLE_0, RLVECT_1, CFCONT_1, REWRITE1, METRIC_1,
COMPLEX1, TOPS_1, LOPBAN_8;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1,
PARTFUN1, FUNCT_2, FUNCT_5, BINOP_1, FUNCOP_1, NUMBERS, XCMPLX_0,
XXREAL_0, XXREAL_2, XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQ_4,
STRUCT_0, PRE_TOPC, RLVECT_1, VECTSP_1, NORMSP_0, NORMSP_1, NORMSP_3,
LOPBAN_1, LOPBAN_5, NFCONT_1, NFCONT_2, PRVECT_3, DUALSP01;
constructors SEQ_2, SEQ_4, NFCONT_1, NFCONT_2, COMSEQ_2, RELSET_1, NAT_D,
RSSPACE3, NDIFF_7, REALSET1, NORMSP_3, LOPBAN_5;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0,
VALUED_1, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1, ORDINAL1, LOPBAN_1,
PRVECT_3, NORMSP_0, NAT_1, NORMSP_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities RLVECT_1, LOPBAN_1, NORMSP_0, BINOP_1, PRVECT_3, LOPBAN_5;
expansions NFCONT_1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, FUNCT_1, FUNCT_2,
ORDINAL1, LOPBAN_1, PARTFUN1, NFCONT_1, VECTSP_1, SEQ_2, COMPLEX1,
XXREAL_0, XCMPLX_1, NORMSP_0, PRVECT_3, LOPBAN_3, RLVECT_4, NFCONT_2,
NDIFF_8, FUNCOP_1, NORMSP_1, NORMSP_3, DUALSP01, SEQ_4, FUNCT_5,
INTEGR20, VALUED_1, XREAL_1, LOPBAN_2, LOPBAN_7;
schemes FUNCT_2, INTEGR20;
begin :: Uniform Continuity and Lipschitz Continuity of
:: Bounded Linear Operators
reserve S,T,W,Y for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve Z for Subset of S;
reserve i,n for Nat;
theorem Th020:
for E,F be RealNormSpace,
E1 be Subset of E,
f be PartFunc of E,F
st E1 is dense & F is complete & dom f = E1
& f is_uniformly_continuous_on E1
holds
(ex g be Function of E,F
st g|E1 = f
& g is_uniformly_continuous_on the carrier of E
& ( for x be Point of E holds
ex seq be sequence of E
st rng seq c= E1 & seq is convergent
& lim seq = x
& f/*seq is convergent
& g.x = lim f/*seq )
& ( for x be Point of E,
seq be sequence of E
st rng seq c= E1 & seq is convergent
& lim seq = x
holds
f/*seq is convergent
& g.x = lim f/*seq )
)
&
(for g1,g2 be Function of E,F
st g1|E1 = f
& g1 is_continuous_on the carrier of E
& g2|E1 = f
& g2 is_continuous_on the carrier of E
holds g1 = g2)
proof
let E,F be RealNormSpace,
E1 be Subset of E,
f be PartFunc of E,F;
assume that
A1: E1 is dense and
A2: F is complete and
A3: dom f = E1 and
A4: f is_uniformly_continuous_on E1;
A6:
for x be Point of E, seq be sequence of E
st rng seq c= E1 & seq is convergent holds
for s being Real st 0 < s holds
ex n being Nat
st for m being Nat st n <= m holds
||.(((f/*seq) . m) - ((f/*seq) . n)).|| < s
proof
let x be Point of E,
seq be sequence of E;
assume that
A7: rng seq c= E1 and
A8: seq is convergent;
set fseq = f/*seq;
let r be Real;
assume 0 < r; then
consider s being Real such that
A10: 0 < s
& for x1, x2 being Point of E
st x1 in E1 & x2 in E1 & ||.x1 - x2.|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A4,NFCONT_2:def 1;
consider n being Nat such that
A11: for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s by A8,A10,LOPBAN_3:4;
take n;
let m be Nat;
assume n <= m; then
A13: ||.((seq . m) - (seq . n)).|| < s by A11;
A14: n in NAT & m in NAT by ORDINAL1:def 12;
B14: seq . m in rng seq & seq . n in rng seq
by FUNCT_2:4,ORDINAL1:def 12;
f /. (seq.m) = fseq.m & f /. (seq.n) = fseq.n by A3,A7,A14,FUNCT_2:109;
hence ||.fseq. m - fseq.n.|| < r by A7,A10,A13,B14;
end;
A16:
for x be Point of E, seq be sequence of E
st rng seq c= E1 & seq is convergent
holds f/*seq is convergent
proof
let x be Point of E,
seq be sequence of E;
assume that
A17: rng seq c= E1 and
A18: seq is convergent;
for s being Real st 0 < s holds
ex n being Nat
st for m being Nat st n <= m holds
||.(((f/*seq) . m) - ((f/*seq) . n)).|| < s by A6,A17,A18;
hence thesis by A2,LOPBAN_1:def 15,LOPBAN_3:5;
end;
A19:
for x be Point of E, seq1,seq2 be sequence of E
st rng seq1 c= E1 & seq1 is convergent & lim seq1 = x
& rng seq2 c= E1 & seq2 is convergent & lim seq2 = x
holds lim (f/*seq1) = lim (f/*seq2)
proof
let x be Point of E,
seq1,seq2 be sequence of E;
assume that
A20: rng seq1 c= E1 & seq1 is convergent & lim seq1 = x and
A21: rng seq2 c= E1 & seq2 is convergent & lim seq2 = x;
deffunc F2(Nat) = seq1.$1;
deffunc F3(Nat) = seq2.$1;
consider s being sequence of the carrier of E such that
A22: for n being Nat holds
s . (2 * n) = F2(n) & s . ((2 * n) + 1) = F3(n)
from INTEGR20:sch 1;
B23:
now
let y be object;
assume y in rng s; then
consider i be object such that
A23: i in NAT & y=s.i by FUNCT_2:11;
reconsider i as Nat by A23;
consider k be Nat such that
A24: i=2*k or i=2*k+1 by INTEGR20:14;
reconsider k1=k, i1=i as Element of NAT by ORDINAL1:def 12;
per cases by A24;
suppose
i = 2*k1; then
s.i = seq1.k1 by A22; then
s.i in rng seq1 by FUNCT_2:4;
hence y in E1 by A20,A23;
end;
suppose
i = 2*k1+1; then
s.i = seq2.k1 by A22; then
s.i in rng seq2 by FUNCT_2:4;
hence y in E1 by A21,A23;
end;
end; then
A28: rng s c= E1 by TARSKI:def 3;
now
let p be Real;
assume
A30: 0 < p; then
consider n1 be Nat such that
A31: for m be Nat st n1 <= m holds ||. seq1.m - x .|| < p
by A20,NORMSP_1:def 7;
consider n2 be Nat such that
A32: for m be Nat st n2 <= m holds ||. seq2.m - x .||<p
by A21,A30,NORMSP_1:def 7;
reconsider n3=max(n1,n2) as Nat by TARSKI:1;
A33: n1 <= n3 & n2 <= n3 by XXREAL_0:25;
reconsider n=2*n3+1 as Nat;
take n;
let m be Nat;
assume
A34: n <= m;
consider k be Nat such that
A35: m=2*k or m=2*k+1 by INTEGR20:14;
reconsider k1=k, m1=m as Element of NAT by ORDINAL1:def 12;
per cases by A35;
suppose
A36: m=2*k1;
then
A37: s.m = seq1.k1 by A22;
A38: 2*n3 <= (2*k)-1 by A34,A36,XREAL_1:19;
2*k-1 < (2*k-1)+1 by XREAL_1:145; then
2*n3 <= 2*k by A38,XXREAL_0:2; then
2*n3/2 <= 2*k/2 by XREAL_1:72; then
n1 <= k by A33,XXREAL_0:2;
hence ||. s.m - x .||<p by A31,A37;
end;
suppose
A39: m=2*k+1;
then
A40: s.m1 = seq2.k1 by A22;
(2*n3+1)-1 <= (2*k+1)-1 by A34,A39,XREAL_1:13; then
2*n3/2 <= 2*k/2 by XREAL_1:72; then
n2 <= k by A33,XXREAL_0:2;
hence ||. s.m - x .||<p by A32,A40;
end;
end;
then
A42: f/*s is convergent by A16,A28,NORMSP_1:def 6;
for i being Nat holds
(f/*s).(2 * i) = (f/*seq1).i & (f/*s).((2 * i) + 1) = (f/*seq2).i
proof
let i be Nat;
A43: i in NAT by ORDINAL1:def 12;
2*i in NAT by ORDINAL1:def 12;
hence (f/*s).(2 * i)
= f/.(s.(2*i)) by A3,B23,FUNCT_2:109,TARSKI:def 3
.= f/.(seq1.i) by A22
.= (f/*seq1).i by A3,A20,A43,FUNCT_2:109;
thus (f/*s).(2 * i+1)
= f/.(s.(2*i+1)) by A3,B23,FUNCT_2:109,TARSKI:def 3
.= f/.(seq2.i) by A22
.= (f/*seq2).i by A3,A21,A43,FUNCT_2:109;
end;
then
lim (f/*seq1) = lim (f/*s)
& lim (f/*seq2) = lim (f/*s) by A42,INTEGR20:18;
hence thesis;
end;
defpred P1[object,object] means
ex seq be sequence of E
st rng seq c= E1 & seq is convergent & lim seq = $1
& f/*seq is convergent & $2= lim (f/*seq);
A46: for x being Element of E
ex y being Element of F st P1[x,y]
proof
let x be Element of E;
consider seq being sequence of E such that
A47: rng seq c= E1 & seq is convergent & lim seq = x by A1,NORMSP_3:14;
take y = lim (f/*seq);
thus thesis by A16,A47;
end;
consider g being Function of E,F such that
A49: for x being Element of E holds P1[x,g . x]
from FUNCT_2:sch 3(A46);
A50: dom g = the carrier of E by FUNCT_2:def 1;
A51: dom f = (the carrier of E) /\ E1 by A3,XBOOLE_1:28
.= dom g /\ E1 by FUNCT_2:def 1;
A52: f is_continuous_on E1 by A4,NFCONT_2:7;
for x being object st x in dom f holds f . x = g . x
proof
let x0 be object;
assume
A53: x0 in dom f;
then
A54: x0 in dom g & x0 in E1 by A51,XBOOLE_0:def 4;
reconsider x=x0 as Point of E by A53;
reconsider seq1 = NAT --> x as sequence of E;
for n be Nat holds seq1.n = x by FUNCOP_1:7,ORDINAL1:def 12; then
A56: seq1 is convergent & lim seq1 = x by NORMSP_3:23;
A58: rng seq1 c= E1
proof
let y be object;
assume y in rng seq1;
then
consider i be object such that
A57: i in NAT & y=seq1.i by FUNCT_2:11;
reconsider i as Nat by A57;
thus y in E1 by A54,A57,FUNCOP_1:7;
end; then
f /* seq1 is convergent & lim f/*seq1 = f/. (lim seq1)
by A52,A54,A56,NFCONT_1:18; then
A59: lim f/*seq1 =f.x by A53,A56,PARTFUN1:def 6;
consider seq2 be sequence of E such that
A60: rng seq2 c= E1 & seq2 is convergent & lim seq2 = x
& f/*seq2 is convergent & g.x= lim (f/*seq2) by A49;
thus thesis by A19,A56,A58,A59,A60;
end; then
A61: g|E1 = f by A51,FUNCT_1:46;
A62: for x be Point of E, seq be sequence of E
st rng seq c= E1 & seq is convergent
& lim seq = x
holds f/*seq is convergent & g.x = lim f/*seq
proof
let x be Point of E, seq be sequence of E;
assume
A63: rng seq c= E1 & seq is convergent & lim seq = x;
consider seq1 be sequence of E such that
A64: rng seq1 c= E1 & seq1 is convergent
& lim seq1 = x
& f/*seq1 is convergent
& g.x = lim f/*seq1 by A49;
thus f/*seq is convergent by A16,A63;
thus thesis by A19,A63,A64;
end;
for r being Real st 0 < r holds
ex s being Real
st 0 < s
& for x1, x2 being Point of E
st x1 in the carrier of E & x2 in the carrier of E
& ||.x1 - x2.|| < s holds
||.g /. x1 - g/. x2.|| < r
proof
let r0 be Real;
assume
A65: 0 < r0;
set r1 = r0/2;
A66: 0 < r1 & r1 < r0 by A65,XREAL_1:215,216;
set r = r1/3;
A67: 0 < r & r < r1 by A66,XREAL_1:221,222;
consider s0 being Real such that
A68: 0 < s0
& for x1, x2 being Point of E
st x1 in E1& x2 in E1
& ||.x1 - x2.|| < s0 holds
||.f /. x1 - f/. x2.|| < r by A4,A66,NFCONT_2:def 1,XREAL_1:222;
set s = s0/3;
A69: 0 < s & s < s0 by A68,XREAL_1:221,222;
take s;
thus 0 < s by A68,XREAL_1:222;
let x1, x2 be Point of E;
assume
A70: x1 in the carrier of E & x2 in the carrier of E
& ||.x1 - x2.|| < s;
consider seq1 be sequence of E such that
A71: rng seq1 c= E1 & seq1 is convergent
& lim seq1 = x1
& f/*seq1 is convergent
& g.x1 = lim f/*seq1 by A49;
consider M10 being Nat such that
A72: for n being Nat st M10 <= n holds
||. seq1.n - x1.|| < s by A69,A71,NORMSP_1:def 7;
consider M11 being Nat such that
A73: for n being Nat st M11 <= n holds
||. (f/*seq1).n - g.x1.|| < r by A67,A71,NORMSP_1:def 7;
set M1 = M10 + M11;
A74: M10 + 0 <= M1 & M11 + 0 <= M1
by XREAL_1:7;
consider seq2 be sequence of E such that
A75: rng seq2 c= E1 & seq2 is convergent
& lim seq2 = x2
& f/*seq2 is convergent
& g.x2 = lim f/*seq2 by A49;
consider M20 being Nat such that
A76: for n being Nat st M20 <= n holds
||. seq2.n - x2.|| < s by A69,A75,NORMSP_1:def 7;
consider M21 being Nat such that
A77: for n being Nat st M21 <= n holds
||. (f/*seq2).n - g.x2.|| < r by A67,A75,NORMSP_1:def 7;
set M2 = M20 + M21;
A78: M20 + 0 <= M2 & M21 + 0 <= M2 by XREAL_1:7;
set n = M1 + M2;
A82: ||. seq1.n - x1.|| < s & ||. (f/*seq1).n - g.x1.|| < r
by A72,A73,A74,XREAL_1:7;
A83: ||. seq2.n - x2.|| < s & ||. (f/*seq2).n - g.x2.|| < r
by A76,A77,A78,XREAL_1:7;
seq2.n - seq1.n
= seq2.n - x2 + x2 - seq1.n by RLVECT_4:1
.= ( seq2.n - x2 ) + ( x2-x1 + x1) - seq1.n by RLVECT_4:1
.= ( seq2.n - x2 ) + ( x2-x1 ) + x1 - seq1.n by RLVECT_1:def 3
.= ( seq2.n - x2 ) + ( x2-x1) + ( x1 - seq1.n ) by RLVECT_1:28; then
A84: ||. seq2.n - seq1.n.||
<= ||. ( seq2.n - x2 ) + ( x2-x1 ) .|| + ||. x1 - seq1.n .||
by NORMSP_1:def 1;
||. ( seq2.n - x2 ) + ( x2-x1 ) .||
<= ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| by NORMSP_1:def 1; then
||. ( seq2.n - x2 ) + ( x2-x1 ) .|| + ||. x1 - seq1.n .||
<= ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| + ||. x1 - seq1.n .||
by XREAL_1:7; then
A85: ||. seq2.n - seq1.n.||
<= ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| + ||. x1 - seq1.n .||
by A84,XXREAL_0:2;
||. x2-x1 .|| < s by A70,NORMSP_1:7; then
A86: ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| < s+s by A83,XREAL_1:8;
||. x1 - seq1.n .|| < s by A82,NORMSP_1:7; then
||. ( seq2.n - x2 ).|| + ||. x2-x1 .||+ ||. x1 - seq1.n .||
< s+s+s by A86,XREAL_1:8; then
||. seq2.n - seq1.n.|| < s+s+s by A85,XXREAL_0:2;
then
A87: ||. seq1.n - seq2.n.|| < s + s+ s by NORMSP_1:7;
A88: n in NAT by ORDINAL1:def 12;
seq2.n in rng seq2 & seq1.n in rng seq1 by FUNCT_2:4,ORDINAL1:def 12;
then
A89: ||.f /. (seq1.n) - f/. (seq2.n).|| < r by A68,A71,A75,A87;
g /. x1 - g/. x2
= g /. x1 - f /. (seq1.n) + f /. (seq1.n) - g/. x2 by RLVECT_4:1
.= (g /. x1 - f /. (seq1.n))
+ ( f /. (seq1.n) - f /. (seq2.n) + f /. (seq2.n) )
- g/. x2 by RLVECT_4:1
.= (g /. x1 - f /. (seq1.n))
+ ( f /. (seq1.n) - f /. (seq2.n) ) + f /. (seq2.n)
- g/. x2 by RLVECT_1:def 3
.= (g /. x1 - f /. (seq1.n))
+ ( f /. (seq1.n) - f /. (seq2.n) )
+ ( f /. (seq2.n) - g/. x2 ) by RLVECT_1:28; then
A90: ||.g /. x1 - g/. x2.||
<= ||. (g /. x1 - f /. (seq1.n))
+ ( f /. (seq1.n) - f /. (seq2.n) ) .||
+ ||. f /. (seq2.n) - g/. x2 .|| by NORMSP_1:def 1;
||. (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) ) .||
<= ||. g /. x1 - f /. (seq1.n) .||
+ ||. f /. (seq1.n) - f /. (seq2.n) .|| by NORMSP_1:def 1; then
||. (g /. x1 - f /. (seq1.n))
+ ( f /. (seq1.n) - f /. (seq2.n) ) .||
+ ||. f /. (seq2.n) - g/. x2 .||
<= ||. g /. x1 - f /. (seq1.n) .||
+ ||. f /. (seq1.n) - f /. (seq2.n) .||
+ ||. f /. (seq2.n) - g/. x2 .|| by XREAL_1:7; then
A91: ||.g /. x1 - g/. x2.||
<= ||. g /. x1 - f /. (seq1.n) .||
+ ||. f /. (seq1.n) - f /. (seq2.n) .||
+ ||. f /. (seq2.n) - g/. x2 .|| by A90,XXREAL_0:2;
A92: ||. g /. x1 - f /. (seq1.n) .||
= ||. f /. (seq1.n) - g . x1 .|| by NORMSP_1:7
.= ||. (f/*seq1).n - g . x1 .|| by A3,A71,A88,FUNCT_2:109;
A93: ||. f /. (seq2.n) - g/. x2 .||
= ||. (f/*seq2).n - g . x2 .|| by A3,A75,A88,FUNCT_2:109;
||. g /. x1 - f /. (seq1.n) .||
+ ||. f /. (seq1.n) - f /. (seq2.n) .||
<= r+r by A82,A89,A92,XREAL_1:7; then
||. g /. x1 - f /. (seq1.n) .||
+ ||. f /. (seq1.n) - f /. (seq2.n) .||
+ ||. f /. (seq2.n) - g/. x2 .||
< r+r+r by A83,A93,XREAL_1:8; then
||.g /. x1 - g/. x2.|| < r+r+r by A91,XXREAL_0:2;
hence ||.g /. x1 - g/. x2.|| < r0 by A66,XXREAL_0:2;
end;
hence ex g be Function of E,F
st g | E1 = f
& g is_uniformly_continuous_on the carrier of E
& ( for x be Point of E holds
ex seq be sequence of E
st rng seq c= E1 & seq is convergent
& lim seq = x
& f/*seq is convergent
& g.x = lim f/*seq )
& ( for x be Point of E,
seq be sequence of E
st rng seq c= E1 & seq is convergent
& lim seq = x
holds f/*seq is convergent & g.x = lim f/*seq )
by A49,A50,A61,A62,NFCONT_2:def 1;
let g1,g2 be Function of E,F such that
A95: g1|E1 = f & g1 is_continuous_on the carrier of E and
A96: g2|E1 = f & g2 is_continuous_on the carrier of E;
for x being Element of E holds g1 . x = g2.x
proof
let x be Element of E;
consider seq being sequence of E such that
A97: rng seq c= E1 & seq is convergent & lim seq = x by A1,NORMSP_3:14;
A106: g1/*seq = f/*seq by A3,A95,A97,FUNCT_2:117
.= g2/*seq by A3,A96,A97,FUNCT_2:117;
thus g1.x = g1/. (lim seq) by A97
.= lim g2/*seq by A95,A97,A106,NFCONT_1:18
.= g2/.x by A96,A97,NFCONT_1:18
.= g2.x;
end;
hence g1 = g2 by FUNCT_2:def 8;
end;
theorem
for E,F,G be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators (E,F),
g be Point of R_NormSpace_of_BoundedLinearOperators (F,G)
holds
ex h be Point of R_NormSpace_of_BoundedLinearOperators (E,G)
st h = g*f
& ||.h.|| <= ||.g.||*||.f.||
proof
let E,F,G be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators (E,F),
g be Point of R_NormSpace_of_BoundedLinearOperators (F,G);
reconsider Lf=f as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
reconsider Lg=g as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
set Lh = Lg*Lf;
reconsider Lh as Lipschitzian LinearOperator of E,G by LOPBAN_2:2;
reconsider h = Lh as Point of R_NormSpace_of_BoundedLinearOperators (E,G)
by LOPBAN_1:def 9;
take h;
thus h = g * f;
A8: ||.h.|| = upper_bound (PreNorms(modetrans(h,E,G))) by LOPBAN_1:def 13
.= upper_bound PreNorms(Lh) by LOPBAN_1:29;
for t be Real st t in PreNorms(Lh)
holds t <= ||.g.|| * ||.f.||
proof
let t be Real;
assume t in PreNorms(Lh); then
consider w be Point of E such that
A9: t = ||. Lh.w .|| & ||.w.|| <= 1;
A10: ||. Lh.w .|| = ||.Lg.(Lf.w).|| by FUNCT_2:15;
A11: ||. Lf.w .|| <= ||.f.|| * ||.w.|| by LOPBAN_1:32;
||.f.|| * ||.w.|| <= ||.f.|| * 1 by A9,XREAL_1:64; then
A12: ||. Lf.w .|| <= ||.f.|| by A11,XXREAL_0:2;
A13: ||.Lg. (Lf.w) .|| <= ||.g.|| * ||. (Lf.w) .|| by LOPBAN_1:32;
||.g.|| * ||. (Lf.w) .|| <= ||.g.|| * ||.f.|| by A12,XREAL_1:64;
hence thesis by A9,A10,A13,XXREAL_0:2;
end;
hence ||.h.|| <= ||.g.|| * ||.f.|| by A8,SEQ_4:45;
end;
theorem LMCONT1:
for E,F be RealNormSpace,
L be Lipschitzian LinearOperator of E,F
holds
L is_Lipschitzian_on the carrier of E &
L is_uniformly_continuous_on the carrier of E
proof
let E,F be RealNormSpace,
L be Lipschitzian LinearOperator of E,F;
consider K being Real such that
A2: 0 <= K &
for x being VECTOR of E holds ||. L.x.|| <= K * ||.x.||
by LOPBAN_1:def 8;
set r = K+1;
A3: K + 0 < r by XREAL_1:8;
set E0 = the carrier of E;
for x1, x2 being Point of E st x1 in E0 & x2 in E0 holds
||.L/. x1 - L/. x2.|| <= r * ||. x1 -x2.||
proof
let x1, x2 be Point of E;
L/.x1 - L/.x2 = L.x1+(-1)*(L.x2) by RLVECT_1:16
.= L.x1+L. ((-1)*x2) by LOPBAN_1:def 5
.= L.(x1+(-1)*x2) by VECTSP_1:def 20
.= L.(x1-x2) by RLVECT_1:16; then
A8: ||.L/. x1 - L/. x2.|| <= K * ||.x1-x2.|| by A2;
K * ||.x1-x2.|| <= r * ||.x1-x2.|| by A3,XREAL_1:64;
hence thesis by A8,XXREAL_0:2;
end;
hence L is_Lipschitzian_on E0 by A2,FUNCT_2:def 1;
hence L is_uniformly_continuous_on E0 by NFCONT_2:9;
end;
theorem
for E,F be RealNormSpace,
E1 be SubRealNormSpace of E,
f be Point of R_NormSpace_of_BoundedLinearOperators (E1,F)
st F is complete
& ex E0 be Subset of E st E0 = the carrier of E1 & E0 is dense
holds
(ex g be Point of R_NormSpace_of_BoundedLinearOperators (E,F)
st dom g = the carrier of E
& g| the carrier of E1 = f
& ||.g.|| = ||.f.||
& ex Lf be PartFunc of E,F st Lf = f
& (for x be Point of E
holds ex seq be sequence of E
st rng seq c= the carrier of E1
& seq is convergent
& lim seq = x
& Lf/*seq is convergent
& g.x = lim Lf/*seq)
& (for x be Point of E, seq be sequence of E
st rng seq c= the carrier of E1
& seq is convergent
& lim seq = x
holds Lf/*seq is convergent & g.x = lim Lf/*seq)
)
&
(for g1,g2 be Point of R_NormSpace_of_BoundedLinearOperators (E,F)
st g1| the carrier of E1 = f
& g2| the carrier of E1 = f
holds g1 = g2)
proof
let E,F be RealNormSpace,
E1 be SubRealNormSpace of E,
f be Point of R_NormSpace_of_BoundedLinearOperators (E1,F);
assume that
A1: F is complete and
A2: ex E0 be Subset of E
st E0 = the carrier of E1 & E0 is dense;
consider E0 be Subset of E such that
A3: E0 = the carrier of E1 & E0 is dense by A2;
reconsider L = f as Lipschitzian LinearOperator of E1,F by LOPBAN_1:def 9;
A4: dom L = the carrier of E1 & rng L c= the carrier of F by FUNCT_2:def 1;
then
L in PFuncs (the carrier of E,the carrier of F) by A3,PARTFUN1:def 3; then
reconsider Lf = L as PartFunc of E,F by PARTFUN1:46;
A5: dom Lf = E0 by A3,FUNCT_2:def 1;
consider K being Real such that
A6: 0 <= K &
for x being VECTOR of E1 holds ||. L.x.|| <= K * ||.x.||
by LOPBAN_1:def 8;
set r = K+1;
A7: K + 0 < r by XREAL_1:8;
for x1, x2 being Point of E st x1 in E0 & x2 in E0 holds
||.Lf/. x1 - Lf/. x2.|| <= r * ||. x1 -x2.||
proof
let x1, x2 be Point of E;
assume x1 in E0 & x2 in E0; then
reconsider xx1 = x1, xx2 = x2 as Point of E1 by A3;
A10: (-1)*x2 =(-1)*xx2 by NORMSP_3:28;
A11: x1-x2 = x1+ (-1)*x2 by RLVECT_1:16
.= xx1+(-1)*xx2 by A10,NORMSP_3:28
.= xx1 -xx2 by RLVECT_1:16;
A12: Lf/.x1 = L.xx1 by A4,PARTFUN1:def 6;
Lf/.x2 = L.xx2 by A4,PARTFUN1:def 6;
then
Lf/.x1 - Lf/.x2 = L.xx1+(-1)*(L.xx2) by A12,RLVECT_1:16
.= L.xx1+L. ((-1)*xx2) by LOPBAN_1:def 5
.= L.(xx1+(-1)*xx2) by VECTSP_1:def 20
.= L.(xx1-xx2) by RLVECT_1:16; then
||.Lf/. x1 - Lf/. x2.|| <= K * ||.xx1-xx2.|| by A6; then
A14: ||.Lf/. x1 - Lf/. x2.|| <= K * ||.x1-x2.|| by A11,NORMSP_3:28;
K * ||.x1-x2.|| <= r * ||.x1-x2.|| by A7,XREAL_1:64;
hence thesis by A14,XXREAL_0:2;
end; then
Lf is_Lipschitzian_on E0 by A3,A6,FUNCT_2:def 1; then
A15: Lf is_uniformly_continuous_on E0 by NFCONT_2:9;
A16: (ex Pg be Function of E,F
st Pg|E0 = Lf
& Pg is_uniformly_continuous_on the carrier of E
& (for x be Point of E
holds ex seq be sequence of E
st rng seq c= E0 & seq is convergent
& lim seq = x
& Lf/*seq is convergent
& Pg.x = lim Lf/*seq)
& (for x be Point of E,
seq be sequence of E
st rng seq c= E0 & seq is convergent
& lim seq = x
holds Lf/*seq is convergent & Pg.x = lim Lf/*seq ) )
& (for Pg1,Pg2 be Function of E,F
st Pg1|E0 = Lf
& Pg1 is_continuous_on the carrier of E
& Pg2|E0 = Lf
& Pg2 is_continuous_on the carrier of E
holds Pg1 = Pg2)
by A1,A3,A5,A15,Th020;
consider Pg be Function of E,F such that
A17: Pg|E0 = Lf and
A18: Pg is_uniformly_continuous_on the carrier of E and
A19: for x be Point of E holds
ex seq be sequence of E
st rng seq c= E0 & seq is convergent
& lim seq = x
& Lf/*seq is convergent
& Pg.x = lim Lf/*seq
and
A20: for x be Point of E, seq be sequence of E
st rng seq c= E0 & seq is convergent
& lim seq = x
holds Lf/*seq is convergent & Pg.x = lim Lf/*seq and
A21: for x be Point of E
holds ex seq be sequence of E
st rng seq c= E0 & seq is convergent
& lim seq = x
& Lf/*seq is convergent
& Pg.x = lim Lf/*seq and
A22: for x be Point of E, seq be sequence of E
st rng seq c= E0 & seq is convergent
& lim seq = x
holds Lf/*seq is convergent & Pg.x = lim Lf/*seq by A16;
A23: for x,y be Point of E holds Pg.(x+y) = Pg.x + Pg.y
proof
let x,y be Point of E;
consider xseq be sequence of E such that
A24: rng xseq c= E0 & xseq is convergent
& lim xseq = x
& Lf/*xseq is convergent
& Pg.x = lim Lf/*xseq by A19;
consider yseq be sequence of E such that
A25: rng yseq c= E0 & yseq is convergent
& lim yseq = y
& Lf/*yseq is convergent
& Pg.y = lim Lf/*yseq by A19;
A29: rng (xseq + yseq) c= E0
proof
let y be object;
assume y in rng (xseq+yseq); then
consider n be Element of NAT such that
A26: y = (xseq+yseq).n by FUNCT_2:113;
xseq.n in rng xseq & yseq.n in rng yseq by FUNCT_2:4; then
reconsider xn = xseq.n, yn = yseq.n as Point of E1 by A3,A24,A25;
xseq.n + yseq.n = xn+yn by NORMSP_3:28; then
xseq.n + yseq.n in E0 by A3;
hence y in E0 by A26,NORMSP_1:def 2;
end;
A30: xseq + yseq is convergent by A24,A25,NORMSP_1:19;
A31: lim (xseq + yseq) = x+y by A24,A25,NORMSP_1:25;
A32: rng (xseq + yseq) c= dom Lf by A3,A29,FUNCT_2:def 1;
A33: rng xseq c= dom Lf by A3,A24,FUNCT_2:def 1;
A34: rng yseq c= dom Lf by A3,A25,FUNCT_2:def 1;
B34: for n be Nat holds (Lf/*(xseq+yseq)).n = (Lf/*xseq).n + (Lf/*yseq).n
proof
let n be Nat;
A35: n in NAT by ORDINAL1:def 12;
xseq.n in rng xseq & yseq.n in rng yseq
by FUNCT_2:4,ORDINAL1:def 12; then
reconsider xn = xseq.n, yn = yseq.n as Point of E1 by A3,A24,A25;
A37: xseq.n + yseq.n = xn + yn by NORMSP_3:28; then
xseq.n + yseq.n in the carrier of E1; then
A39: xseq.n + yseq.n in dom L by FUNCT_2:def 1;
thus (Lf/*(xseq+yseq)).n = Lf/.((xseq+yseq).n) by A32,A35,FUNCT_2:109
.= Lf/.(xseq.n+yseq.n) by NORMSP_1:def 2
.= L.(xn+yn) by A37,A39,PARTFUN1:def 6
.= L/.xn + L/.yn by VECTSP_1:def 20
.= (Lf/*xseq).n + Lf/.(yseq.n) by A33,A35,FUNCT_2:109
.= (Lf/*xseq).n + (Lf/*yseq).n by A34,A35,FUNCT_2:109;
end;
A41: lim Lf/*(xseq +yseq)
= lim (Lf/*xseq + Lf/*yseq) by B34,NORMSP_1:def 2
.= lim Lf/*xseq +lim Lf/*yseq by A24,A25,NORMSP_1:25;
thus Pg.(x+y) = Pg.x + Pg.y by A20,A24,A25,A29,A30,A31,A41;
end;
for x be Point of E, a be Real holds Pg.(a*x) = a* Pg.x
proof
let x be Point of E, a be Real;
consider xseq be sequence of E such that
A42: rng xseq c= E0 & xseq is convergent
& lim xseq = x
& Lf/*xseq is convergent
& Pg.x = lim Lf/*xseq by A19;
A46: rng (a*xseq) c= E0
proof
let y be object;
assume y in rng (a*xseq); then
consider n be Element of NAT such that
A43: y = (a*xseq).n by FUNCT_2:113;
xseq.n in rng xseq by FUNCT_2:4; then
reconsider xn = xseq.n as Point of E1 by A3,A42;
a*xseq.n = a*xn by NORMSP_3:28; then
a*xseq.n in E0 by A3;
hence y in E0 by A43,NORMSP_1:def 5;
end;
A47: a*xseq is convergent by A42,NORMSP_1:22;
A48: lim (a*xseq) = a*x by A42,NORMSP_1:28;
A49: rng (a*xseq) c= dom Lf by A3,A46,FUNCT_2:def 1;
A50: rng xseq c= dom Lf by A3,A42,FUNCT_2:def 1;
B50: for n be Nat holds (Lf/*(a*xseq)).n = a*(Lf/*xseq).n
proof
let n be Nat;
A51: n in NAT by ORDINAL1:def 12;
xseq.n in rng xseq by FUNCT_2:4,ORDINAL1:def 12; then
reconsider xn=xseq.n as Point of E1 by A3,A42;
A53: a*xseq.n = a*xn by NORMSP_3:28; then
a*xseq.n in the carrier of E1; then
A55: a*xseq.n in dom L by FUNCT_2:def 1;
thus (Lf/*((a*xseq))).n = Lf/.(((a*xseq)).n) by A49,A51,FUNCT_2:109
.= Lf/.(a*xseq.n) by NORMSP_1:def 5
.= L.(a*xn) by A53,A55,PARTFUN1:def 6
.= a * L/.xn by LOPBAN_1:def 5
.= a * (Lf/*xseq).n by A50,A51,FUNCT_2:109;
end;
lim Lf/*((a*xseq))
= lim (a*(Lf/*xseq)) by B50,NORMSP_1:def 5
.= a* lim Lf/*xseq by A42,NORMSP_1:28;
hence Pg.(a*x) = a * Pg.x by A20,A42,A46,A47,A48;
end; then
reconsider Pg as LinearOperator of E,F
by A23,LOPBAN_1:def 5,VECTSP_1:def 20;
reconsider Pg as Lipschitzian LinearOperator of E,F
by A18,NFCONT_2:7,LOPBAN_7:6;
reconsider g = Pg as Point of R_NormSpace_of_BoundedLinearOperators (E,F)
by LOPBAN_1:def 9;
A58: dom g = the carrier of E by FUNCT_2:def 1;
A61: ||.f.|| = upper_bound (PreNorms(modetrans(f,E1,F))) by LOPBAN_1:def 13
.= upper_bound PreNorms(L) by LOPBAN_1:29;
A63: ||.g.|| = upper_bound (PreNorms(modetrans(g,E,F))) by LOPBAN_1:def 13
.= upper_bound PreNorms(Pg) by LOPBAN_1:29;
for t be Real st t in PreNorms(L) holds t <= ||.g.||
proof
let t be Real;
assume t in PreNorms(L); then
consider w be Point of E1 such that
A64: t = ||. L.w .|| & ||.w.|| <= 1;
A65: the carrier of E1 c= the carrier of E by DUALSP01:def 16;
w in the carrier of E1; then
reconsider w1 = w as Point of E by A65;
A67: ||.w1.|| <= 1 by A64,NORMSP_3:28;
A68: not PreNorms(Pg) is empty & PreNorms(Pg) is bounded_above
by LOPBAN_1:27;
L.w = Pg.w1 by A3,A17,FUNCT_1:49; then
t in PreNorms(Pg) by A64,A67;
hence t <= ||.g.|| by A63,A68,SEQ_4:def 1;
end; then
A69: ||.f.|| <= ||.g.|| by A61,SEQ_4:45;
for t be Real st t in PreNorms(Pg) holds t <= ||.f.||
proof
let t be Real;
assume t in PreNorms(Pg); then
consider x be Point of E such that
A70: t = ||. Pg.x .|| & ||.x.|| <= 1;
consider xseq be sequence of E such that
A71: rng xseq c= E0 & xseq is convergent
& lim xseq = x
& Lf/*xseq is convergent
& Pg.x = lim Lf/*xseq by A19;
A72: ||. Pg.x .||
= lim ||.Lf/*xseq.|| by A71,LOPBAN_1:20;
A73: ||.xseq.|| is convergent
& lim ||.xseq.|| = ||. lim xseq.|| by A71,LOPBAN_1:20;
A74: ||.Lf/*xseq.|| is convergent by A71,NORMSP_1:23;
A75: ||.f.|| (#) ||.xseq.|| is convergent by A71,LOPBAN_1:20,SEQ_2:7;
for n be Nat holds
||.Lf/*xseq.|| .n <= ( ||.f.|| (#) ||.xseq.||) .n
proof
let n be Nat;
A77: n in NAT by ORDINAL1:def 12;
A78: rng xseq c= dom Lf by A3,A71,FUNCT_2:def 1;
xseq.n in rng xseq by FUNCT_2:4,ORDINAL1:def 12; then
reconsider xn = xseq.n as Point of E1 by A3,A71;
A80: dom Lf = the carrier of E1 by FUNCT_2:def 1;
A81: ||.Lf/*xseq.|| .n
= ||. (Lf/*xseq).n .|| by NORMSP_0:def 4
.= ||. Lf/.(xseq.n) .|| by A77,A78,FUNCT_2:109
.= ||. L.xn .|| by A80,PARTFUN1:def 6;
||. L.xn .|| <= ||.f.|| * ||.xn.|| by LOPBAN_1:32; then
||. L.xn .|| <= ||.f.|| * ||.xseq.n.|| by NORMSP_3:28; then
||. L.xn .|| <= ||.f.|| * ( ||.xseq.|| .n) by NORMSP_0:def 4;
hence thesis by A81,VALUED_1:6;
end; then
lim ||.Lf/*xseq.|| <= lim(||.f.|| (#) ||.xseq.||)
by A74,A75,SEQ_2:18; then
A82: lim ||.Lf/*xseq.|| <= ||.f.|| * ||.x.|| by A71,A73,SEQ_2:8;
||.f.|| * ||.x.|| <= ||.f.|| * 1 by A70,XREAL_1:64;
hence t <= ||.f.|| by A70,A72,A82,XXREAL_0:2;
end; then
||.g.|| <= ||.f.|| by A63,SEQ_4:45;
hence ex g be Point of R_NormSpace_of_BoundedLinearOperators (E,F)
st dom g = the carrier of E
& g| the carrier of E1 = f
& ||.g.|| = ||.f.||
& ex Lf be PartFunc of E,F
st Lf = f
& (for x be Point of E
holds ex seq be sequence of E
st rng seq c= the carrier of E1
& seq is convergent
& lim seq = x
& Lf/*seq is convergent
& g.x = lim Lf/*seq)
& (for x be Point of E,
seq be sequence of E
st rng seq c= the carrier of E1
& seq is convergent
& lim seq = x
holds Lf/*seq is convergent & g.x = lim Lf/*seq)
by A3,A17,A21,A22,A58,A69,XXREAL_0:1;
thus for g1,g2 be Point of R_NormSpace_of_BoundedLinearOperators (E,F)
st g1| the carrier of E1 = f
& g2| the carrier of E1 = f
holds g1 = g2
proof
let g1,g2 be Point of R_NormSpace_of_BoundedLinearOperators (E,F);
assume
A84: g1| the carrier of E1 = f
& g2| the carrier of E1 = f;
reconsider Pg1 = g1, Pg2 = g2 as Lipschitzian LinearOperator of E,F
by LOPBAN_1:def 9;
A85: Pg1 is_continuous_on the carrier of E by LMCONT1,NFCONT_2:7;
Pg2 is_continuous_on the carrier of E by LMCONT1,NFCONT_2:7;
hence thesis by A1,A3,A5,A15,A84,A85,Th020;
end;
end;
begin :: Basic Properties of Currying
theorem
for E,F,G be non empty set,
f be Function of [:E,F:],G,
x be object st x in E
holds
(curry f).x is Function of F,G
proof
let E,F,G be non empty set,
f be Function of [:E,F:],G,
x be object;
assume
A1: x in E;
dom f = [:E,F:] by FUNCT_2:def 1; then
consider g being Function such that
A4: (curry f) . x = g
& dom g = F
& rng g c= rng f
& for y being object st y in F holds
g . y = f . (x,y) by A1,FUNCT_5:29,ZFMISC_1:90;
thus (curry f) . x is Function of F,G by A4,XBOOLE_1:1,FUNCT_2:2;
end;
theorem
for E,F,G be non empty set,
f be Function of [:E,F:],G,
y be object st y in F
holds
(curry' f).y is Function of E,G
proof
let E,F,G be non empty set,
f be Function of [:E,F:],G,
y be object;
assume
A1: y in F;
dom f = [:E,F:] by FUNCT_2:def 1; then
ex g being Function st (curry' f) . y = g & dom g = E
& rng g c= rng f & for x being object st x in E holds
g . x = f . (x,y) by A1,FUNCT_5:32,ZFMISC_1:90;
hence (curry' f) . y is Function of E,G by XBOOLE_1:1,FUNCT_2:2;
end;
theorem LM4:
for E,F,G be non empty set,
f be Function of [:E,F:],G,
x,y be object
st x in E & y in F holds
( (curry f).x ).y = f.(x,y)
proof
let E,F,G be non empty set,
f be Function of [:E,F:],G,
x,y be object;
assume that
A1: x in E and
A2: y in F;
dom f = [:E,F:] by FUNCT_2:def 1; then
ex g being Function st (curry f) . x = g & dom g = F
& rng g c= rng f & for y being object st y in F holds
g . y = f . (x,y) by A1,FUNCT_5:29,ZFMISC_1:90;
hence ( (curry f).x ).y = f.(x,y) by A2;
end;
theorem LM5:
for E,F,G be non empty set,
f be Function of [:E,F:],G,
x,y be object
st x in E & y in F holds
( (curry' f).y ).x = f.(x,y)
proof
let E,F,G be non empty set,
f be Function of [:E,F:],G,
x,y be object;
assume that
A1: x in E and
A2: y in F;
dom f = [:E,F:] by FUNCT_2:def 1; then
ex g being Function st (curry' f) . y = g & dom g = E
& rng g c= rng f & for x being object st x in E holds
g . x = f . (x,y) by A2,FUNCT_5:32,ZFMISC_1:90;
hence ( (curry' f).y ).x = f.(x,y) by A1;
end;
definition ::: probably better define it for general modules
let E,F,G be RealLinearSpace;
let f be Function of [:the carrier of E,the carrier of F:],the carrier of G;
attr f is Bilinear means
( for v being Point of E st v in dom (curry f)
holds (curry f).v is additive homogeneous Function of F,G )
&
( for v being Point of F st v in dom (curry' f)
holds (curry' f).v is additive homogeneous Function of E,G );
end;
begin :: Equivalence of Some Definitions of Continuity of Bounded
:: Bilinear Operators
theorem EX1: ::: functorial registration
for E,F,G be RealLinearSpace
holds ( [:the carrier of E,the carrier of F:] ) --> 0.G is Bilinear
proof
let E,F,G be RealLinearSpace;
set f = ( [:the carrier of E,the carrier of F:] ) --> 0.G;
A2: for x being Point of E
holds (curry f).x is additive homogeneous Function of F,G
proof
let x be Point of E;
reconsider L = (curry f).x as Function of F,G;
A5: for y1,y2 be Point of F holds L.(y1+y2) = L.y1 + L.y2
proof
let y1,y2 be Point of F;
A11: L.(y1+y2) = f.(x,y1+y2) by LM4
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
A12: L.y1 = f.(x,y1) by LM4
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
L.y2 = f.(x,y2) by LM4
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
hence L.(y1+y2) = L.y1 + L.y2 by A11,A12,RLVECT_1:4;
end;
for y be Point of F, a be Real holds L.(a*y) = a * L.y
proof
let y be Point of F, a be Real;
A18: L.(a*y) = f.(x,a*y) by LM4
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
L.y = f.(x,y) by LM4
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
hence L.(a*y) = a * L.y by A18,RLVECT_1:10;
end;
hence thesis by A5,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
for x being Point of F st x in dom (curry' f)
holds (curry' f).x is additive homogeneous Function of E,G
proof
let x be Point of F;
assume x in dom (curry' f);
reconsider L = (curry' f).x as Function of E,G;
A22: for y1,y2 be Point of E holds L.(y1+y2) = L.y1+L.y2
proof
let y1,y2 be Point of E;
A28: L.(y1+y2) = f.(y1+y2,x) by LM5
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
A29: L.y1 = f.(y1,x) by LM5
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
L.y2 = f.(y2,x) by LM5
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
hence L.(y1+y2) = L.y1 + L.y2 by A28,A29,RLVECT_1:4;
end;
for y be Point of E, a be Real holds L.(a*y) = a * L.y
proof
let y be Point of E, a be Real;
A35: L.(a*y) = f.(a*y,x) by LM5
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
L.y = f.(y,x) by LM5
.= 0.G by ZFMISC_1:87,FUNCOP_1:7;
hence L.(a*y) = a * L.y by A35,RLVECT_1:10;
end;
hence thesis by A22,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence f is Bilinear by A2;
end;
registration
let E,F,G be RealLinearSpace;
cluster Bilinear for Function of
[: the carrier of E, the carrier of F:], the carrier of G;
correctness
proof
( [:the carrier of E,the carrier of F:] ) --> 0.G is Bilinear by EX1;
hence thesis;
end;
end;
theorem LM6:
for E,F,G be RealLinearSpace,
L be Function of
[:the carrier of E,the carrier of F:], the carrier of G
holds
L is Bilinear
iff
( ( for x1,x2 be Point of E,
y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) )
&
( for x be Point of E,
y be Point of F,
a be Real
holds L.(a * x, y) = a * L.(x,y) )
&
( for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) )
&
( for x be Point of E,
y be Point of F,
a be Real
holds L.(x, a*y) = a * L.(x,y) )
)
proof
let E,F,G be RealLinearSpace,
L be Function of
[:the carrier of E,the carrier of F:], the carrier of G;
A1: dom(curry L) = the carrier of E
& dom(curry' L) = the carrier of F by FUNCT_2:def 1;
hereby
assume
A2: L is Bilinear;
thus for x1,x2 be Point of E, y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y)
proof
let x1,x2 be Point of E, y be Point of F;
reconsider Ly = (curry' L).y
as additive homogeneous Function of E,G by A1,A2;
A5: Ly.x1 = L. (x1,y) by LM5;
A6: Ly.x2 = L. (x2,y) by LM5;
thus L.(x1+x2,y) = Ly.(x1+x2) by LM5
.= L.(x1,y) + L.(x2,y) by A5,A6,VECTSP_1:def 20;
end;
thus for x be Point of E,
y be Point of F,
a be Real
holds L.(a*x, y) = a * L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
reconsider Ly = (curry' L).y
as additive homogeneous Function of E,G by A1,A2;
thus L.(a*x, y) = Ly.(a*x) by LM5
.= a * Ly.x by LOPBAN_1:def 5
.= a * L.(x,y) by LM5;
end;
thus for x be Point of E, y1,y2 be Point of F
holds L.(x, y1+y2) = L.(x,y1) + L.(x,y2)
proof
let x be Point of E, y1,y2 be Point of F;
reconsider Lx = (curry L).x
as additive homogeneous Function of F,G by A1,A2;
A8: Lx.y1 = L.(x,y1) by LM4;
A9: Lx.y2 = L.(x,y2) by LM4;
thus L.(x,y1+y2) = Lx.(y1+y2) by LM4
.= L. (x,y1) + L. (x,y2) by A8,A9,VECTSP_1:def 20;
end;
thus for x be Point of E,
y be Point of F,
a be Real
holds L.(x, a*y) = a * L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
reconsider Lx = (curry L).x
as additive homogeneous Function of F,G by A1,A2;
A10: Lx.y = L.(x,y) by LM4;
thus L.(x, a*y) = Lx.(a*y) by LM4
.= a * L.(x,y) by A10,LOPBAN_1:def 5;
end;
end;
assume that
A11: for x1,x2 be Point of E, y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) and
A12: for x be Point of E,
y be Point of F,
a be Real holds L.(a*x, y) = a * L.(x,y) and
A13: for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) and
A14: for x be Point of E,
y be Point of F,
a be Real holds L.(x, a*y) = a * L.(x,y);
A15: for x being Point of E st x in dom (curry L)
holds (curry L).x is additive homogeneous Function of F,G
proof
let x be Point of E;
assume x in dom (curry L);
reconsider Lx = (curry L).x as Function of F,G;
A16: for y1,y2 be Point of F holds Lx.(y1+y2) = Lx.y1+Lx.y2
proof
let y1,y2 be Point of F;
A17: L.(x,y1) = Lx.y1 by LM4;
thus Lx.(y1+y2) = L.(x,y1+y2) by LM4
.= L.(x,y1) + L.(x,y2) by A13
.= Lx.y1 + Lx.y2 by A17,LM4;
end;
for y be Point of F, a be Real holds Lx.(a*y) = a * Lx.y
proof
let y be Point of F, a be Real;
thus Lx.(a*y) = L. (x, a*y) by LM4
.= a * L.(x,y) by A14
.= a * Lx.y by LM4;
end;
hence thesis by A16,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
for y being Point of F st y in dom (curry' L)
holds (curry' L).y is additive homogeneous Function of E,G
proof
let y be Point of F;
assume y in dom (curry' L);
reconsider Ly = (curry' L).y as Function of E,G;
A22: for x1,x2 be Point of E holds Ly.(x1+x2) = Ly.x1 + Ly.x2
proof
let x1,x2 be Point of E;
A23: L.(x1,y) = Ly.x1 by LM5;
thus Ly.(x1+x2) = L.(x1+x2,y) by LM5
.= L.(x1,y) + L.(x2,y) by A11
.= Ly.x1+Ly.x2 by A23,LM5;
end;
for x be Point of E,a be Real holds Ly.(a*x) = a * Ly.x
proof
let x be Point of E, a be Real;
thus Ly.(a*x) = L.(a*x,y) by LM5
.= a * L.(x,y) by A12
.= a * Ly.x by LM5;
end;
hence thesis by A22,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence L is Bilinear by A15;
end;
definition
let E,F,G be RealLinearSpace;
let f be Function of [:E,F:],G;
attr f is Bilinear means
ex g be Function of [:the carrier of E,the carrier of F:], the carrier of G
st f = g & g is Bilinear;
end;
registration
let E,F,G be RealLinearSpace;
cluster Bilinear for Function of [:E,F:],G;
correctness
proof
set g = ( [:the carrier of E,the carrier of F:] ) --> 0.G;
reconsider f = g as Function of [:E,F:],G;
take f;
thus thesis by EX1;
end;
end;
definition
let E,F,G be RealLinearSpace;
let f be Function of [:E,F:],G;
let x be Point of E;
let y be Point of F;
redefine func f.(x,y) -> Point of G; :: redefines . (BINOP_1, definition)
correctness
proof
f.[x,y] is Point of G;
hence thesis;
end;
end;
theorem
for E,F,G be RealLinearSpace,
L be Function of [:E,F:],G holds
L is Bilinear
iff
( ( for x1,x2 be Point of E, y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) )
&
( for x be Point of E,
y be Point of F,
a be Real
holds L.(a*x,y) = a * L.(x,y) )
&
( for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) )
&
( for x be Point of E,
y be Point of F,
a be Real
holds L. (x, a*y) = a * L.(x,y) ) ) by LM6;
definition
let E,F,G be RealLinearSpace;
mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G;
end;
definition
let E,F,G be RealNormSpace;
let f be Function of [:E,F:],G;
attr f is Bilinear means
ex g be Function of
[:the carrier of E, the carrier of F:], the carrier of G
st f = g & g is Bilinear;
end;
registration
let E,F,G be RealNormSpace;
cluster Bilinear for Function of [:E,F:],G;
correctness
proof
set g = ( [:the carrier of E,the carrier of F:] ) --> 0.G;
reconsider f = g as Function of [:E,F:],G;
take f;
thus thesis by EX1;
end;
end;
definition
let E,F,G be RealNormSpace;
mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G;
end;
reserve E,F,G for RealNormSpace;
reserve L for BilinearOperator of E,F,G;
reserve x for Element of E;
reserve y for Element of F;
definition
let E,F,G be RealNormSpace;
let f be Function of [:E,F:], G;
let x be Point of E;
let y be Point of F;
redefine func f.(x,y) -> Point of G; :: redefines . (BINOP_1, definition)
correctness
proof
f.[x,y] is Point of G;
hence thesis;
end;
end;
theorem LM8:
for E,F,G be RealNormSpace,
L be Function of [:E,F:],G
holds
L is Bilinear
iff
( ( for x1,x2 be Point of E, y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) )
&
( for x be Point of E,
y be Point of F,
a be Real
holds L.(a*x, y) = a * L.(x,y) )
&
( for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) )
&
( for x be Point of E,
y be Point of F,
a be Real
holds L.(x,a*y) = a * L.(x,y) ) ) by LM6;
theorem
for E,F,G be RealNormSpace,
f be BilinearOperator of E,F,G
holds
( f is_continuous_on the carrier of [:E,F:]
iff
f is_continuous_in 0.( [:E,F:] ) )
&
( f is_continuous_on the carrier of [:E,F:]
iff
ex K be Real
st 0 <= K
& for x be Point of E,y be Point of F
holds ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.|| )
proof
let E,F,G be RealNormSpace,
f be BilinearOperator of E,F,G;
A1: dom f = the carrier of [:E,F:] by FUNCT_2:def 1;
A2: f. 0. [:E,F:] = f.(0.E,0.F) by PRVECT_3:18
.= f.(0* 0.E,0.F) by RLVECT_1:10
.= 0 * f.(0.E,0.F) by LM8
.= 0.G by RLVECT_1:10;
A4: f is_continuous_in 0.( [:E,F:] ) implies
ex K be Real
st 0 <= K
& for x be Point of E,y be Point of F
holds ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.||
proof
assume f is_continuous_in 0. [:E,F:]; then
consider s be Real such that
A5: 0 < s
& for z be Point of [:E,F:]
st z in dom f
& ||. z - 0. [:E,F:] .|| < s
holds ||. f/.z- f/. 0. [:E,F:] .|| < 1 by NFCONT_1:7;
consider s1 be Real such that
A7: 0 < s1 & s1 < s
& [:Ball(0.E,s1),Ball(0.F,s1):]
c= Ball(0. [:E,F:],s) by A5,NDIFF_8:22,PRVECT_3:18;
set s2 = s1/2;
A8: 0 < s2 & s2 < s1 by A7,XREAL_1:215,216;
A9: now
let x be Point of E, y be Point of F;
assume ||.x.|| <= s2 & ||.y.|| <= s2; then
A10: ||.x.|| < s1 & ||.y.|| < s1 by A8,XXREAL_0:2;
reconsider z = [x,y] as Point of [:E,F:];
||.x - 0.E .|| < s1 by A10,RLVECT_1:13; then
||.0.E -x .|| < s1 by NORMSP_1:7; then
A12: x in Ball(0.E,s1);
||.y - 0.F .|| < s1 by A10,RLVECT_1:13; then
||.0.F -y .|| < s1 by NORMSP_1:7; then
y in Ball(0.F,s1); then
z in [:Ball(0.E,s1),Ball(0.F,s1):] by A12,ZFMISC_1:87; then
z in Ball(0. [:E,F:],s) by A7; then
ex z1 be Point of [:E,F:]
st z = z1 & ||. 0. [:E,F:] - z1 .|| < s; then
||.z - 0. [:E,F:] .|| < s by NORMSP_1:7; then
||. f/.z - f/. 0. [:E,F:] .|| < 1 by A5,A1;
hence ||. f.(x,y) .||< 1 by A2,RLVECT_1:13;
end;
A14: 0 < s2*s2 by A8,XREAL_1:129;
take K = 1/(s2*s2);
thus 0 <= K by A7;
let x be Point of E,y be Point of F;
A15: f.(0.E,y) = f.(0 * 0.E,y) by RLVECT_1:10
.= 0 * f.(0.E,y) by LM8
.= 0.G by RLVECT_1:10;
A16: f.(x,0.F) = f.(x,0 * 0.F) by RLVECT_1:10
.= 0 * f.(x,0.F) by LM8
.= 0.G by RLVECT_1:10;
thus ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.||
proof
per cases;
suppose
C16: x <> 0.E & y <> 0.F; then
||.x.|| <> 0 & ||.y.|| <> 0 by NORMSP_0:def 5; then
A17: 0 < ||.x.|| & 0 < ||.y.||;
set x1 = (s2/||.x.||) * x;
set y1 = (s2/||.y.||) * y;
A19: ||.x1.|| = |. s2 / ||.x.|| .| * ||.x.|| by NORMSP_1:def 1
.= (s2 / ||.x.||) * ||.x.|| by A7,COMPLEX1:43
.= s2 by C16,NORMSP_0:def 5,XCMPLX_1:87;
A21: ||.y1.||
= |. s2 / ||.y.|| .| * ||.y.|| by NORMSP_1:def 1
.= (s2/||.y.||)*||.y.|| by A7,COMPLEX1:43
.= s2 by C16,NORMSP_0:def 5,XCMPLX_1:87;
A23: f. (x1,y1)
= (s2 / ||.x.||) * f.(x, (s2 / ||.y.||) * y) by LM8;
f.(x, (s2 / ||.y.||) * y)
= (s2/||.y.||) * f.(x,y) by LM8; then
A24: f.(x1,y1)
= ((s2 / ||.x.||) * (s2 / ||.y.||) ) * ( f.(x,y) )
by A23,RLVECT_1:def 7
.= (s2 * s2) / (||.x.|| * ||.y.||) * f.(x,y) by XCMPLX_1:76;
A25: 0 < ||.x.|| * ||.y.|| by A17,XREAL_1:129;
||.f. (x1,y1) .||
= |. (s2 * s2) / ( ||.x.|| * ||.y.||) .| * ||. f. (x,y) .||
by A24,NORMSP_1:def 1
.= (s2 * s2)/ (||.x.|| * ||.y.||) * ||. f.(x,y) .||
by A7,COMPLEX1:43; then
A28: (s2 * s2) / (||.x.|| * ||.y.||) * ||. f.(x,y) .|| < 1
by A9,A19,A21;
(s2 * s2) / (||.x.|| * ||.y.||) * ||. f.(x,y) .|| * (||.x.||*||.y.||)
<= 1 * (||.x.|| * ||.y.||) by A28,XREAL_1:64; then
(s2 * s2) / (||.x.||*||.y.||) * (||.x.||*||.y.||) * ||. f.(x,y) .||
<= ||.x.||*||.y.||; then
(s2 * s2) * ||. f.(x,y) .|| <= ||.x.|| * ||.y.|| by A25,XCMPLX_1:87;
then
(s2 * s2) * ||. f.(x,y) .|| / (s2 * s2)
<= ||.x.|| * ||.y.|| / (s2 * s2) by A7,XREAL_1:72; then
||. f.(x,y) .|| <= (||.x.|| * ||.y.||) / (s2 * s2)
by A14,XCMPLX_1:89; then
||. f.(x,y) .|| <= 1 / (s2 * s2) * (||.x.|| * ||.y.||)
by XCMPLX_1:99;
hence ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.||;
end;
suppose
A29: x = 0.E or y = 0.F; then
||.x.|| = 0 or ||.y.|| = 0;
hence ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.|| by A15,A16,A29;
end;
end;
end;
( ex K be Real
st 0 <= K
& for x be Point of E,y be Point of F holds
||.f. (x,y) .|| <= K * ||.x.|| * ||.y.|| )
implies f is_continuous_on the carrier of [:E,F:]
proof
given K be Real such that
A32: 0 <= K
& for x be Point of E,y be Point of F holds
||. f.(x,y) .|| <= K * ||.x.|| * ||.y.||;
A33: the carrier of [:E,F:] c= dom f by FUNCT_2:def 1;
for z0 be Point of [:E,F:], r1 be Real
st z0 in the carrier of [:E,F:] & 0 < r1
ex s be Real
st 0 < s
& for z1 be Point of [:E,F:]
st z1 in the carrier of [:E,F:]
& ||. z1 - z0 .|| < s
holds ||. f/.z1 - f/.z0 .|| < r1
proof
let z0 be Point of [:E,F:],r1 be Real;
assume
A34: z0 in the carrier of [:E,F:] & 0 < r1;
set r = r1/2;
A35: 0 < r & r < r1 by A34,XREAL_1:215,216;
consider x0 be Point of E,y0 be Point of F such that
A36: z0 = [x0,y0] by PRVECT_3:18;
set KXY0 = ( K + 1 ) * (||.x0.|| + 1 + ||.y0.||);
set s1 = r / KXY0;
K + 0 < K + 1 by XREAL_1:8; then
A39: K * (||.x0.|| + 1 + ||.y0.||)
< (K+1) * (||.x0.|| + 1 + ||.y0.||) by XREAL_1:68;
A40: 0 < KXY0 by A32,XREAL_1:129; then
A41: 0 < s1 by A35,XREAL_1:139;
set s = min(s1,1);
A42: s <= 1 & s <= s1 by XXREAL_0:17;
A43: 0 < s by A41,XXREAL_0:21; then
A44: ( K * (||.x0.|| + 1 + ||.y0.||)) * s
<= KXY0 * s1 by A32,A39,A42,XREAL_1:66;
take s;
thus 0 < s by A41,XXREAL_0:21;
let z1 be Point of [:E,F:];
assume
A45: z1 in the carrier of [:E,F:] & ||. z1 - z0 .|| < s;
consider x1 be Point of E,y1 be Point of F such that
A46: z1 = [x1,y1] by PRVECT_3:18;
A47: f.z1 - f.z0
= f.(x1,y1) - f.(x0,y1) + f.(x0,y1) - f.(x0,y0) by A36,A46,RLVECT_4:1
.= (f.(x1,y1) - f.(x0,y1)) + (f.(x0,y1) -f.(x0,y0)) by RLVECT_1:28;
A49: f.(x1,y1) - f.(x0,y1)
= f.(x1,y1) +(-1)* f.(x0,y1) by RLVECT_1:16
.= f.(x1,y1) + f.((-1)*x0,y1) by LM8
.= f.(x1+(-1)*x0,y1) by LM8
.= f.(x1-x0,y1) by RLVECT_1:16;
A51: f.(x0,y1) - f.(x0,y0)
= f.(x0,y1) +(-1)* f.(x0,y0) by RLVECT_1:16
.= f.(x0,y1) + f.(x0,(-1)*y0) by LM8
.= f.(x0, y1+(-1)*y0) by LM8
.= f.(x0,y1-y0) by RLVECT_1:16;
A52: ||. f.(x1-x0,y1) .|| <= K * ||.x1-x0.|| * ||.y1.|| by A32;
A53: ||. f.(x0,y1-y0) .|| <= K * ||.x0.|| * ||.y1-y0.|| by A32;
-z0 = [-x0,-y0] by A36,PRVECT_3:18; then
A54: z1 - z0 = [x1-x0,y1-y0] by A46,PRVECT_3:18; then
||.x1-x0.|| <= ||.z1- z0.|| by NDIFF_8:21; then
A55: ||.x1-x0.|| < s by A45,XXREAL_0:2;
||.y1-y0.|| <= ||.z1- z0.|| by A54,NDIFF_8:21; then
A56: ||.y1-y0.|| < s by A45,XXREAL_0:2;
||.x1-x0.|| * ||.y1.|| <= s * ||.y1.|| by A55,XREAL_1:64; then
K * (||.x1-x0.|| * ||.y1.||) <= K * ( s * ||.y1.||) by A32,XREAL_1:64;
then
A57: ||.f.(x1-x0,y1) .|| <= K * s * ||.y1.|| by A52,XXREAL_0:2;
||.y1-y0.|| * ||.x0.|| <= s * ||.x0.|| by A56,XREAL_1:64; then
K * ( ||.x0.|| * ||.y1-y0.|| ) <= K * ( s *||.x0.|| )
by A32,XREAL_1:64; then
||.f.(x0,y1-y0) .|| <= K * s * ||.x0.|| by A53,XXREAL_0:2; then
A58: ||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .||
<= K * s * ||.y1.|| + K * s * ||.x0.|| by A57,XREAL_1:7;
||.y1.|| = ||. y1 - y0 + y0 .|| by RLVECT_4:1; then
A60: ||.y1.|| <= ||.y1-y0.|| + ||.y0.|| by NORMSP_1:def 1;
||. y1-y0 .|| + ||.y0.|| <= s + ||.y0.|| by A56,XREAL_1:7; then
A61: ||.y1.|| <= s + ||.y0.|| by A60,XXREAL_0:2;
s + ||.y0.|| <= 1 + ||.y0.|| by A42,XREAL_1:7; then
||.y1.|| <= 1 + ||.y0.|| by A61,XXREAL_0:2; then
||.y1.|| + ||.x0.|| <= 1 + ||.y0.|| + ||.x0.|| by XREAL_1:7; then
s * (||.y1.|| + ||.x0.||) <= s * (1 + ||.y0.|| + ||.x0.||)
by A43,XREAL_1:64; then
s * (||.y1.|| + ||.x0.||) * K <= s * (1 + ||.y0.|| + ||.x0.||) * K
by A32,XREAL_1:64; then
||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .||
<= K * s * (||.x0.|| + 1+ ||.y0.||) by A58,XXREAL_0:2; then
||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .|| <= KXY0 * (r/KXY0)
by A44,XXREAL_0:2; then
A64: ||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .|| <= r
by A40,XCMPLX_1:87;
||.f.z1 - f.z0 .||
<= ||. f.(x1,y1) -f.(x0,y1) .|| + ||. f.(x0,y1) - f.(x0,y0) .||
by A47,NORMSP_1:def 1; then
||. f/.z1 - f/.z0 .|| <= r by A49,A51,A64,XXREAL_0:2;
hence ||. f/.z1 - f/.z0 .|| < r1 by A35,XXREAL_0:2;
end;
hence thesis by A33,NFCONT_1:19;
end;
hence thesis by A4;
end;