let X be RealNormSpace-Sequence; for Y being RealNormSpace
for f being MultilinearOperator of X,Y
for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds
for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).||
let Y be RealNormSpace; for f being MultilinearOperator of X,Y
for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds
for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).||
let f be MultilinearOperator of X,Y; for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds
for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).||
let K be Real; ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) implies for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).|| )
assume A1:
( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) )
; for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).||
let v0, v1 be Point of (product X); for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).||
let Cv0, Cv1 be FinSequence; for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being 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).||
let i be Element of dom X; ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) implies ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )
assume A2:
( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) )
; ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||
( 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 being Function st
( Cv1 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) )
by A2, CARD_3:def 5;
A6:
ex g being Function st
( (reproj (i,v0)) . (v1 . i) = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) )
by A4, CARD_3:def 5;
for x being object st x in dom v1 holds
v1 . x = ((reproj (i,v0)) . (v1 . i)) . x
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 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 (mlt (R2,R3)) = (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 being FinSequence of REAL such that
A19:
( dom Nx = dom X & ( for i being 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 (mlt (R2,R3)) =
(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 (mlt (R2,R3)) = len X
by FINSEQ_1:def 3;
for k being Element of NAT st k in dom Nx holds
( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )
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
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||
by A12, XXREAL_0:2; verum