let X be finite-dimensional RealNormSpace; for Y being RealNormSpace
for L being LinearOperator of X,Y st dim X <> 0 holds
L is Lipschitzian
let Y be RealNormSpace; for L being LinearOperator of X,Y st dim X <> 0 holds
L is Lipschitzian
let L be LinearOperator of X,Y; ( dim X <> 0 implies L is Lipschitzian )
assume A1:
dim X <> 0
; L is Lipschitzian
reconsider X0 = X as finite-dimensional RealLinearSpace ;
set b = the OrdBasis of RLSp2RVSp X;
RLSStruct(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X #) = RLSStruct(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X #)
;
then consider r1, r2 being Real such that
A2:
( 0 < r1 & 0 < r2 & ( for x being Point of X holds
( ||.x.|| <= r1 * ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) & (max_norm (X, the OrdBasis of RLSp2RVSp X)) . x <= r2 * ||.x.|| ) ) )
by A1, REAL_NS3:24;
reconsider e = the OrdBasis of RLSp2RVSp X as FinSequence of X ;
deffunc H1( Nat) -> Element of REAL = In (||.(L . (e /. $1)).||,REAL);
A3:
the carrier of X = dom L
by FUNCT_2:def 1;
A4:
rng e c= the carrier of X
;
consider k being FinSequence of REAL such that
A5:
( len k = len the OrdBasis of RLSp2RVSp X & ( for i being Nat st i in dom k holds
k . i = H1(i) ) )
from FINSEQ_2:sch 1();
set k1 = Sum k;
for i being Nat st i in dom k holds
0 <= k . i
then A6:
0 <= Sum k
by RVSUM_1:84;
for x being Point of X holds ||.(L . x).|| <= (r2 * ((Sum k) + 1)) * ||.x.||
proof
let x be
Point of
X;
||.(L . x).|| <= (r2 * ((Sum k) + 1)) * ||.x.||
consider u being
Element of
(RLSp2RVSp X),
v being
Element of
REAL (dim X) such that A7:
(
x = u &
v = u |-- the
OrdBasis of
RLSp2RVSp X &
(max_norm (X, the OrdBasis of RLSp2RVSp X)) . x = (max_norm (dim X)) . v )
by REAL_NS3:def 3;
reconsider ub =
u |-- the
OrdBasis of
RLSp2RVSp X as
FinSequence of
REAL ;
A10:
len (u |-- the OrdBasis of RLSp2RVSp X) = len the
OrdBasis of
RLSp2RVSp X
by MATRLIN:def 7;
then A11:
dom (u |-- the OrdBasis of RLSp2RVSp X) =
Seg (len the OrdBasis of RLSp2RVSp X)
by FINSEQ_1:def 3
.=
dom the
OrdBasis of
RLSp2RVSp X
by FINSEQ_1:def 3
;
then A12:
dom (lmlt ((u |-- the OrdBasis of RLSp2RVSp X), the OrdBasis of RLSp2RVSp X)) =
dom (u |-- the OrdBasis of RLSp2RVSp X)
by MATRLIN:12
.=
Seg (len the OrdBasis of RLSp2RVSp X)
by A10, FINSEQ_1:def 3
;
A13:
lmlt (
(u |-- the OrdBasis of RLSp2RVSp X), the
OrdBasis of
RLSp2RVSp X) =
the
lmult of
(RLSp2RVSp X) .: (
(u |-- the OrdBasis of RLSp2RVSp X), the
OrdBasis of
RLSp2RVSp X)
by MATRLIN:def 5
.=
the
Mult of
X .: (
ub, the
OrdBasis of
RLSp2RVSp X)
;
A14:
rng ( the Mult of X .: (ub,e)) c= the
carrier of
X
;
reconsider f0 = the
Mult of
X .: (
ub,
e) as
FinSequence of the
carrier of
X ;
A15:
dom f0 =
Seg (len the OrdBasis of RLSp2RVSp X)
by A12, A13
.=
dom the
OrdBasis of
RLSp2RVSp X
by FINSEQ_1:def 3
;
rng f0 c= dom L
by A14, FUNCT_2:def 1;
then A16:
len (L * f0) =
len f0
by FINSEQ_2:29
.=
len the
OrdBasis of
RLSp2RVSp X
by A12, A13, FINSEQ_1:def 3
;
A17:
dom (L * f0) =
Seg (len the OrdBasis of RLSp2RVSp X)
by A16, FINSEQ_1:def 3
.=
dom the
OrdBasis of
RLSp2RVSp X
by FINSEQ_1:def 3
;
A18:
dom ( the Mult of Y .: (ub,(L * e))) = dom the
OrdBasis of
RLSp2RVSp X
proof
A19:
dom ( the Mult of Y .: (ub,(L * e))) = dom ( the Mult of Y * <:ub,(L * e):>)
by FUNCOP_1:def 3;
A20:
dom <:ub,(L * e):> =
(dom ub) /\ (dom (L * e))
by FUNCT_3:def 7
.=
(dom ub) /\ (dom e)
by A3, A4, RELAT_1:27
.=
dom the
OrdBasis of
RLSp2RVSp X
by A11
;
A21:
dom the
Mult of
Y = [:REAL, the carrier of Y:]
by FUNCT_2:def 1;
A22:
rng <:ub,(L * e):> c= [:(rng ub),(rng (L * e)):]
by FUNCT_3:51;
[:(rng ub),(rng (L * e)):] c= [:REAL, the carrier of Y:]
by ZFMISC_1:96;
then
rng <:ub,(L * e):> c= [:REAL, the carrier of Y:]
by A22;
hence
dom ( the Mult of Y .: (ub,(L * e))) = dom the
OrdBasis of
RLSp2RVSp X
by A19, A20, A21, RELAT_1:27;
verum
end;
A23:
for
i being
object st
i in dom (L * f0) holds
(L * f0) . i = ( the Mult of Y .: (ub,(L * e))) . i
proof
let i0 be
object ;
( i0 in dom (L * f0) implies (L * f0) . i0 = ( the Mult of Y .: (ub,(L * e))) . i0 )
assume A24:
i0 in dom (L * f0)
;
(L * f0) . i0 = ( the Mult of Y .: (ub,(L * e))) . i0
then reconsider i =
i0 as
Nat ;
the
OrdBasis of
RLSp2RVSp X . i in rng the
OrdBasis of
RLSp2RVSp X
by A17, A24, FUNCT_1:3;
then reconsider bi = the
OrdBasis of
RLSp2RVSp X . i as
Element of
X ;
reconsider ri =
ub . i as
Real ;
A25:
(L * e) . i = L . ( the OrdBasis of RLSp2RVSp X . i)
by A17, A24, FUNCT_1:13;
thus (L * f0) . i0 =
L . (f0 . i)
by A24, FUNCT_1:12
.=
L . ( the Mult of X . ((ub . i),( the OrdBasis of RLSp2RVSp X . i)))
by A15, A17, A24, FUNCOP_1:22
.=
L . (ri * bi)
.=
ri * (L . bi)
by LOPBAN_1:def 5
.=
the
Mult of
Y . (
(ub . i),
((L * e) . i))
by A25
.=
( the Mult of Y .: (ub,(L * e))) . i0
by A17, A18, A24, FUNCOP_1:22
;
verum
end;
reconsider f =
L * f0 as
FinSequence of the
carrier of
Y ;
A26:
L . x =
L . (Sum (lmlt ((u |-- the OrdBasis of RLSp2RVSp X), the OrdBasis of RLSp2RVSp X)))
by A7, MATRLIN:35
.=
L . (Sum f0)
by A13, REAL_NS2:75
.=
Sum (L * f0)
by Th1
.=
Sum ( the Mult of Y .: (ub,(L * e)))
by A17, A18, A23, FUNCT_1:2
.=
Sum f
by A17, A18, A23, FUNCT_1:2
;
deffunc H2(
Nat)
-> Element of
REAL =
In (
||.(f /. $1).||,
REAL);
consider g being
FinSequence of
REAL such that A27:
(
len g = len f & ( for
i being
Nat st
i in dom g holds
g . i = H2(
i) ) )
from FINSEQ_2:sch 1();
A28:
for
i being
Element of
NAT st
i in dom f holds
g . i = ||.(f /. i).||
then A29:
||.(L . x).|| <= Sum g
by A26, A27, NDIFF_5:7;
A30:
for
i being
Nat st
i in Seg (len the OrdBasis of RLSp2RVSp X) holds
g . i <= (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k) . i
proof
let i be
Nat;
( i in Seg (len the OrdBasis of RLSp2RVSp X) implies g . i <= (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k) . i )
assume A31:
i in Seg (len the OrdBasis of RLSp2RVSp X)
;
g . i <= (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k) . i
then A32:
i in dom f
by A16, FINSEQ_1:def 3;
A33:
dom ub = Seg (len the OrdBasis of RLSp2RVSp X)
by A10, FINSEQ_1:def 3;
A34:
i in dom the
OrdBasis of
RLSp2RVSp X
by A31, FINSEQ_1:def 3;
the
OrdBasis of
RLSp2RVSp X /. i in the
carrier of
X
;
then A35:
the
OrdBasis of
RLSp2RVSp X /. i in dom L
by FUNCT_2:def 1;
A36:
(L * the OrdBasis of RLSp2RVSp X) . i =
L . ( the OrdBasis of RLSp2RVSp X . i)
by A34, FUNCT_1:13
.=
L . ( the OrdBasis of RLSp2RVSp X /. i)
by A34, PARTFUN1:def 6
.=
L /. ( the OrdBasis of RLSp2RVSp X /. i)
by A35, PARTFUN1:def 6
;
A37:
i in dom f
by A16, A31, FINSEQ_1:def 3;
then f /. i =
f . i
by PARTFUN1:def 6
.=
( the Mult of Y .: (ub,(L * the OrdBasis of RLSp2RVSp X))) . i
by A17, A18, A23, FUNCT_1:2
.=
the
Mult of
Y . (
(ub . i),
((L * the OrdBasis of RLSp2RVSp X) . i))
by A17, A18, A37, FUNCOP_1:22
.=
(ub /. i) * (L /. ( the OrdBasis of RLSp2RVSp X /. i))
by A31, A33, A36, PARTFUN1:def 6
.=
(ub /. i) * (L /. ( the OrdBasis of RLSp2RVSp X /. i))
;
then A38:
g . i =
||.((ub /. i) * (L /. ( the OrdBasis of RLSp2RVSp X /. i))).||
by A28, A32
.=
|.(ub /. i).| * ||.(L /. (e /. i)).||
by NORMSP_1:def 1
;
i in dom k
by A5, A31, FINSEQ_1:def 3;
then k . i =
In (
||.(L . (e /. i)).||,
REAL)
by A5
.=
||.(L . (e /. i)).||
;
then
g . i <= ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * (k . i)
by A8, A31, A33, A38, XREAL_1:64;
hence
g . i <= (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k) . i
by RVSUM_1:45;
verum
end;
A39:
g is
len the
OrdBasis of
RLSp2RVSp X -element
by A16, A27, CARD_1:def 7;
dom (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k) =
dom k
by VALUED_1:def 5
.=
Seg (len k)
by FINSEQ_1:def 3
.=
Seg (len the OrdBasis of RLSp2RVSp X)
by A5
;
then
len (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k) = len the
OrdBasis of
RLSp2RVSp X
by FINSEQ_1:def 3;
then
((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k is
len the
OrdBasis of
RLSp2RVSp X -element
by CARD_1:def 7;
then
Sum g <= Sum (((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * k)
by A30, A39, RVSUM_1:82;
then
Sum g <= ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) * (Sum k)
by RVSUM_1:87;
then A40:
||.(L . x).|| <= (Sum k) * ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x)
by A29, XXREAL_0:2;
A41:
0 <= (max_norm (X, the OrdBasis of RLSp2RVSp X)) . x
by A1, REAL_NS3:18;
(Sum k) + 0 < (Sum k) + 1
by XREAL_1:8;
then
(Sum k) * ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) <= ((Sum k) + 1) * ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x)
by A41, XREAL_1:64;
then A42:
||.(L . x).|| <= ((Sum k) + 1) * ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x)
by A40, XXREAL_0:2;
((Sum k) + 1) * ((max_norm (X, the OrdBasis of RLSp2RVSp X)) . x) <= ((Sum k) + 1) * (r2 * ||.x.||)
by A2, A6, XREAL_1:64;
hence
||.(L . x).|| <= (r2 * ((Sum k) + 1)) * ||.x.||
by A42, XXREAL_0:2;
verum
end;
hence
L is Lipschitzian
by A2, A6, LOPBAN_1:def 8; verum