:: H\"older's Inequality and {M}inkowski's Inequality
:: by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-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, LIMFUNC1, XBOOLE_0, XXREAL_0, CARD_1, ARYTM_3,
POWER, RELAT_1, PREPOWER, ARYTM_1, PARTFUN1, FUNCT_1, FDIFF_1, VALUED_1,
SUBSET_1, TARSKI, XXREAL_1, ORDINAL2, SEQ_1, SERIES_1, VALUED_0,
COMPLEX1, SEQ_2, XXREAL_2, NAT_1, FUNCT_2, FCONT_1, CARD_3, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FUNCT_1, FUNCT_2,
LIMFUNC1, RCOMP_1, FCONT_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1,
ORDINAL1, NUMBERS, REAL_1, NAT_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2,
SEQ_2, SERIES_1, FDIFF_1, PREPOWER, POWER, TAYLOR_1, RECDEF_1;
constructors PARTFUN1, REAL_1, NAT_1, INT_2, SEQ_2, SEQM_3, RCOMP_1, RFUNCT_2,
FCONT_1, LIMFUNC1, FDIFF_1, PREPOWER, SERIES_1, TAYLOR_1, VALUED_1,
RECDEF_1, RELSET_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, RCOMP_1, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, FCONT_3,
NAT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities SUBSET_1, LIMFUNC1;
expansions TARSKI;
theorems XBOOLE_1, ABSVALUE, XBOOLE_0, XREAL_0, XCMPLX_1, RCOMP_1, SEQ_1,
SEQ_2, SEQM_3, SERIES_1, NAT_1, POWER, FCONT_1, FDIFF_1, ROLLE, SEQ_4,
PREPOWER, RELSET_1, FUNCT_2, TAYLOR_1, XREAL_1, COMPLEX1, XXREAL_0,
PARTFUN1, ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, RELAT_1, NUMBERS;
schemes SEQ_1, RECDEF_1, NAT_1, PARTFUN2;
begin :: H\"older 's inequality
reserve a, b, p, q for Real;
registration
let x be Real;
cluster right_closed_halfline(x) -> non empty;
coherence
proof
reconsider x as Real;
x in {g where g is Real: x<=g};
hence thesis by XXREAL_1:232;
end;
end;
theorem
for p, q be Real st 0 < p & 0 < q
for a be Real st 0 <= a holds
(a to_power p) * (a to_power q) = a to_power (p+q)
proof
let p, q be Real such that
A1: 0 < p and
A2: 0 < q;
let a be Real such that
A3: 0 <=a;
now
per cases;
case
A4: a=0;
then (a to_power p) * (a to_power q) = 0 * (0 to_power q) by A1,
POWER:def 2
.= 0;
hence thesis by A1,A2,A4,POWER:def 2;
end;
case
a <> 0;
hence thesis by A3,POWER:27;
end;
end;
hence thesis;
end;
theorem
for p, q be Real st 0 < p & 0 < q
for a be Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p*q)
proof
let p, q be Real such that
A1: 0 < p and
A2: 0 < q;
A3: 0 < p*q by A1,A2,XREAL_1:129;
let a be Real such that
A4: 0 <=a;
now
per cases;
case
A5: a=0;
then (a to_power p) to_power q = 0 to_power q by A1,POWER:def 2
.= 0 by A2,POWER:def 2;
hence thesis by A3,A5,POWER:def 2;
end;
case
a <> 0;
hence thesis by A4,POWER:33;
end;
end;
hence thesis;
end;
theorem Th3:
for p be Real st 0 <= p
for a,b be Real st 0 <= a & a <= b holds
a to_power p <= b to_power p
proof
let p be Real such that
A1: 0 <= p;
let a, b be Real such that
A2: 0 <= a and
A3: a <= b;
per cases by A1;
suppose
S1: 0 = p;
a to_power 0 = 1 & b to_power 0 = 1 by POWER:24;
hence thesis by S1;
end;
suppose
S2: 0 < p;
per cases;
suppose a = b;
hence thesis;
end;
suppose
A4: a <> b;
A5: a < b by A3,A4,XXREAL_0:1;
now
per cases;
suppose
A6: a=0;
then a to_power p = 0 by S2,POWER:def 2;
hence thesis by A3,A4,A6,POWER:34;
end;
suppose a <> 0;
hence thesis by A2,A5,S2,POWER:37;
end;
end;
hence thesis;
end;
end;
end;
theorem Th4:
1 < p & 1/p + 1/q = 1 & 0 < a & 0 < b implies a * b <= a #R p / p
+ b #R q / q & (a * b = a #R p / p + b #R q / q iff a #R p= b #R q)
proof
assume that
A1: 1 < p and
A2: 1/p + 1/q = 1 and
A3: 0 < a and
A4: 0 < b;
A5: 0 < b #R q by A4,PREPOWER:81;
reconsider pp=1/p as Real;
1-pp <> 0 by A1,XREAL_1:189;
then
A6: (q")" <> 0 by A2;
then ((1*q+1*p)/(p*q))*(p*q) =1*(p*q) by A1,A2,XCMPLX_1:116;
then
A7: q+p=p*q by A1,A6,XCMPLX_1:6,87;
then
A8: (q-1)*p =q;
A9: 0 < b #R (q-1) by A4,PREPOWER:81;
A10: now
assume
A11: a #R p= b #R q;
then
A12: a #R p = (b #R (q-1) ) #R p by A4,A8,PREPOWER:91;
a=a #R 1 by A3,PREPOWER:72
.=a #R (p *(1/p) ) by A1,XCMPLX_1:106
.= (a #R p ) #R (1/p) by A3,PREPOWER:91
.= (b #R (q-1) ) #R (p *(1/p)) by A4,A12,PREPOWER:81,91
.=(b #R (q-1) ) #R 1 by A1,XCMPLX_1:106
.= b #R (q-1) by A4,PREPOWER:72,81;
then a*1 = b #R (q-1);
then a *( b #R ( (1-q)+ (q-1)) ) = b #R (q-1) by A4,PREPOWER:71;
then a *(( b #R (1-q))*( b #R (q-1))) =1*( b #R (q-1)) by A4,PREPOWER:75;
then
A13: a *( b #R (1-q))*( b #R (q-1)) =1*( b #R (q-1));
thus a #R p / p + b #R q / q =b #R q *(1/ p) + b #R q / q by A11,
XCMPLX_1:99
.=b #R q *(1/ p) + b #R q *(1/q) by XCMPLX_1:99
.=b #R q * (1/p + 1/q)
.=b #R q *(a*(b #R (1-q))) by A2,A9,A13,XCMPLX_1:5
.=a* ( (b #R (1-q)) *(b #R q))
.=a*(b #R ((1-q) + q)) by A4,PREPOWER:75
.=a* b by A4,PREPOWER:72;
end;
A14: 0 < b #R (1-q) by A4,PREPOWER:81;
then
A15: 0*(b #R (1-q)) < a * (b #R (1-q)) by A3,XREAL_1:68;
ex h be PartFunc of REAL,REAL st dom(h)= right_open_halfline(0) & for x
be Real st x > 0 holds h.x=x #R p / p & h is_differentiable_in x & diff(h,x)=x
#R (p-1)
proof
set h=(1/p)(#)( #R p);
take h;
dom( #R p) =right_open_halfline(0) by TAYLOR_1:def 4;
hence
A16: dom(h)= right_open_halfline(0) by VALUED_1:def 5;
now
let x be Real such that
A17: x > 0;
x in {g where g is Real: 0<g} by A17;
then
A18: x in right_open_halfline(0) by XXREAL_1:230;
hence h.x = (1/p) * ( #R p).x by A16,VALUED_1:def 5
.=(1/p) *(x #R p) by A18,TAYLOR_1:def 4
.=(x #R p) /p by XCMPLX_1:99;
A19: ( #R p) is_differentiable_in x by A17,TAYLOR_1:21;
hence h is_differentiable_in x by FDIFF_1:15;
thus diff(h,x) = (1/p)*diff(( #R p),x) by A19,FDIFF_1:15
.= (1/p)*(p*(x #R (p-1))) by A17,TAYLOR_1:21
.= (1/p)*p*(x #R (p-1))
.= 1*x #R (p-1) by A1,XCMPLX_1:106
.=x #R (p-1);
end;
hence thesis;
end;
then consider h be PartFunc of REAL,REAL such that
A20: dom(h)= right_open_halfline(0) and
A21: for x be Real st x > 0 holds h.x=x #R p / p & h
is_differentiable_in x & diff(h,x)=x #R (p-1);
ex g be PartFunc of REAL,REAL st dom(g)=REAL &
for x be Element of REAL holds g.x=
1 / q - x & g is_differentiable_in x & diff(g,x)=-1
proof
deffunc U(Real) = In(1/q - $1,REAL);
defpred X[set] means $1 in REAL;
consider g being PartFunc of REAL,REAL such that
A22: for d be Element of REAL holds d in dom g iff X[d] and
A23: for d be Element of REAL st d in dom g holds g/.d = U(d) from
PARTFUN2:sch 2;
take g;
for x be object st x in REAL holds x in dom g by A22;
then
A24: dom(g) c= REAL & REAL c=dom(g) by RELAT_1:def 18;
then
A25: dom(g)=[#]REAL by XBOOLE_0:def 10;
A26: for d be Element of REAL holds g.d = 1 / q-d
proof
let d be Element of REAL;
g/.d = U(d) by A23,A25;
hence thesis by A25,PARTFUN1:def 6;
end;
A27: for d be Real st d in REAL holds g.d = (-1)*d + 1 / q
proof
let d be Real such that
A28: d in REAL;
thus g.d=1 / q-d by A26,A28
.= (-1)*d + 1 / q;
end;
then
A29: g is_differentiable_on dom(g) by A25,FDIFF_1:23;
for x be Element of REAL holds g is_differentiable_in x & diff(g,x)=-1
proof
let d be Element of REAL;
thus g is_differentiable_in d by A25,A29,FDIFF_1:9;
thus diff(g,d)=(g`|dom(g)).d by A25,A29,FDIFF_1:def 7
.= -1 by A25,A27,FDIFF_1:23;
end;
hence thesis by A24,A26,XBOOLE_0:def 10;
end;
then consider g be PartFunc of REAL,REAL such that
A30: dom(g)=REAL and
A31: for x be Element of REAL holds g.x=1 / q - x and
A32: for x be Element of REAL holds g is_differentiable_in x & diff(g,x)=-1;
set f=h+g;
A33: dom f= right_open_halfline(0) /\ REAL by A30,A20,VALUED_1:def 1
.= right_open_halfline(0) by XBOOLE_1:28;
A34: for x be Real st x in right_open_halfline(0) holds f.x=x #R p / p + 1 /
q - x & f is_differentiable_in x & diff(f,x)=x #R (p-1) -1
proof
let x be Real such that
A35: x in right_open_halfline(0);
reconsider xx=x as Element of REAL by XREAL_0:def 1;
x in {y where y is Real: 0< y} by A35,XXREAL_1:230;
then
A36: ex y be Real st x=y & 0 < y;
then
A37: diff(h,x)=x #R (p-1) by A21;
thus f.x=h.x + g.x by A33,A35,VALUED_1:def 1
.=x #R p / p + g.xx by A21,A36
.=x #R p / p +(1 / q - x) by A31
.=x #R p / p +1 / q - x;
A38: g is_differentiable_in xx by A32;
A39: h is_differentiable_in x by A21,A36;
hence f is_differentiable_in x by A38,FDIFF_1:13;
A40: diff(g,xx)=-1 by A32;
thus diff(f,x)=diff(h,x)+diff(g,x) by A38,A39,FDIFF_1:13
.=x #R (p-1) - 1 by A40,A37;
end;
A41: for x be Real st 0 < x & x <> 1 holds x < x #R p / p + 1 / q
proof
1 in {y where y is Real: 0< y};
then 1 in right_open_halfline(0) by XXREAL_1:230;
then
A42: f.1= 1 #R p / p + 1 / q - 1 by A34
.=1/p + 1/q -1 by PREPOWER:73
.=0 by A2;
for x be Real st x in right_open_halfline(0) holds f
is_differentiable_in x by A34;
then
A43: f is_differentiable_on right_open_halfline(0) by A33,FDIFF_1:9;
let x be Real such that
A44: 0 < x and
A45: x <> 1;
x in {y where y is Real: 0< y} by A44;
then
A46: x in right_open_halfline(0) by XXREAL_1:230;
now
per cases by A45,XXREAL_0:1;
case
x<1;
then
A47: 1-1 < 1-x by XREAL_1:15;
set t=1-x;
A48: 1-1 < p-1 by A1,XREAL_1:14;
now
let z be object;
assume z in [.x,x+t.];
then z in {r where r is Real: x<=r & r<=x+t }
by RCOMP_1:def 1;
then ex r be Real st r=z & x<=r & r<=x+t;
then z in {y where y is Real: 0< y} by A44;
hence z in right_open_halfline(0) by XXREAL_1:230;
end;
then
A49: [.x,x+t.] c= right_open_halfline(0);
f|right_open_halfline(0) is continuous by A43,FDIFF_1:25;
then
A50: f|[.x,x+t.] is continuous by A49,FCONT_1:16;
].x,x+t.[ c= [.x,x+t.] by XXREAL_1:25;
then f is_differentiable_on ].x,x+t.[ by A43,A49,FDIFF_1:26,XBOOLE_1:1;
then consider s be Real such that
A51: 0<s and
A52: s<1 and
A53: f.(x+t) = f.x + t*diff(f,x+s*t) by A33,A47,A49,A50,ROLLE:4;
s*t < 1*t by A47,A52,XREAL_1:68;
then x+s*t < x+t by XREAL_1:8;
then (x+s*t) to_power (p-1) < (x+s*t) to_power 0 by A44,A47,A51,A48,
POWER:40;
then (x+s*t) #R (p-1) < (x+s*t) to_power 0 by A44,A47,A51,POWER:def 2;
then (x+s*t) #R (p-1) < (x+s*t) #R 0 by A44,A47,A51,POWER:def 2;
then (x+s*t) #R (p-1) < 1 by A44,A47,A51,PREPOWER:71;
then
A54: (x+s*t) #R (p-1) -1 < 1-1 by XREAL_1:14;
x+s*t in {y where y is Real: 0< y} by A44,A47,A51;
then x+s*t in right_open_halfline(0) by XXREAL_1:230;
then diff(f,x+s*t) =(x+s*t) #R (p-1)-1 by A34;
then t*diff(f,x+s*t) < t*0 by A47,A54,XREAL_1:68;
then f.x + t*diff(f,x+s*t) < f.x +0 by XREAL_1:8;
then 0 < x #R p / p + 1 / q-x by A34,A46,A42,A53;
then 0+x < x #R p / p + 1 / q-x+x by XREAL_1:8;
hence thesis;
end;
case
x > 1;
then
A55: 1-1 < x-1 by XREAL_1:14;
set t=x-1;
now
let z be object;
assume z in [.1,1+t.];
then z in {r where r is Real: 1<=r & r<=1+t }
by RCOMP_1:def 1;
then ex r be Real st r=z & 1<=r & r<=1+t;
then z in {y where y is Real: 0< y};
hence z in right_open_halfline(0) by XXREAL_1:230;
end;
then
A56: [.1,1+t.] c= right_open_halfline(0);
A57: 1-1 < p-1 by A1,XREAL_1:14;
f|right_open_halfline(0) is continuous by A43,FDIFF_1:25;
then
A58: f|[.1,1+t.] is continuous by A56,FCONT_1:16;
].1,1+t.[ c= [.1,1+t.] by XXREAL_1:25;
then f is_differentiable_on ].1,1+t.[ by A43,A56,FDIFF_1:26,XBOOLE_1:1;
then consider s be Real such that
A59: 0<s and
s<1 and
A60: f.(1+t) = f.1 + t*diff(f,1+s*t) by A33,A55,A56,A58,ROLLE:4;
0*t < s*t by A55,A59,XREAL_1:68;
then 1+ 0 < 1+ s*t by XREAL_1:8;
then 1 < (1+s*t) #R (p-1) by A57,PREPOWER:86;
then
A61: 1-1 < (1+s*t) #R (p-1) -1 by XREAL_1:14;
1+s*t in {y where y is Real: 0< y} by A55,A59;
then 1+s*t in right_open_halfline(0) by XXREAL_1:230;
then diff(f,1+s*t) =(1+s*t) #R (p-1)-1 by A34;
then t*0 < t*diff(f,1+s*t) by A55,A61,XREAL_1:68;
then 0 < x #R p / p + 1 / q-x by A34,A46,A42,A60;
then 0+x < x #R p / p + 1 / q-x+x by XREAL_1:8;
hence thesis;
end;
end;
hence thesis;
end;
A62: (1-q)*p + q=0 by A7;
A63: now
assume a * b = a #R p / p + b #R q / q;
then a*b = a #R p /p+ (1 / q)*(b #R q) by XCMPLX_1:99;
then a*b = a #R p * (1/p)+ (1 / q)*(b #R q) by XCMPLX_1:99;
then a*b = a #R p * (b #R 0/p)+ (1 / q)*(b #R q) by A4,PREPOWER:71;
then a*b = a #R p * ((b #R ((1-q)*p) )*(b #R q)/p)+ (1 / q)*(b #R q) by A4
,A62,PREPOWER:75;
then a*b = a #R p * ((b #R ((1-q)*p) )/ p*(b #R q))+ (1 / q)*(b #R q) by
XCMPLX_1:74;
then a*b = (a #R p * ((b #R ((1-q)*p) )/ p )*(b #R q))+ (1 / q)*(b #R q);
then a*b = (a #R p * (b #R ((1-q)*p) )/ p )*(b #R q)+ (1 / q)*(b #R q) by
XCMPLX_1:74;
then a*b = (a #R p * (b #R ((1-q)*p) )/ p + 1 / q)*(b #R q);
then
a*b = ((a #R p * (b #R (1-q)) #R p )/ p + 1 / q)*(b #R q) by A4,PREPOWER:91;
then
a*b = ((a * (b #R (1-q))) #R p / p + 1 / q)*(b #R q) by A3,A14,PREPOWER:78;
then a*(b #R ((1-q) + q)) = ((a * (b #R (1-q))) #R p / p + 1 / q)*(b #R q
) by A4,PREPOWER:72;
then a*( (b #R (1-q)) *(b #R q)) = ((a * (b #R (1-q))) #R p / p + 1 / q)*
(b #R q) by A4,PREPOWER:75;
then a * (b #R (1-q)) *(b #R q) = ((a * (b #R (1-q))) #R p / p + 1 / q)*(
b #R q);
then
A64: a * (b #R (1-q)) = (a * (b #R (1-q))) #R p / p + 1 / q by A5,XCMPLX_1:5;
a *(( b #R (1-q))*( b #R (q-1))) = a *( b #R (1-q))*( b #R (q-1))
.= 1*( b #R (q-1)) by A41,A15,A64;
then a *( b #R ( (1-q)+ (q-1)) ) = b #R (q-1) by A4,PREPOWER:75;
then a*1 = b #R (q-1) by A4,PREPOWER:71;
hence a #R p = b #R q by A4,A8,PREPOWER:91;
end;
a * (b #R (1-q)) <= (a * (b #R (1-q))) #R p / p + 1 / q
proof
now
per cases;
case
a * (b #R (1-q)) =1;
hence a * (b #R (1-q)) =(a * (b #R (1-q))) #R p / p + 1 / q by A2,
PREPOWER:73;
end;
case
a * (b #R (1-q)) <>1;
hence thesis by A41,A15;
end;
end;
hence thesis;
end;
then a * (b #R (1-q)) *(b #R q) <= ((a * (b #R (1-q))) #R p / p + 1 / q)*(b
#R q) by A5,XREAL_1:64;
then a*( (b #R (1-q)) *(b #R q)) <= ((a * (b #R (1-q))) #R p / p + 1 / q)*(
b #R q);
then a*(b #R ((1-q) + q)) <= ((a * (b #R (1-q))) #R p / p + 1 / q)*(b #R q)
by A4,PREPOWER:75;
then a*b <= ((a * (b #R (1-q))) #R p / p + 1 / q)*(b #R q) by A4,PREPOWER:72;
then a*b <= ((a #R p * (b #R (1-q)) #R p )/ p + 1 / q)*(b #R q) by A3,A14,
PREPOWER:78;
then a*b <= (a #R p * (b #R ((1-q)*p) )/ p + 1 / q)*(b #R q) by A4,
PREPOWER:91;
then a*b <= (a #R p * (b #R ((1-q)*p) )/ p )*(b #R q)+ (1 / q)*(b #R q);
then a*b <= (a #R p * ((b #R ((1-q)*p) )/ p )*(b #R q))+ (1 / q)*(b #R q)
by XCMPLX_1:74;
then a*b <= a #R p * ((b #R ((1-q)*p) )/ p*(b #R q))+ (1 / q)*(b #R q);
then a*b <= a #R p * ((b #R ((1-q)*p) )*(b #R q)/p)+ (1 / q)*(b #R q) by
XCMPLX_1:74;
then a*b <= a #R p * (b #R ((1-q)*p + q)/p)+ (1 / q)*(b #R q) by A4,
PREPOWER:75;
then a*b <= a #R p * (1/p)+ (1 / q)*(b #R q) by A4,A7,PREPOWER:71;
then a*b <= a #R p /p+ (1 / q)*(b #R q) by XCMPLX_1:99;
hence thesis by A63,A10,XCMPLX_1:99;
end;
theorem Th5:
1 < p & 1/p + 1/q = 1 & 0 <= a & 0 <= b implies a * b <= a
to_power p / p + b to_power q / q & (a * b = a to_power p / p + b to_power q /
q iff a to_power p = b to_power q)
proof
assume that
A1: 1 < p and
A2: 1/p + 1/q = 1 and
A3: 0 <= a and
A4: 0 <= b;
A5: 0 <= a to_power p / p
proof
now
per cases by A3;
case
0 < a;
then 0 < a to_power p by POWER:34;
hence thesis by A1;
end;
case
0 = a;
then 0 = a to_power p by A1,POWER:def 2;
hence thesis;
end;
end;
hence thesis;
end;
reconsider pp=1/p as Real;
1/p < 1 by A1,XREAL_1:189;
then
A6: 1-1 < 1-pp by XREAL_1:15;
then
A7: 0 < q by A2;
A8: 0 <= b to_power q / q
proof
now
per cases by A4;
case
0 < b;
then 0 < b to_power q by POWER:34;
hence thesis by A7;
end;
case
0 = b;
then 0 = b to_power q by A7,POWER:def 2;
hence thesis;
end;
end;
hence thesis;
end;
now
per cases;
case
A9: a*b=0;
now
per cases by A9,XCMPLX_1:6;
case
A10: a=0;
A11: now
assume a * b = a to_power p / p + b to_power q / q;
then 0 = 0/p + b to_power q / q by A1,A10,POWER:def 2;
then 0*q = (b to_power q /q)*q;
then 0 = b to_power q by A7,XCMPLX_1:87;
then
A12: 0 = (b to_power q ) to_power (1/q) by A2,A6,POWER:def 2;
A13: 0=b
proof
assume
A14: b <> 0;
then 0 = b to_power (q * (1/q) ) by A4,A12,POWER:33;
then 0 = b to_power 1 by A7,XCMPLX_1:106;
hence contradiction by A14,POWER:25;
end;
thus a to_power p = 0 by A1,A10,POWER:def 2
.= b to_power q by A7,A13,POWER:def 2;
end;
now
assume a to_power p = b to_power q;
then
A15: b to_power q /q =0 /q by A1,A10,POWER:def 2
.=0;
a to_power p /p = 0/p by A1,A10,POWER:def 2
.=0;
hence a*b=a to_power p /p + b to_power q /q by A9,A15;
end;
hence a * b = a to_power p / p + b to_power q / q iff a to_power p =
b to_power q by A11;
end;
case
A16: b=0;
A17: 1/p > 0 by A1,XREAL_1:139;
A18: now
assume a * b = a to_power p / p + b to_power q / q;
then 0 = 0/q + a to_power p / p by A7,A16,POWER:def 2;
then 0*p = (a to_power p/p)*p;
then 0 = a to_power p by A1,XCMPLX_1:87;
then
A19: 0 = (a to_power p ) to_power (1/p) by A17,POWER:def 2;
A20: 0=a
proof
assume
A21: a <> 0;
then 0 = a to_power (p * (1/p) ) by A3,A19,POWER:33;
then 0 = a to_power 1 by A1,XCMPLX_1:106;
hence contradiction by A21,POWER:25;
end;
thus b to_power q = 0 by A7,A16,POWER:def 2
.= a to_power p by A1,A20,POWER:def 2;
end;
now
assume a to_power p = b to_power q;
then
A22: a to_power p /p =0 /p by A7,A16,POWER:def 2
.=0;
b to_power q /q = 0/q by A7,A16,POWER:def 2
.= 0;
hence a*b=a to_power p /p + b to_power q /q by A9,A22;
end;
hence a * b = a to_power p / p + b to_power q / q iff a to_power p =
b to_power q by A18;
end;
end;
hence thesis by A5,A8;
end;
case
A23: a*b<>0;
then
A24: a <> 0;
A25: b <> 0 by A23;
then
a * b = a #R p / p + b #R q / q iff a #R p = b #R q by A1,A2,A3,A4,A24
,Th4;
then
A26: a * b = a to_power p / p + b #R q / q iff a to_power p = b #R q by A3,A24
,POWER:def 2;
a * b <= a #R p / p + b #R q / q by A1,A2,A3,A4,A24,A25,Th4;
then a * b <= a to_power p / p + b #R q / q by A3,A24,POWER:def 2;
hence thesis by A4,A25,A26,POWER:def 2;
end;
end;
hence thesis;
end;
Lm1: for a be Real_Sequence st
for n be Nat holds 0 <= a.n
for n be Nat holds a.n <= Partial_Sums(a).n
proof
let a be Real_Sequence such that
A1: for n be Nat holds 0 <= a.n;
defpred P[Nat] means a.$1 <=Partial_Sums(a).$1;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then
A3: Partial_Sums(a).(n+1) = Partial_Sums(a).n + a.(n+1) & a.n + a.(n+1) <=
Partial_Sums(a).n + a.(n+1) by SERIES_1:def 1,XREAL_1:6;
0 <= a.n by A1;
then 0 + a.(n+1) <= a.n + a.(n+1) by XREAL_1:6;
hence thesis by A3,XXREAL_0:2;
end;
A4: P[0] by SERIES_1:def 1;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
Lm2: for a be Real_Sequence st
for n be Nat holds 0 <= a.n
for n be Nat holds 0 <= Partial_Sums(a).n
proof
let a be Real_Sequence such that
A1: for n be Nat holds 0 <= a.n;
let n be Nat;
a.n <=Partial_Sums(a).n by A1,Lm1;
hence thesis by A1;
end;
Lm3: for a be Real_Sequence st
for n be Nat holds 0 <= a.n
for n be Nat st Partial_Sums(a).n=0
for k be Nat st k <= n holds a.k=0
proof
let a be Real_Sequence such that
A1: for n be Nat holds 0 <= a.n;
let n be Nat such that
A2: Partial_Sums(a).n=0;
now
A3: Partial_Sums(a) is non-decreasing by A1,SERIES_1:16;
let k be Nat;
assume k <=n;
then
A4: Partial_Sums(a).k <= Partial_Sums(a).n by A3,SEQM_3:6;
a.k <=Partial_Sums(a).k by A1,Lm1;
hence a.k=0 by A1,A2,A4;
end;
hence thesis;
end;
Lm4: for a be Real_Sequence for n be Nat
st for k be Nat st k <=n holds a.k=0
holds Partial_Sums(a).n=0
proof
let a be Real_Sequence;
defpred P[Nat] means
(for k be Nat st k <=$1 holds a.k
=0) implies Partial_Sums(a).$1=0;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: P[n];
now
assume
A3: for k be Nat st k <=n+1 holds a.k=0;
A4: now
A5: n <= n+1 by NAT_1:11;
let k be Nat;
assume k <= n;
hence a.k=0 by A3,A5,XXREAL_0:2;
end;
thus Partial_Sums(a).(n+1) =Partial_Sums(a).n+a.(n+1) by SERIES_1:def 1
.=0 by A2,A3,A4;
end;
hence thesis;
end;
A6: P[0]
proof
assume for k be Nat st k <=0 holds a.k=0;
then a.0=0;
hence thesis by SERIES_1:def 1;
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(A6,A1);
end;
begin :: Minkowski's inequality
theorem Th6:
for p, q be Real st 1 < p & 1/p + 1/q = 1
for a,b,ap,bq,ab be
Real_Sequence st ( for n be Nat holds ap.n=|.a.n.| to_power p & bq.
n=|.b.n.| to_power q & ab.n=|.a.n* b.n.|) holds for n be Nat holds
Partial_Sums(ab).n <= ( (Partial_Sums(ap).n) to_power (1/p) ) * ( (Partial_Sums
(bq).n) to_power (1/q) )
proof
let p,q be Real such that
A1: 1 < p and
A2: 1/p + 1/q = 1;
reconsider pp=1/p as Real;
let a,b,ap,bq,ab be Real_Sequence such that
A3: for n be Nat holds ap.n=|.a.n.| to_power p & bq.n=|.b.
n.| to_power q & ab.n=|.a.n* b.n.|;
let n be Nat;
set B=Partial_Sums(bq).n;
1/p < 1 by A1,XREAL_1:189;
then
A4: 1-1 < 1-pp by XREAL_1:15;
then
A5: 0 < q by A2;
A6: for n be Nat holds 0 <= bq.n
proof
let n be Nat;
A7: bq.n=|.b.n.| to_power q by A3;
now
per cases by COMPLEX1:46;
case
|.b.n.| = 0;
hence thesis by A5,A7,POWER:def 2;
end;
case
|.b.n.| > 0;
hence thesis by A7,POWER:34;
end;
end;
hence thesis;
end;
then
A8: 0 <= B by Lm2;
set A=Partial_Sums(ap).n;
A9: for n be Nat holds 0 <= ap.n
proof
let n be Nat;
A10: ap.n=|.a.n.| to_power p by A3;
now
per cases by COMPLEX1:46;
case
|.a.n.| = 0;
hence thesis by A1,A10,POWER:def 2;
end;
case
|.a.n.| > 0;
hence thesis by A10,POWER:34;
end;
end;
hence thesis;
end;
then
A11: 0 <= A by Lm2;
set Bq=B to_power (1/q);
set Ap=A to_power (1/p);
A12: 1/p > 0 by A1,XREAL_1:139;
now
per cases;
case
A13: A*B = 0;
A14: 0 <= Ap
proof
now
per cases by A9,Lm2;
case
0 < A;
hence thesis by POWER:34;
end;
case
0 = A;
hence thesis by A12,POWER:def 2;
end;
end;
hence thesis;
end;
0 <= Bq
proof
now
per cases by A6,Lm2;
case
0 < B;
hence thesis by POWER:34;
end;
case
0 = B;
hence thesis by A2,A4,POWER:def 2;
end;
end;
hence thesis;
end;
then
A15: 0 <=Ap*Bq by A14;
now
per cases by A13,XCMPLX_1:6;
case
A16: A=0;
A17: for k be Nat st k <=n holds a.k=0
proof
let k be Nat;
assume k <=n;
then ap.k=0 by A9,A16,Lm3;
then
A18: |.a.k.| to_power p = 0 by A3;
|.a.k.| =0
proof
assume |.a.k.| <> 0;
then |.a.k.| > 0 by COMPLEX1:46;
hence contradiction by A18,POWER:34;
end;
hence thesis by ABSVALUE:2;
end;
for k be Nat st k <=n holds ab.k=0
proof
let k be Nat such that
A19: k <=n;
thus ab.k=|.a.k * b.k.| by A3
.=|.0 * b.k.| by A17,A19
.=0 by ABSVALUE:2;
end;
hence thesis by A15,Lm4;
end;
case
A20: B=0;
A21: for k be Nat st k <=n holds b.k=0
proof
let k be Nat;
assume k <=n;
then bq.k=0 by A6,A20,Lm3;
then
A22: |.b.k.| to_power q = 0 by A3;
|.b.k.| =0
proof
assume |.b.k.| <> 0;
then |.b.k.| > 0 by COMPLEX1:46;
hence contradiction by A22,POWER:34;
end;
hence thesis by ABSVALUE:2;
end;
for k be Nat st k <=n holds ab.k=0
proof
let k be Nat such that
A23: k <=n;
thus ab.k=|.a.k * b.k.| by A3
.=|.a.k * 0.| by A21,A23
.=0 by ABSVALUE:2;
end;
hence thesis by A15,Lm4;
end;
end;
hence thesis;
end;
case
A24: A*B <> 0;
deffunc G(Nat) =|.b.$1.|/Bq;
consider y be Real_Sequence such that
A25: for n be Nat holds y.n=G(n) from SEQ_1:sch 1;
A26: B <> 0 by A24;
then
A27: Bq > 0 by A8,POWER:34;
A28: for n be Nat holds 0 <=y.n
proof
let n be Nat;
0 <= |.b.n.| by COMPLEX1:46;
then 0 <= |.b.n.|/Bq by A27;
hence thesis by A25;
end;
deffunc F(Nat) =|.a.$1.|/Ap;
consider x be Real_Sequence such that
A29: for n be Nat holds x.n=F(n) from SEQ_1:sch 1;
A30: for n be Nat holds ((1/(Ap*Bq)) (#) ab).n = x.n * y.n
proof
let n be Nat;
x.n= |.a.n.|/Ap & y.n= |.b.n.|/Bq by A29,A25;
hence x.n*y.n= (|.a.n.|*|.b.n.|)/(Ap*Bq) by XCMPLX_1:76
.=|.a.n*b.n.|/(Ap*Bq) by COMPLEX1:65
.=ab.n/(Ap*Bq) by A3
.=(1/(Ap*Bq))*ab.n by XCMPLX_1:99
.=((1/(Ap*Bq)) (#) ab).n by SEQ_1:9;
end;
A31: Partial_Sums( (1/(Ap*Bq)) (#) ab).n = ((1/(Ap*Bq)) (#) Partial_Sums
(ab)).n by SERIES_1:9
.= (1/(Ap*Bq)) * Partial_Sums(ab).n by SEQ_1:9;
A32: A <> 0 by A24;
then
A33: Ap > 0 by A11,POWER:34;
then
A34: Ap*Bq > 0 by A27,XREAL_1:129;
A35: for n be Nat holds (((1/p)(#)((1/A)(#)ap)) + ((1/q)(#)((
1/B)(#)bq))).n = (x.n) to_power p / p + (y.n) to_power q / q
proof
let n be Nat;
A36: (|.a.n.|/Ap) to_power p =|.a.n.| to_power p/Ap to_power p
proof
now
per cases;
case
A37: |.a.n.| =0;
hence (|.a.n.|/Ap) to_power p =0 /Ap to_power p by A1,
POWER:def 2
.=|.a.n.| to_power p/Ap to_power p by A1,A37,POWER:def 2;
end;
case
|.a.n.| <> 0;
then |.a.n.| > 0 by COMPLEX1:46;
hence thesis by A33,POWER:31;
end;
end;
hence thesis;
end;
A38: (|.b.n.|/Bq) to_power q =|.b.n.| to_power q/Bq to_power q
proof
now
per cases;
case
A39: |.b.n.| =0;
hence (|.b.n.|/Bq) to_power q =0 /Bq to_power q by A5,
POWER:def 2
.=|.b.n.| to_power q/Bq to_power q by A5,A39,POWER:def 2;
end;
case
|.b.n.| <> 0;
then |.b.n.| > 0 by COMPLEX1:46;
hence thesis by A27,POWER:31;
end;
end;
hence thesis;
end;
y.n= |.b.n.|/Bq by A25;
then
A40: (y.n) to_power q / q =( bq.n / Bq to_power q) /q by A3,A38
.=( bq.n / (B to_power ((1/q)*q))) /q by A8,A26,POWER:33
.= ( bq.n / (B to_power 1 )) /q by A5,XCMPLX_1:87
.= ( bq.n / B ) /q by POWER:25
.= (1/q)*(bq.n / B) by XCMPLX_1:99
.= (1/q)*((1/B)*bq.n) by XCMPLX_1:99
.= (1/q)*(((1/B)(#)bq).n) by SEQ_1:9
.=((1/q)(#)((1/B)(#)bq)).n by SEQ_1:9;
x.n= |.a.n.|/Ap by A29;
then (x.n) to_power p / p =( ap.n / Ap to_power p) /p by A3,A36
.=( ap.n / (A to_power ((1/p)*p))) /p by A11,A32,POWER:33
.= ( ap.n / (A to_power 1 )) /p by A1,XCMPLX_1:87
.= ( ap.n / A ) /p by POWER:25
.= (1/p)*(ap.n / A) by XCMPLX_1:99
.= (1/p)*((1/A)*ap.n) by XCMPLX_1:99
.= (1/p)*(((1/A)(#)ap).n) by SEQ_1:9
.=((1/p)(#)((1/A)(#)ap)).n by SEQ_1:9;
hence thesis by A40,SEQ_1:7;
end;
A41: for n be Nat holds 0 <=x.n
proof
let n be Nat;
0 <= |.a.n.| by COMPLEX1:46;
then 0 <= |.a.n.|/Ap by A33;
hence thesis by A29;
end;
A42: for n be Nat holds x.n * y.n <= (x.n) to_power p / p + (
y.n) to_power q / q & (x.n * y.n = (x.n) to_power p / p + (y.n) to_power q / q
iff (x.n) to_power p = (y.n) to_power q)
proof
let n be Nat;
0 <= x.n & 0 <= y.n by A41,A28;
hence thesis by A1,A2,Th5;
end;
for n be Nat holds ((1/(Ap*Bq)) (#) ab).n <= (((1/p)(#)(
(1/A)(#)ap)) + ((1/q)(#)((1/B)(#)bq))).n
proof
let n be Nat;
x.n * y.n <= (x.n) to_power p / p + (y.n) to_power q / q & (((1/p
)(#)((1/A) (#)ap)) + ((1/q)(#)((1/B)(#)bq))).n = (x.n) to_power p / p + (y.n)
to_power q / q by A42,A35;
hence thesis by A30;
end;
then
A43: Partial_Sums( (1/(Ap*Bq)) (#) ab).n <=Partial_Sums(((1/p)(#)((1/A)
(#)ap)) + ((1/q)(#)((1/B)(#)bq))).n by SERIES_1:14;
Partial_Sums(((1/p)(#)((1/A)(#)ap)) + ((1/q)(#)((1/B)(#)bq))).n = (
Partial_Sums(((1/p)(#)((1/A)(#)ap))) + Partial_Sums(((1/q)(#)((1/B)(#)bq)))).n
by SERIES_1:5
.=Partial_Sums((1/p)(#)((1/A)(#)ap)).n + Partial_Sums((1/q)(#)((1/B)
(#)bq)).n by SEQ_1:7
.=((1/p)(#)Partial_Sums((1/A)(#)ap)).n + Partial_Sums((1/q)(#)((1/B)
(#)bq)).n by SERIES_1:9
.=(1/p)*(Partial_Sums((1/A)(#)ap).n) + Partial_Sums((1/q)(#)((1/B)
(#)bq)).n by SEQ_1:9
.=(1/p)*(((1/A)(#)Partial_Sums(ap)).n) + Partial_Sums((1/q)(#)((1/B)
(#)bq)).n by SERIES_1:9
.=(1/p)*((1/A)*Partial_Sums(ap).n) + Partial_Sums((1/q)(#)((1/B)(#)
bq)).n by SEQ_1:9
.=(1/p)*((1/A)*Partial_Sums(ap).n) + ((1/q)(#)Partial_Sums((1/B)(#)
bq)).n by SERIES_1:9
.=(1/p)*((1/A)*Partial_Sums(ap).n) + (1/q)*(Partial_Sums((1/B)(#)bq)
.n) by SEQ_1:9
.=(1/p)*((1/A)*Partial_Sums(ap).n) + (1/q)*(((1/B)(#)Partial_Sums(bq
)).n) by SERIES_1:9
.=(1/p)*((1/A)*Partial_Sums(ap).n) +(1/q)*((1/B)*Partial_Sums(bq).n)
by SEQ_1:9
.=(1/p)*1 +(1/q)*((1/B)*B) by A32,XCMPLX_1:87
.=(1/p)*1 +(1/q)*(1) by A26,XCMPLX_1:87
.=1 by A2;
then Partial_Sums(ab).n/(Ap*Bq) <= 1 by A43,A31,XCMPLX_1:99;
hence thesis by A34,XREAL_1:187;
end;
end;
hence thesis;
end;
theorem Th7:
for p be Real st 1 < p
for a,b,ap,bp,ab be Real_Sequence st ( for
n be Nat holds ap.n=|.a.n.| to_power p & bp.n=|.b.n.| to_power p &
ab.n=|.a.n+b.n.| to_power p ) holds for n be Nat holds (
Partial_Sums(ab).n) to_power (1/p) <= ( Partial_Sums(ap).n) to_power (1/p) + (
Partial_Sums(bp).n) to_power (1/p)
proof
let p be Real such that
A1: 1 < p;
A2: 1/p > 0 by A1,XREAL_1:139;
let a,b,ap,bp,ab be Real_Sequence such that
A3: for n be Nat holds ap.n=|.a.n.| to_power p & bp.n=|.b.
n.| to_power p & ab.n=|.a.n+ b.n.| to_power p;
A4: for n be Nat holds 0 <= ap.n
proof
let n be Nat;
A5: ap.n=|.a.n.| to_power p by A3;
now
per cases by COMPLEX1:46;
case
|.a.n.| = 0;
hence thesis by A1,A5,POWER:def 2;
end;
case
|.a.n.| > 0;
hence thesis by A5,POWER:34;
end;
end;
hence thesis;
end;
A6: for n be Nat holds 0 <= bp.n
proof
let n be Nat;
A7: bp.n=|.b.n.| to_power p by A3;
now
per cases by COMPLEX1:46;
case
|.b.n.| = 0;
hence thesis by A1,A7,POWER:def 2;
end;
case
|.b.n.| > 0;
hence thesis by A7,POWER:34;
end;
end;
hence thesis;
end;
deffunc F(Nat)=|.a.$1+ b.$1.| to_power (p-1);
consider x be Real_Sequence such that
A8: for n be Nat holds x.n=F(n) from SEQ_1:sch 1;
A9: 1-1 < p-1 by A1,XREAL_1:14;
A10: for n be Nat holds 0 <= x.n
proof
let n be Nat;
A11: x.n=|.a.n+ b.n.| to_power (p-1) by A8;
now
per cases by COMPLEX1:46;
case
|.a.n+ b.n.| = 0;
hence thesis by A9,A11,POWER:def 2;
end;
case
|.a.n+ b.n.| > 0;
hence thesis by A11,POWER:34;
end;
end;
hence thesis;
end;
A12: for n be Nat holds (x(#)abs(b)).n= |.b.n*x.n.|
proof
let n be Nat;
0 <= x.n by A10;
then
A13: |.x.n.|=x.n by ABSVALUE:def 1;
thus (x(#)abs(b)).n =x.n * abs(b).n by SEQ_1:8
.=x.n * |.b.n.| by SEQ_1:12
.=|.b.n*x.n.| by A13,COMPLEX1:65;
end;
reconsider pp=1/p as Real;
reconsider qq=1-pp as Real;
reconsider q=1/qq as Real;
A14: qq=1/q by XCMPLX_1:56;
then
A15: 1/p + 1/q= 1;
1/p < 1 by A1,XREAL_1:189;
then
A16: 1-1 < 1-pp by XREAL_1:15;
then
A17: q <> 0 by A14;
then ((1*q+1*p)/(p*q))*(p*q) =1*(p*q) by A1,A15,XCMPLX_1:116;
then
A18: q+p=p*q by A1,A17,XCMPLX_1:6,87;
A19: for n be Nat holds ab.n=x.n*|.a.n+b.n.|
proof
let n be Nat;
now
per cases;
case
A20: |.a.n+b.n.|=0;
thus ab.n=|.a.n+ b.n.| to_power p by A3
.= x.n * |.a.n+b.n.| by A1,A20,POWER:def 2;
end;
case
A21: |.a.n+b.n.| <> 0;
A22: 0 <= |.a.n+b.n.| by COMPLEX1:46;
thus ab.n =|.a.n+ b.n.| to_power ((p-1)+1) by A3
.= |.a.n+ b.n.| to_power (p-1) * |.a.n+ b.n.| to_power 1 by A21,A22
,POWER:27
.=(|.a.n+ b.n.| to_power (p-1)) * |.a.n+ b.n.| by POWER:25
.= x.n * |.a.n+b.n.| by A8;
end;
end;
hence thesis;
end;
A23: for n be Nat holds ab.n <= ( x(#)abs(a)+x(#)abs(b) ).n
proof
let n be Nat;
A24: x.n * (|.a.n.|+|.b.n.|) = x.n * (|.a.n.|)+x.n * (|.b.n.|)
.= x.n * (abs(a).n)+x.n * (|.b.n.|) by SEQ_1:12
.= x.n * (abs(a).n)+x.n * (abs(b).n) by SEQ_1:12
.= (x(#)abs(a)).n +x.n * (abs(b).n) by SEQ_1:8
.= (x(#)abs(a)).n +(x(#)abs(b)).n by SEQ_1:8
.= (x(#)abs(a) +x(#)abs(b)).n by SEQ_1:7;
0 <= x.n & ab.n=x.n*|.a.n+b.n.| by A10,A19;
hence thesis by A24,COMPLEX1:56,XREAL_1:64;
end;
A25: 0 < q by A16,A14;
A26: for n be Nat holds |.x.n.| to_power q = ab.n
proof
let n be Nat;
0 <= x.n by A10;
then |.x.n.|=x.n by ABSVALUE:def 1;
then
A27: |.x.n.| to_power q = (|.a.n+b.n.| to_power (p-1)) to_power q by A8;
now
per cases;
case
A28: |.a.n+b.n.|=0;
then
A29: ab.n = 0 to_power p by A3
.= 0 by A1,POWER:def 2;
|.x.n.| to_power q =0 to_power q by A9,A27,A28,POWER:def 2
.=0 by A25,POWER:def 2;
hence thesis by A29;
end;
case
|.a.n+b.n.| <> 0;
then 0 < |.a.n+b.n.| by COMPLEX1:46;
hence |.x.n.| to_power q = |.a.n+b.n.| to_power ((p-1)*q) by A27,
POWER:33
.=ab.n by A3,A18;
end;
end;
hence thesis;
end;
A30: for n be Nat holds (x(#)abs(a)).n= |.a.n*x.n.|
proof
let n be Nat;
0 <= x.n by A10;
then
A31: |.x.n.|=x.n by ABSVALUE:def 1;
thus (x(#)abs(a)).n =x.n * abs(a).n by SEQ_1:8
.=x.n * |.a.n.| by SEQ_1:12
.=|.a.n*x.n.| by A31,COMPLEX1:65;
end;
A32: for n be Nat holds Partial_Sums(ab).n <= ( ((Partial_Sums(ap
).n) to_power (1/p)) + ((Partial_Sums(bp).n) to_power (1/p))) * ( (Partial_Sums
(ab).n) to_power (1/q) )
proof
let n be Nat;
A33: (Partial_Sums(x(#)abs(a)+x(#)abs(b))).n =(Partial_Sums(x(#)abs(a))+
Partial_Sums(x(#)abs(b))).n by SERIES_1:5
.=Partial_Sums(x(#)abs(a)).n+Partial_Sums(x(#)abs(b)).n by SEQ_1:7;
Partial_Sums(x(#)abs(a)).n <= ( (Partial_Sums(ap).n) to_power (1/p) )
* ( ( Partial_Sums(ab).n) to_power (1/q) ) & Partial_Sums(x(#)abs(b)).n <= ( (
Partial_Sums(bp).n) to_power (1/p) ) * ( (Partial_Sums(ab).n) to_power (1/q) )
by A1,A3,A15,A30,A12,A26,Th6;
then
A34: Partial_Sums(x(#)abs(a)).n + Partial_Sums(x(#)abs(b)).n <= ( (
Partial_Sums(ap).n) to_power (1/p) ) * ( (Partial_Sums(ab).n) to_power (1/q) )
+ ( (Partial_Sums(bp).n) to_power (1/p) ) * ( (Partial_Sums(ab).n) to_power (1/
q) ) by XREAL_1:7;
Partial_Sums(ab).n <= Partial_Sums(x(#)abs(a)+x(#)abs(b)).n by A23,
SERIES_1:14;
hence thesis by A33,A34,XXREAL_0:2;
end;
A35: for n be Nat holds 0 <= ab.n
proof
let n be Nat;
0 <= |.a.n+b.n.| by COMPLEX1:46;
then
A36: 0 to_power p <= |.a.n+b.n.| to_power p by A1,Th3;
ab.n=|.a.n+b.n.| to_power p by A3;
hence thesis by A1,A36,POWER:def 2;
end;
now
let n be Nat;
set A=Partial_Sums(ab).n;
set C= ( ((Partial_Sums(ap).n) to_power (1/p)) + ((Partial_Sums(bp).n)
to_power (1/p)));
set D= ( A to_power (1/q) );
A37: 0 <= A by A35,Lm2;
0 <= Partial_Sums(bp).n by A6,Lm2;
then 0 to_power (1/p) <= (Partial_Sums(bp).n) to_power (1/p) by A2,Th3;
then
A38: 0 <= (Partial_Sums(bp).n) to_power (1/p) by A2,POWER:def 2;
0 <= Partial_Sums(ap).n by A4,Lm2;
then 0 to_power (1/p) <= (Partial_Sums(ap).n) to_power (1/p) by A2,Th3;
then 0 <= (Partial_Sums(ap).n) to_power (1/p) by A2,POWER:def 2;
then
A39: 0+0 <= (Partial_Sums(ap).n) to_power (1/p) + (Partial_Sums(bp).n)
to_power (1/p) by A38;
now
per cases;
case
A=0;
hence A to_power (1/p) <= C by A2,A39,POWER:def 2;
end;
case
A40: A<>0;
set B=1/D;
A41: 0 < D by A37,A40,POWER:34;
then
A42: 0 < B by XREAL_1:139;
A43: C*D*B = C* (D *B) .= C*1 by A41,XCMPLX_1:87
.= C;
A *B =A/D by XCMPLX_1:99
.=(A to_power 1) / D by POWER:25
.=A to_power (1-(1/q)) by A37,A40,POWER:29
.= A to_power (1/p) by A14;
hence A to_power (1/p) <= (Partial_Sums(ap).n) to_power (1/p) + (
Partial_Sums(bp).n) to_power (1/p) by A32,A42,A43,XREAL_1:64;
end;
end;
hence (Partial_Sums(ab).n) to_power (1/p) <= (Partial_Sums(ap).n) to_power
(1/p) + (Partial_Sums(bp).n) to_power (1/p);
end;
hence thesis;
end;
theorem Th8:
for a,b be Real_Sequence st (for n be Nat holds a.n <=
b.n ) & b is convergent & a is non-decreasing holds a is convergent & lim a <=
lim b
proof
let a,b be Real_Sequence such that
A1: for n be Nat holds a.n <= b.n and
A2: b is convergent and
A3: a is non-decreasing;
A4: b is bounded by A2;
A5: a is bounded_above
proof
consider r be Real such that
A6: for n be Nat holds b.n < r by A4,SEQ_2:def 3;
now
let n be Nat;
a.n <=b.n by A1;
then a.n <= r by A6,XXREAL_0:2;
then a.n+0 < r+1 by XREAL_1:8;
hence a.n < r+1;
end;
hence thesis by SEQ_2:def 3;
end;
hence a is convergent by A3;
thus thesis by A1,A2,A3,A5,SEQ_2:18;
end;
theorem Th9:
for a,b,c be Real_Sequence st (for n be Nat holds a.n
<= b.n+c.n ) & b is convergent & c is convergent & a is non-decreasing holds a
is convergent & lim a <= lim b + lim c
proof
let a,b,c be Real_Sequence such that
A1: for n be Nat holds a.n <= b.n+c.n and
A2: b is convergent & c is convergent and
A3: a is non-decreasing;
A4: now
let n be Nat;
a.n <=b.n + c.n by A1;
hence a.n <= (b+c).n by SEQ_1:7;
end;
A5: b+c is convergent by A2;
hence a is convergent by A3,A4,Th8;
lim (b+c) = lim b + lim c by A2,SEQ_2:6;
hence thesis by A3,A5,A4,Th8;
end;
theorem Th10:
for p be Real st 0 < p
for a,ap be Real_Sequence st a is
convergent & (for n be Nat holds 0 <=a.n ) &
(for n be Nat holds ap.n=(a.n) to_power p)
holds ap is convergent & lim ap = (lim a) to_power p
proof
let p be Real such that
A1: 0 < p;
let a,ap be Real_Sequence such that
A2: a is convergent and
A3: for n be Nat holds 0 <=a.n and
A4: for n be Nat holds ap.n=(a.n) to_power p;
now
per cases;
case
A5: lim a =0;
now
per cases;
case
ex n be Nat st for m be Nat st n<=m
holds a.m=0;
then consider N be Nat such that
A6: for m be Nat st N<=m holds a.m=0;
A7: for n be Nat holds (a^\N).n=0
proof
let n be Nat;
a.(n+N)=0 by A6,NAT_1:12;
hence thesis by NAT_1:def 3;
end;
A8: now
let e be Real such that
A9: e>0;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A10: (lim a) to_power p = 0 by A1,A5,POWER:def 2;
(ap^\N).m= ap.(m+N) by NAT_1:def 3
.= (a.(m+N)) to_power p by A4
.= ((a^\N).m) to_power p by NAT_1:def 3
.= 0 to_power p by A7
.= 0 by A1,POWER:def 2;
hence |.(ap^\N).m-((lim a) to_power p).| < e by A9,A10,ABSVALUE:2;
end;
then
A11: (ap^\N) is convergent by SEQ_2:def 6;
then ((lim a) to_power p) =lim(ap^\N) by A8,SEQ_2:def 7;
hence thesis by A11,SEQ_4:20,21;
end;
case
A12: for n be Nat ex m be Nat st n<=m & a. m<>0;
defpred P[set] means a.$1 <> 0;
ex m1 be Nat st 0<=m1 & a.m1 <>0 by A12;
then
A13: ex m be Nat st P[m];
consider M be Nat such that
A14: P[M] & for n be Nat st P[n] holds M<=n from NAT_1:sch 5(A13
);
defpred P[set,set,set] means for n,m be Nat st $2=n & $3=
m holds n<m & a.m <>0 & for k be Nat st n<k & a.k <>0 holds m<=k;
A15: (lim a) to_power p =0 by A1,A5,POWER:def 2;
reconsider M as Nat;
A16: now
let n be Nat;
consider m be Nat such that
A17: n+1<=m & a.m <>0 by A12;
take m;
thus n<m & a.m <>0 by A17,NAT_1:13;
end;
A18: for n being Nat, x being Element of NAT
ex y being Element of NAT st P[n,x,y]
proof
let n be Nat, x be Element of NAT;
defpred P[Nat] means x<$1 & a.$1 <>0;
ex m be Nat st P[m] by A16;
then
A19: ex m be Nat st P[m];
consider l be Nat such that
A20: P[l] & for k be Nat st P[k] holds l<=k from NAT_1:sch 5(
A19);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A20;
end;
reconsider zz=0 as Element of NAT;
consider F be sequence of NAT such that
A21: F.0=In(M,NAT) & for n be Nat holds P[n,F.n,F.(n+1)]
from RECDEF_1:sch 2(A18);
rng F c= NAT by RELAT_1:def 19;
then
A22: rng F c= REAL by NUMBERS:19;
dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A22,RELSET_1:4;
for n being Nat holds F.n<F.(n+1) by A21;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A23: for n be Nat st a.n <> 0 ex m be Nat st F .m=n
proof
defpred P[set] means a.$1 <>0 & for m be Nat holds F.m
<>$1;
assume ex n be Nat st P[n];
then
A24: ex n be Nat st P[n];
consider M1 be Nat such that
A25: P[M1] & for n be Nat st P[n] holds M1<=n from NAT_1:sch 5
(A24);
defpred P[Nat] means $1<M1 & a.$1 <> 0 & ex m be Nat st
F.m=$1;
A26: ex n be Nat st P[n]
proof
take M;
M<=M1 & M <> M1 by A14,A21,A25;
hence M<M1 by XXREAL_0:1;
thus a.M <>0 by A14;
take 0;
thus thesis by A21;
end;
A27: for n be Nat st P[n] holds n<=M1;
consider MX be Nat such that
A28: P[MX] & for n be Nat st P[n] holds n<=MX from NAT_1:sch 6
(A27,A26);
A29: for k be Nat st MX<k & k<M1 holds a.k=0
proof
given k be Nat such that
A30: MX<k and
A31: k<M1 & a.k <> 0;
now
per cases;
case
ex m be Nat st F.m=k;
hence contradiction by A28,A30,A31;
end;
case
for m be Nat holds F.m<>k;
hence contradiction by A25,A31;
end;
end;
hence contradiction;
end;
consider m be Nat such that
A32: F.m=MX by A28;
A33: MX<F.(m+1) & a.(F.(m+1))<>0 by A21,A32;
A34: F.(m+1)<=M1 by A21,A25,A28,A32;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A34,XXREAL_0:1;
hence contradiction by A29,A33;
end;
hence contradiction by A25;
end;
A35: a*F is convergent & lim (a*F)=0 by A2,A5,SEQ_4:16,17;
A36: now
let e be Real;
assume
A37: 0<e;
then 0 < (e to_power (1/p) ) by POWER:34;
then consider n be Nat such that
A38: for m be Nat st n<=m holds |.(a*F).m-0.| < (e
to_power (1/p) ) by A35,SEQ_2:def 7;
reconsider k=F.n as Nat;
take k;
let m be Nat such that
A39: k<=m;
now
per cases;
case
a.m=0;
then ap.m= 0 to_power p by A4
.= 0 by A1,POWER:def 2;
hence |.ap.m-((lim a) to_power p).|<e by A15,A37,ABSVALUE:2;
end;
case
A40: a.m<>0;
then consider l be Nat such that
A41: m=F.l by A23;
A42: l in NAT by ORDINAL1:def 12;
n<=l by A39,A41,SEQM_3:1;
then |.(a*F).l-0.|< (e to_power (1/p) ) by A38;
then
A43: |.a.(F.l).|< (e to_power (1/p) ) by FUNCT_2:15,A42;
A44: (a.m) to_power p = ap.m by A4;
A45: a.m > 0 by A3,A40;
then
A46: 0 < ap.m by A44,POWER:34;
|.a.m.| > 0 by A40,COMPLEX1:47;
then |.a.m.| to_power p < (e to_power (1/p) ) to_power p by A1
,A41,A43,POWER:37;
then |.a.m.| to_power p < e to_power ( (1/p) *p ) by A37,
POWER:33;
then |.a.m.| to_power p < e to_power 1 by A1,XCMPLX_1:106;
then |.a.m.| to_power p < e by POWER:25;
then ap.m < e by A45,A44,ABSVALUE:def 1;
hence |.ap.m -((lim a) to_power p).| < e by A15,A46,
ABSVALUE:def 1;
end;
end;
hence |.ap.m -((lim a) to_power p).| < e;
end;
hence ap is convergent by SEQ_2:def 6;
hence lim ap = (lim a) to_power p by A36,SEQ_2:def 7;
end;
end;
hence thesis;
end;
case
A47: lim a <>0;
A48: 0 <= lim a by A2,A3,SEQ_2:17;
ex k be Nat st rng (a^\k) c= dom ( #R p)
proof
set e0=(lim a );
A49: e0/2 > 0 by A47,A48,XREAL_1:215;
then consider k be Nat such that
A50: for m be Nat st k<=m holds |.a.m-e0.|<e0/2 by A2,
SEQ_2:def 7;
take k;
A51: now
let m be Nat;
|.a.(k+m)-e0.|<e0/2 by A50,NAT_1:12;
then -(e0/2) <= a.(k+m)-e0 by ABSVALUE:5;
then -(e0/2)+e0 <= a.(k+m)-e0+e0 by XREAL_1:7;
hence 0 < (a^\k).m by A49,NAT_1:def 3;
end;
let x be object;
assume x in rng (a^\k);
then consider n be Element of NAT such that
A52: x = (a^\k).n by FUNCT_2:113;
0 < (a^\k).n by A51;
then (a^\k).n in {g where g is Real: 0<g};
then (a^\k).n in right_open_halfline(0) by XXREAL_1:230;
hence x in dom ( #R p) by A52,TAYLOR_1:def 4;
end;
then consider k be Nat such that
A53: rng (a^\k) c= dom ( #R p);
now
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
(a^\k).n in rng (a^\k) by VALUED_0:28;
then (a^\k).n in dom ( #R p) by A53;
then
A54: (a^\k).n in right_open_halfline(0) by TAYLOR_1:def 4;
then a.(k+n) in right_open_halfline(0) by NAT_1:def 3;
then a.(k+n) in {g where g is Real: 0<g} by XXREAL_1:230;
then
A55: ex g be Real st a.(k+n) = g & g > 0;
thus (( #R p)/*(a^\k)).x = ( #R p).((a^\k).n) by A53,FUNCT_2:108
.=((a^\k).n) #R p by A54,TAYLOR_1:def 4
.=(a.(k+n)) #R p by NAT_1:def 3
.=(a.(k+n)) to_power p by A55,POWER:def 2
.=ap.(k+n) by A4
.=(ap^\k).x by NAT_1:def 3;
end;
then
A56: ( #R p)/*(a^\k) = ap^\k by FUNCT_2:12;
A57: lim (a^\k) = lim a by A2,SEQ_4:20;
lim a > 0 by A2,A3,A47,SEQ_2:17;
then ( #R p) is_continuous_in lim (a^\k) by A57,FDIFF_1:24,TAYLOR_1:21;
then
A58: ( #R p)/*(a^\k) is convergent & ( #R p).(lim (a^\k)) = lim (( #R p
)/*(a^\k)) by A2,A53,FCONT_1:def 1;
lim a in {g where g is Real: 0<g} by A47,A48;
then lim a in right_open_halfline(0) by XXREAL_1:230;
then ( #R p).(lim (a^\k)) =(lim a) #R p by A57,TAYLOR_1:def 4
.=(lim a) to_power p by A47,A48,POWER:def 2;
hence thesis by A58,A56,SEQ_4:21,22;
end;
end;
hence thesis;
end;
theorem
for p be Real st 0 < p for a,ap be Real_Sequence st a is summable & (
for n be Nat holds 0 <=a.n ) & (for n be Nat holds ap.n=(
Partial_Sums(a).n) to_power p) holds ap is convergent & lim ap = Sum(a)
to_power p & ap is non-decreasing & for n be Nat holds ap.n <= Sum(a
) to_power p
proof
let p be Real such that
A1: 0 < p;
let a,ap be Real_Sequence such that
A2: a is summable and
A3: for n be Nat holds 0 <=a.n and
A4: for n be Nat holds ap.n=(Partial_Sums(a).n) to_power p;
A5: Partial_Sums(a) is convergent & for n be Nat holds 0 <=
Partial_Sums(a).n by A2,A3,Lm2,SERIES_1:def 2;
then lim ap = (lim Partial_Sums(a)) to_power p by A1,A4,Th10;
hence
A6: ap is convergent & lim ap = (Sum(a)) to_power p by A1,A4,A5,Th10,
SERIES_1:def 3;
A7: Partial_Sums(a) is non-decreasing by A3,SERIES_1:16;
now
let n, m be Nat;
assume n <=m;
then
A8: Partial_Sums(a).n <= Partial_Sums(a).m by A7,SEQM_3:6;
A9: ap.n = (Partial_Sums(a).n) to_power p & ap.m = (Partial_Sums(a).m)
to_power p by A4;
0 <= Partial_Sums(a).n by A3,Lm2;
hence ap.n <= ap.m by A1,A9,A8,Th3;
end;
hence
A10: ap is non-decreasing by SEQM_3:6;
thus thesis by A6,A10,SEQ_4:37;
end;
theorem
for p, q be Real st 1 < p & 1/p + 1/q = 1 for a,b,ap,bq,ab be
Real_Sequence st ( for n be Nat holds ap.n=|.a.n.| to_power p & bq.
n=|.b.n.| to_power q & ab.n=|.a.n* b.n.| ) & ap is summable & bq is summable
holds ab is summable & Sum ab <= ( Sum(ap) to_power (1/p) ) * ( Sum(bq)
to_power (1/q) )
proof
let p,q be Real such that
A1: 1 < p and
A2: 1/p + 1/q = 1;
let a,b,ap,bq,ab be Real_Sequence such that
A3: for n be Nat holds ap.n=|.a.n.| to_power p & bq.n=|.b.
n.| to_power q & ab.n=|.a.n* b.n.| and
A4: ap is summable and
A5: bq is summable;
A6: Partial_Sums(ap) is convergent by A4,SERIES_1:def 2;
reconsider pp=1/p as Real;
1/p < 1 by A1,XREAL_1:189;
then
A7: 1-1 < 1-pp by XREAL_1:15;
then
A8: 0 < q by A2;
for n be Nat holds 0 <= bq.n
proof
let n be Nat;
A9: bq.n=|.b.n.| to_power q by A3;
now
per cases by COMPLEX1:46;
case
|.b.n.| = 0;
hence thesis by A8,A9,POWER:def 2;
end;
case
|.b.n.| > 0;
hence thesis by A9,POWER:34;
end;
end;
hence thesis;
end;
then
A10: for n be Nat holds 0 <= Partial_Sums(bq).n by Lm2;
for n be Nat holds 0 <= ab.n
proof
let n be Nat;
ab.n= |.a.n*b.n.| by A3;
hence thesis by COMPLEX1:46;
end;
then
A11: Partial_Sums(ab) is non-decreasing by SERIES_1:16;
deffunc G(Nat)=(Partial_Sums(bq).$1) to_power (1/q);
consider y be Real_Sequence such that
A12: for n be Nat holds y.n=G(n) from SEQ_1:sch 1;
for n be Nat holds 0 <= ap.n
proof
let n be Nat;
A13: ap.n=|.a.n.| to_power p by A3;
now
per cases by COMPLEX1:46;
case
|.a.n.| = 0;
hence thesis by A1,A13,POWER:def 2;
end;
case
|.a.n.| > 0;
hence thesis by A13,POWER:34;
end;
end;
hence thesis;
end;
then
A14: for n be Nat holds 0 <= Partial_Sums(ap).n by Lm2;
deffunc F(Nat)=(Partial_Sums(ap).$1) to_power (1/p);
consider x be Real_Sequence such that
A15: for n be Nat holds x.n=F(n) from SEQ_1:sch 1;
A16: for n be Nat holds Partial_Sums(ab).n <=(x(#)y).n
proof
let n be Nat;
A17: y.n = (Partial_Sums(bq).n) to_power (1/q) by A12;
Partial_Sums(ab).n <= ( (Partial_Sums(ap).n) to_power (1/p) ) * ( (
Partial_Sums(bq).n) to_power (1/q) ) & x.n = (Partial_Sums(ap).n) to_power (1/
p) by A1,A2,A3,A15,Th6;
hence thesis by A17,SEQ_1:8;
end;
A18: 1/p > 0 by A1,XREAL_1:139;
then
A19: x is convergent by A15,A6,A14,Th10;
A20: Partial_Sums(bq) is convergent by A5,SERIES_1:def 2;
then
A21: y is convergent by A2,A7,A12,A10,Th10;
then x(#)y is convergent by A19;
then
A22: Partial_Sums(ab) is convergent & lim Partial_Sums(ab) <= lim (x(#)y) by
A16,A11,Th8;
Sum ap = lim Partial_Sums(ap) by SERIES_1:def 3;
then
A23: lim x= Sum(ap) to_power (1/p) by A18,A15,A6,A14,Th10;
Sum(bq) = lim Partial_Sums(bq) by SERIES_1:def 3;
then lim y= Sum(bq) to_power (1/q) by A2,A7,A12,A20,A10,Th10;
then
lim (x(#)y) = (Sum(ap) to_power (1/p))* (Sum(bq) to_power (1/q)) by A19,A23
,A21,SEQ_2:15;
hence thesis by A22,SERIES_1:def 2,def 3;
end;
theorem
for p be Real st 1 < p for a,b,ap,bp,ab be Real_Sequence st ( for n be
Nat holds ap.n=|.a.n.| to_power p & bp.n=|.b.n.| to_power p & ab.n
=|.a.n+b.n.| to_power p ) & ap is summable & bp is summable holds ab is
summable & Sum(ab) to_power (1/p) <= Sum(ap) to_power (1/p) + Sum(bp) to_power
(1/p)
proof
let p be Real such that
A1: 1 < p;
A2: 1/p > 0 by A1,XREAL_1:139;
let a,b,ap,bp,ab be Real_Sequence such that
A3: for n be Nat holds ap.n=|.a.n.| to_power p & bp.n=|.b.
n.| to_power p & ab.n=|.a.n+ b.n.| to_power p and
A4: ap is summable and
A5: bp is summable;
deffunc H(Nat)=(Partial_Sums(ab).$1) to_power (1/p);
consider z be Real_Sequence such that
A6: for n be Nat holds z.n=H(n) from SEQ_1:sch 1;
A7: for n be Nat holds 0 <= ab.n
proof
let n be Nat;
A8: ab.n=|.a.n +b.n.| to_power p by A3;
per cases by COMPLEX1:46;
suppose
|.a.n+b.n.| = 0;
hence thesis by A1,A8,POWER:def 2;
end;
suppose
|.a.n+b.n.| > 0;
hence thesis by A8,POWER:34;
end;
end;
A9: for n be Nat holds 0 <= z.n
proof
let n be Nat;
A10: z.n=(Partial_Sums(ab).n) to_power (1/p) by A6;
per cases by A7,Lm2;
suppose
Partial_Sums(ab).n = 0;
hence thesis by A2,A10,POWER:def 2;
end;
suppose
Partial_Sums(ab).n > 0;
hence thesis by A10,POWER:34;
end;
end;
A11: Partial_Sums(ab) is non-decreasing by A7,SERIES_1:16;
A12: now
let n,m be Nat;
assume n <= m;
then
A13: Partial_Sums(ab).n <= Partial_Sums(ab).m by A11,SEQM_3:6;
A14: 0 <= (Partial_Sums(ab).m) to_power (1/p)
proof
per cases by A7,Lm2;
suppose
Partial_Sums(ab).m = 0;
hence thesis by A2,POWER:def 2;
end;
suppose
Partial_Sums(ab).m > 0;
hence thesis by POWER:34;
end;
end;
now
per cases;
case
Partial_Sums(ab).n = Partial_Sums(ab).m;
hence (Partial_Sums(ab).n) to_power (1/p) <= (Partial_Sums(ab).m)
to_power (1/p);
end;
case
Partial_Sums(ab).n <> Partial_Sums(ab).m;
then
A15: Partial_Sums(ab).n < Partial_Sums(ab).m by A13,XXREAL_0:1;
now
per cases;
case
Partial_Sums(ab).n =0;
hence (Partial_Sums(ab).n) to_power (1/p) <= (Partial_Sums(ab).m)
to_power (1/p) by A2,A14,POWER:def 2;
end;
case
A16: Partial_Sums(ab).n <> 0;
0 <= Partial_Sums(ab).n by A7,Lm2;
hence (Partial_Sums(ab).n) to_power (1/p) <= (Partial_Sums(ab).m)
to_power (1/p) by A2,A15,A16,POWER:37;
end;
end;
hence (Partial_Sums(ab).n) to_power (1/p) <= (Partial_Sums(ab).m)
to_power (1/p);
end;
end;
hence (Partial_Sums(ab).n) to_power (1/p) <= (Partial_Sums(ab).m) to_power
(1/p);
end;
now
let n,m be Nat;
assume
A17: n <= m;
z.n =(Partial_Sums(ab).n) to_power (1/p) & z.m =(Partial_Sums(ab).m)
to_power (1/p) by A6;
hence z.n <= z.m by A12,A17;
end;
then
A18: z is non-decreasing by SEQM_3:6;
for n be Nat holds 0 <= ap.n
proof
let n be Nat;
A19: ap.n=|.a.n.| to_power p by A3;
now
per cases by COMPLEX1:46;
case
|.a.n.| = 0;
hence thesis by A1,A19,POWER:def 2;
end;
case
|.a.n.| > 0;
hence thesis by A19,POWER:34;
end;
end;
hence thesis;
end;
then
A20: for n be Nat holds 0 <= Partial_Sums(ap).n by Lm2;
deffunc F(Nat)=(Partial_Sums(ap).$1) to_power (1/p);
consider x be Real_Sequence such that
A21: for n be Nat holds x.n=F(n) from SEQ_1:sch 1;
for n be Nat holds 0 <= bp.n
proof
let n be Nat;
A22: bp.n=|.b.n.| to_power p by A3;
now
per cases by COMPLEX1:46;
case
|.b.n.| = 0;
hence thesis by A1,A22,POWER:def 2;
end;
case
|.b.n.| > 0;
hence thesis by A22,POWER:34;
end;
end;
hence thesis;
end;
then
A23: for n be Nat holds 0 <= Partial_Sums(bp).n by Lm2;
deffunc G(Nat)=(Partial_Sums(bp).$1) to_power (1/p);
consider y be Real_Sequence such that
A24: for n be Nat holds y.n=G(n) from SEQ_1:sch 1;
A25: Partial_Sums(bp) is convergent by A5,SERIES_1:def 2;
then
A26: y is convergent by A2,A24,A23,Th10;
A27: Partial_Sums(ap) is convergent by A4,SERIES_1:def 2;
then
A28: x is convergent by A2,A21,A20,Th10;
A29: for n be Nat holds z.n <=x.n + y.n
proof
let n be Nat;
A30: y.n = (Partial_Sums(bp).n) to_power (1/p) by A24;
(Partial_Sums(ab).n) to_power (1/p) <= ( (Partial_Sums(ap).n)
to_power (1/p) ) + ( (Partial_Sums(bp).n) to_power (1/p) ) & x.n = (
Partial_Sums(ap).n) to_power (1/p) by A1,A3,A21,Th7;
hence thesis by A6,A30;
end;
then
A31: z is convergent by A28,A26,A18,Th9;
A32: for n be Nat holds (z.n) to_power p = Partial_Sums(ab).n
proof
let n be Nat;
A33: z.n = (Partial_Sums(ab).n) to_power (1/p) by A6;
now
per cases;
case
A34: Partial_Sums(ab).n =0;
then z.n= 0 by A2,A33,POWER:def 2;
hence thesis by A1,A34,POWER:def 2;
end;
case
A35: Partial_Sums(ab).n <> 0;
0 <= Partial_Sums(ab).n by A7,Lm2;
hence (z.n) to_power p = ( Partial_Sums(ab).n) to_power ((1/p)*p) by
A33,A35,POWER:33
.=( Partial_Sums(ab).n) to_power 1 by A1,XCMPLX_1:106
.= Partial_Sums(ab).n by POWER:25;
end;
end;
hence thesis;
end;
then lim Partial_Sums(ab) = (lim z) to_power p by A1,A9,A31,Th10;
then
A36: Sum(ab)= (lim z) to_power p by SERIES_1:def 3;
A37: Sum(ab) to_power (1/p) = lim z
proof
per cases;
suppose
A38: lim z=0;
hence Sum(ab) to_power (1/p) = 0 to_power (1/p) by A1,A36,POWER:def 2
.= lim z by A2,A38,POWER:def 2;
end;
suppose
lim z <> 0;
then 0 < lim z by A9,A31,SEQ_2:17;
hence (Sum ab) to_power (1/p) = (lim z) to_power ((1/p)*p) by A36,
POWER:33
.= (lim z) to_power 1 by A1,XCMPLX_1:106
.= lim z by POWER:25;
end;
end;
Sum(bp) = lim Partial_Sums(bp) by SERIES_1:def 3;
then
A39: lim y= Sum(bp) to_power (1/p) by A2,A24,A25,A23,Th10;
Sum(ap) = lim Partial_Sums(ap) by SERIES_1:def 3;
then
A40: lim x= Sum(ap) to_power (1/p) by A2,A21,A27,A20,Th10;
Partial_Sums(ab) is convergent by A1,A9,A31,A32,Th10;
hence thesis by A28,A40,A26,A39,A29,A18,A37,Th9,SERIES_1:def 2;
end;