let X be RealBanachSpace; :: thesis: 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 number 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 number 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; :: thesis: for T being Subset of (R_NormSpace_of_BoundedLinearOperators X,Y) st ( for x being Point of X ex K being real number 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 number 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); :: thesis: ( ( for x being Point of X ex K being real number 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 number 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 number st
( 0 <= KTx & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.(f . x).|| <= KTx ) )
; :: thesis: ex L being real number 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 <> {}
;
:: thesis: ex L being real number 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 bounded 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 the
carrier 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 bounded LinearOperator of X,Y : f in T }
;
A5:
for
x being
Point of
X holds not
Ta . x is
empty
defpred S2[
Element of
NAT ,
set ]
means $2
= { x where x is Point of X : ( Ta . x is bounded_above & sup (Ta . x) <= $1 ) } ;
A8:
for
n being
Element of
NAT ex
y being
Element of
bool the
carrier of
X st
S2[
n,
y]
ex
Xn being
Function of
NAT ,
(bool the carrier of X) st
for
n being
Element of
NAT holds
S2[
n,
Xn . n]
from FUNCT_2:sch 3(A8);
then consider Xn being
Function of
NAT ,
(bool the carrier of X) such that A9:
for
n being
Element of
NAT holds
Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & sup (Ta . x) <= n ) }
;
reconsider Xn =
Xn as
SetSequence of
X ;
A10:
for
n being
Element of
NAT holds
Xn . n is
closed
A24:
union (rng Xn) is
Subset of
X
by PROB_1:23;
the
carrier of
X c= union (rng Xn)
then
union (rng Xn) = the
carrier of
X
by A24, XBOOLE_0:def 10;
then consider n0 being
Element of
NAT ,
r being
Real,
x0 being
Point of
X such that A32:
(
0 < r &
H1(
x0,
r)
c= Xn . n0 )
by A10, Th3;
A33:
for
f being
bounded 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
A36:
for
x being
Point of
X st
x <> 0. X holds
((r / (2 * ||.x.||)) * x) + x0 in H1(
x0,
r)
proof
let x be
Point of
X;
:: thesis: ( x <> 0. X implies ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) )
assume
x <> 0. X
;
:: thesis: ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r)
then A37:
||.x.|| <> 0
by NORMSP_1:def 2;
A38:
||.x.|| >= 0
by NORMSP_1:8;
A39:
abs (||.x.|| " ) = ||.x.|| "
by A38, ABSVALUE:def 1;
A40:
0 < r / 2
by A32, XREAL_1:217;
reconsider x1 =
(||.x.|| " ) * x as
Point of
X ;
||.x1.|| = (abs (||.x.|| " )) * ||.x.||
by NORMSP_1:def 2;
then A41:
||.x1.|| = 1
by A37, A39, XCMPLX_0:def 7;
||.((r / 2) * x1).|| = (abs (r / 2)) * ||.x1.||
by NORMSP_1:def 2;
then A42:
||.((r / 2) * x1).|| = r / 2
by A40, A41, ABSVALUE:def 1;
A43:
r / 2
< r
by A32, XREAL_1:218;
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (x0 + (- x0))).||
by RLVECT_1:def 6;
then
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (0. X)).||
by RLVECT_1:16;
then
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / (2 * ||.x.||)) * x).||
by RLVECT_1:def 7;
then
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / 2) / ||.x.||) * x).||
by XCMPLX_1:79;
then
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / 2) * x1).||
by RLVECT_1:def 9;
then
||.(x0 - (((r / (2 * ||.x.||)) * x) + x0)).|| = r / 2
by A42, NORMSP_1:11;
hence
((r / (2 * ||.x.||)) * x) + x0 in H1(
x0,
r)
by A43;
:: thesis: verum
end; set M =
upper_bound (Ta . x0);
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:16;
then
x0 in H1(
x0,
r)
by A32;
then
x0 in Xn . n0
by A32;
then
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & sup (Ta . x1) <= n0 ) }
by A9;
then consider xx1 being
Point of
X such that A44:
(
xx1 = x0 &
Ta . xx1 is
bounded_above &
sup (Ta . xx1) <= n0 )
;
consider f being
set such that A45:
f in T
by A2, XBOOLE_0:def 1;
reconsider f =
f as
bounded LinearOperator of
X,
Y by A45, LOPBAN_1:def 10;
take KT =
(2 * ((upper_bound (Ta . x0)) + n0)) / r;
:: thesis: ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= KT ) )
Ta . xx1 = { ||.(g . xx1).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A44, A45;
then
||.(f . x0).|| <= sup (Ta . x0)
by A44, SEQ_4:def 4;
then
0 <= sup (Ta . x0)
by NORMSP_1:8;
then A46:
2
* ((upper_bound (Ta . x0)) + n0) >= 0
;
then A47:
0 <= KT
by A32;
A48:
now let f be
bounded LinearOperator of
X,
Y;
:: thesis: ( f in T implies for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT )assume A49:
f in T
;
:: thesis: for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KTA50:
for
x being
Point of
X st
x <> 0. X holds
||.(f . x).|| <= KT * ||.x.||
proof
let x be
Point of
X;
:: thesis: ( x <> 0. X implies ||.(f . x).|| <= KT * ||.x.|| )
assume A51:
x <> 0. X
;
:: thesis: ||.(f . x).|| <= KT * ||.x.||
then
||.x.|| <> 0
by NORMSP_1:def 2;
then
||.x.|| > 0
by NORMSP_1:8;
then A52:
2
* ||.x.|| > 0
by XREAL_1:131;
A54:
||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0
by A33, A36, A49, A51;
set nrp1 =
r / (2 * ||.x.||);
set nrp2 =
(2 * ||.x.||) / r;
||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).||
by LOPBAN_1:def 6;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (abs (r / (2 * ||.x.||))) * ||.(f . x).||
by NORMSP_1:def 2;
then A56:
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (r / (2 * ||.x.||)) * ||.(f . x).||
by A52, A32, ABSVALUE:def 1;
A57:
||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| = ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).||
by LOPBAN_1:def 5;
set nr1 =
||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).||;
set nr2 =
||.(f . ((r / (2 * ||.x.||)) * x)).||;
set nr3 =
||.(f . x0).||;
||.(- (f . x0)).|| = ||.(f . x0).||
by NORMSP_1:6;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) - (- (f . x0))).||
by NORMSP_1:12;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).||
by A56, RLVECT_1:30;
then A58:
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= n0
by A54, A57, XXREAL_0:2;
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:16;
then
x0 in H1(
x0,
r)
by A32;
then
x0 in Xn . n0
by A32;
then
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & sup (Ta . x1) <= n0 ) }
by A9;
then consider x1 being
Point of
X such that A59:
(
x1 = x0 &
Ta . x1 is
bounded_above &
sup (Ta . x1) <= n0 )
;
Ta . x1 = { ||.(g . x1).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A49, A59;
then
||.(f . x0).|| <= sup (Ta . x0)
by A59, SEQ_4:def 4;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).||
by XREAL_1:12;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= n0
by A58, 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:8;
then
((2 * ||.x.||) / r) * ((r / (2 * ||.x.||)) * ||.(f . x).||) <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A32, A52, XREAL_1:66;
then
((r / (2 * ||.x.||)) * ((2 * ||.x.||) / r)) * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
;
then
1
* ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A32, A52, XCMPLX_1:113;
hence
||.(f . x).|| <= KT * ||.x.||
;
:: thesis: verum
end; A60:
for
x being
Point of
X holds
||.(f . x).|| <= KT * ||.x.||
thus
for
k being
real number st
k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT
:: thesis: 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 A32, A46;
:: thesis: verum end;