let X be RealBanachSpace; for Y being RealNormSpace
for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
let Y be RealNormSpace; for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
let T be Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ( ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) implies ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) ) )
assume A1:
for x being Point of X ex KTx being Real st
( 0 <= KTx & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= KTx ) )
; ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
per cases
( T <> {} or T = {} )
;
suppose A2:
T <> {}
;
ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )deffunc H1(
Point of
X,
Real)
-> Subset of
X =
Ball ($1,$2);
defpred S1[
Point of
X,
set ]
means $2
= { ||.(f . $1).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ;
A3:
for
x being
Point of
X ex
y being
Element of
bool REAL st
S1[
x,
y]
ex
Ta being
Function of the
carrier of
X,
(bool REAL) st
for
x being
Element of
X holds
S1[
x,
Ta . x]
from FUNCT_2:sch 3(A3);
then consider Ta being
Function of
X,
(bool REAL) such that A4:
for
x being
Point of
X holds
Ta . x = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T }
;
defpred S2[
Nat,
set ]
means $2
= { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= $1 ) } ;
A5:
for
n being
Element of
NAT ex
y being
Element of
bool the
carrier of
X st
S2[
n,
y]
ex
Xn being
sequence of
(bool the carrier of X) st
for
n being
Element of
NAT holds
S2[
n,
Xn . n]
from FUNCT_2:sch 3(A5);
then consider Xn being
sequence of
(bool the carrier of X) such that A6:
for
n being
Element of
NAT holds
Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) }
;
reconsider Xn =
Xn as
SetSequence of
X ;
A7:
the
carrier of
X c= union (rng Xn)
A15:
for
x being
Point of
X holds not
Ta . x is
empty
A17:
for
n being
Nat holds
Xn . n is
closed
proof
let n be
Nat;
Xn . n is closed
A18:
n in NAT
by ORDINAL1:def 12;
for
s1 being
sequence of
X st
rng s1 c= Xn . n &
s1 is
convergent holds
lim s1 in Xn . n
proof
let s1 be
sequence of
X;
( rng s1 c= Xn . n & s1 is convergent implies lim s1 in Xn . n )
assume that A19:
rng s1 c= Xn . n
and A20:
s1 is
convergent
;
lim s1 in Xn . n
A21:
Ta . (lim s1) = { ||.(f . (lim s1)).|| where f is Lipschitzian LinearOperator of X,Y : f in T }
by A4;
A22:
for
y being
Real st
y in Ta . (lim s1) holds
y <= n
proof
let y be
Real;
( y in Ta . (lim s1) implies y <= n )
assume
y in Ta . (lim s1)
;
y <= n
then consider f being
Lipschitzian LinearOperator of
X,
Y such that A23:
y = ||.(f . (lim s1)).||
and A24:
f in T
by A21;
A25:
f is_continuous_in lim s1
by Th4;
A26:
dom f = the
carrier of
X
by FUNCT_2:def 1;
then A27:
rng s1 c= dom f
by A19, XBOOLE_1:1;
then A28:
f /* s1 is
convergent
by A20, A25, NFCONT_1:def 5;
for
k being
Nat holds
||.(f /* s1).|| . k <= n
proof
let k be
Nat;
||.(f /* s1).|| . k <= n
A29:
k in NAT
by ORDINAL1:def 12;
||.(f /* s1).|| . k = ||.((f /* s1) . k).||
by NORMSP_0:def 4;
then A30:
||.(f /* s1).|| . k = ||.(f /. (s1 . k)).||
by A19, A26, FUNCT_2:109, A29, XBOOLE_1:1;
dom s1 = NAT
by FUNCT_2:def 1;
then
s1 . k in rng s1
by FUNCT_1:3, A29;
then
s1 . k in Xn . n
by A19;
then
s1 . k in { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) }
by A6, A18;
then consider x being
Point of
X such that A31:
x = s1 . k
and A32:
Ta . x is
bounded_above
and A33:
upper_bound (Ta . x) <= n
;
Ta . x = { ||.(g . x).|| where g is Lipschitzian LinearOperator of X,Y : g in T }
by A4;
then
||.(f . (s1 . k)).|| in Ta . (s1 . k)
by A24, A31;
then
||.(f . (s1 . k)).|| <= upper_bound (Ta . (s1 . k))
by A31, A32, SEQ_4:def 1;
hence
||.(f /* s1).|| . k <= n
by A30, A31, A33, XXREAL_0:2;
verum
end;
then A34:
for
i being
Nat st
0 <= i holds
||.(f /* s1).|| . i <= n
;
f /. (lim s1) = lim (f /* s1)
by A20, A25, A27, NFCONT_1:def 5;
then
lim ||.(f /* s1).|| = ||.(f /. (lim s1)).||
by A28, LOPBAN_1:20;
hence
y <= n
by A23, A28, A34, NORMSP_1:23, RSSPACE2:5;
verum
end;
then
for
y being
ExtReal st
y in Ta . (lim s1) holds
y <= n
;
then A35:
n is
UpperBound of
Ta . (lim s1)
by XXREAL_2:def 1;
not
Ta . (lim s1) is
empty
by A15;
then A36:
upper_bound (Ta . (lim s1)) <= n
by A22, SEQ_4:45;
A37:
Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) }
by A6, A18;
Ta . (lim s1) is
bounded_above
by A35;
hence
lim s1 in Xn . n
by A36, A37;
verum
end;
hence
Xn . n is
closed
by NFCONT_1:def 3;
verum
end; consider f being
object such that A38:
f in T
by A2, XBOOLE_0:def 1;
reconsider f =
f as
Lipschitzian LinearOperator of
X,
Y by A38, LOPBAN_1:def 9;
union (rng Xn) is
Subset of
X
by PROB_1:11;
then
union (rng Xn) = the
carrier of
X
by A7, XBOOLE_0:def 10;
then consider n0 being
Nat,
r being
Real,
x0 being
Point of
X such that A39:
0 < r
and A40:
H1(
x0,
r)
c= Xn . n0
by A17, Th3;
A41:
n0 in NAT
by ORDINAL1:def 12;
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:5;
then
x0 in H1(
x0,
r)
by A39;
then
x0 in Xn . n0
by A40;
then
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) }
by A6, A41;
then consider xx1 being
Point of
X such that A42:
xx1 = x0
and A43:
Ta . xx1 is
bounded_above
and
upper_bound (Ta . xx1) <= n0
;
Ta . xx1 = { ||.(g . xx1).|| where g is Lipschitzian LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A42, A38;
then
||.(f . x0).|| <= upper_bound (Ta . x0)
by A42, A43, SEQ_4:def 1;
then A44:
0 <= upper_bound (Ta . x0)
;
A45:
for
x being
Point of
X st
x <> 0. X holds
((r / (2 * ||.x.||)) * x) + x0 in H1(
x0,
r)
set M =
upper_bound (Ta . x0);
take KT =
(2 * ((upper_bound (Ta . x0)) + n0)) / r;
( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT ) )A51:
for
f being
Lipschitzian LinearOperator of
X,
Y st
f in T holds
for
x being
Point of
X st
x in H1(
x0,
r) holds
||.(f . x).|| <= n0
proof
let f be
Lipschitzian LinearOperator of
X,
Y;
( f in T implies for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0 )
assume A52:
f in T
;
for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0
A53:
n0 in NAT
by ORDINAL1:def 12;
let x be
Point of
X;
( x in H1(x0,r) implies ||.(f . x).|| <= n0 )
assume
x in H1(
x0,
r)
;
||.(f . x).|| <= n0
then
x in Xn . n0
by A40;
then
x in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) }
by A6, A53;
then consider x1 being
Point of
X such that A54:
x1 = x
and A55:
Ta . x1 is
bounded_above
and A56:
upper_bound (Ta . x1) <= n0
;
Ta . x1 = { ||.(g . x1).|| where g is Lipschitzian LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x).|| in Ta . x
by A52, A54;
then
||.(f . x).|| <= upper_bound (Ta . x)
by A54, A55, SEQ_4:def 1;
hence
||.(f . x).|| <= n0
by A54, A56, XXREAL_0:2;
verum
end; A57:
now for f being Lipschitzian LinearOperator of X,Y st f in T holds
for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KTlet f be
Lipschitzian LinearOperator of
X,
Y;
( f in T implies for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT )assume A58:
f in T
;
for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KTA59:
for
x being
Point of
X st
x <> 0. X holds
||.(f . x).|| <= KT * ||.x.||
proof
A60:
n0 in NAT
by ORDINAL1:def 12;
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:5;
then
x0 in H1(
x0,
r)
by A39;
then
x0 in Xn . n0
by A40;
then A61:
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) }
by A6, A60;
set nr3 =
||.(f . x0).||;
let x be
Point of
X;
( x <> 0. X implies ||.(f . x).|| <= KT * ||.x.|| )
set nrp1 =
r / (2 * ||.x.||);
set nrp2 =
(2 * ||.x.||) / r;
set nr1 =
||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).||;
set nr2 =
||.(f . ((r / (2 * ||.x.||)) * x)).||;
||.(- (f . x0)).|| = ||.(f . x0).||
by NORMSP_1:2;
then A62:
||.(f . ((r / (2 * ||.x.||)) * x)).|| - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) - (- (f . x0))).||
by NORMSP_1:8;
assume A63:
x <> 0. X
;
||.(f . x).|| <= KT * ||.x.||
then A64:
||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0
by A51, A45, A58;
consider x1 being
Point of
X such that A65:
x1 = x0
and A66:
Ta . x1 is
bounded_above
and
upper_bound (Ta . x1) <= n0
by A61;
Ta . x1 = { ||.(g . x1).|| where g is Lipschitzian LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A58, A65;
then
||.(f . x0).|| <= upper_bound (Ta . x0)
by A65, A66, SEQ_4:def 1;
then A67:
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).||
by XREAL_1:10;
||.x.|| <> 0
by A63, NORMSP_0:def 5;
then A68:
||.x.|| > 0
;
||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).||
by LOPBAN_1:def 5;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = |.(r / (2 * ||.x.||)).| * ||.(f . x).||
by NORMSP_1:def 1;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (r / (2 * ||.x.||)) * ||.(f . x).||
by A39, ABSVALUE:def 1;
then
(
||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| = ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| &
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| )
by A62, RLVECT_1:17, VECTSP_1:def 20;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= n0
by A64, XXREAL_0:2;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= n0
by A67, XXREAL_0:2;
then
(((r / (2 * ||.x.||)) * ||.(f . x).||) + (- (upper_bound (Ta . x0)))) + (upper_bound (Ta . x0)) <= n0 + (upper_bound (Ta . x0))
by XREAL_1:6;
then
((2 * ||.x.||) / r) * ((r / (2 * ||.x.||)) * ||.(f . x).||) <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A39, XREAL_1:64;
then A69:
((r / (2 * ||.x.||)) * ((2 * ||.x.||) / r)) * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
;
2
* ||.x.|| > 0
by A68, XREAL_1:129;
then
1
* ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A39, A69, XCMPLX_1:112;
hence
||.(f . x).|| <= KT * ||.x.||
;
verum
end; A70:
for
x being
Point of
X holds
||.(f . x).|| <= KT * ||.x.||
thus
for
k being
Real st
k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT
verum end;
for
f being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
f in T holds
||.f.|| <= KT
hence
(
0 <= KT & ( for
f being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
f in T holds
||.f.|| <= KT ) )
by A39, A44;
verum end;