:: On the Partial Product of Series and Related Basic Inequalities
:: by Fuguo Ge and Xiquan Liang
::
:: Received July 6, 2005
:: Copyright (c) 2005-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, XXREAL_0, SUBSET_1, SEQ_1, COMPLEX1, SQUARE_1, NEWTON,
RELAT_1, ARYTM_3, ARYTM_1, CARD_1, POWER, PREPOWER, FUNCT_1, SERIES_1,
VALUED_1, NAT_1, REAL_1, SERIES_3, ABIAN, FUNCT_7;
notations SUBSET_1, ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NEWTON, REAL_1, NAT_1, PREPOWER, COMPLEX1, VALUED_1, SEQ_1,
ABIAN, POWER, SERIES_1, FUNCT_2;
constructors REAL_1, SQUARE_1, NAT_1, NEWTON, PREPOWER, SERIES_1, VALUED_1,
PARTFUN1, RELSET_1, BINOP_2, ABIAN;
registrations NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED,
COMPLEX1, NEWTON, VALUED_1, FUNCT_2, VALUED_0, RELSET_1, ORDINAL1;
requirements REAL, SUBSET, NUMERALS, ARITHM;
equalities SQUARE_1, XCMPLX_0;
theorems XCMPLX_1, SQUARE_1, SIN_COS2, POLYEQ_2, ABSVALUE, NEWTON, POWER,
ASYMPT_1, XREAL_1, PREPOWER, FUNCT_2, SERIES_1, SEQ_1, COMPLEX1,
POLYEQ_1, XXREAL_0, ABIAN;
schemes NAT_1;
begin
reserve a,b,c for positive Real,
m,x,y,z for Real,
n for Nat,
s,s1,s2,s3,s4,s5 for Real_Sequence;
registration
let x;
cluster |.x.| -> non negative;
coherence;
end;
Lm1: x^2=x|^2
proof
x^2=x|^1*x
.=x|^(1+1) by NEWTON:6
.=x|^2;
hence thesis;
end;
Lm2: 2|^3=8
proof
2|^3=2|^(2+1) .=2|^2*2 by NEWTON:6
.=2^2*2 by Lm1
.=8;
hence thesis;
end;
Lm3: 3|^3=27
proof
3|^3=3|^(2+1) .=3|^2*3 by NEWTON:6
.=3^2*3 by Lm1
.=27;
hence thesis;
end;
Lm4: (-x)|^3=-x|^3
proof
3 = 2*1 + 1;
then 3 is odd by ABIAN:1;
hence thesis by POWER:2;
end;
Lm5: (x+y)|^3=x|^3+3*x^2*y+3*x*y^2+y|^3
proof
(x+y)|^3=x|^3+(3*y*x^2+3*y^2*x)+y|^3 by POLYEQ_1:14
.=x|^3+3*x^2*y+3*x*y^2+y|^3;
hence thesis;
end;
Lm6: x|^3+y|^3=(x+y)*(x^2-x*y+y^2)
proof
(x^2-x*y+y^2)*(x+y) =x^2*x+y*x^2-(x*(x*y)+y*(x*y))+(x*y^2+y*y^2+0*y^2)
.=x|^ 3+y*x^2-(x*(x*y)+y*(x*y))+(x*y^2+y*y^2) by POLYEQ_2:4
.=x|^ 3+y*x^2-(x^2*y+y*y*x)+(x*y^2+y|^ 3) by POLYEQ_2:4
.=x|^3+y|^3;
hence thesis;
end;
Lm7: x^2<=y*z implies |.x.| <= sqrt(y*z)
proof
A1: x^2>=0 by XREAL_1:63;
assume x^2<=y*z;
then
A2: sqrt(x^2)<=sqrt(y*z) by A1,SQUARE_1:26;
per cases;
suppose
A3: x>=0;
then x<=sqrt(y*z) by A2,SQUARE_1:22;
hence thesis by A3,ABSVALUE:def 1;
end;
suppose
A4: x<0;
then -x<=sqrt(y*z) by A2,SQUARE_1:23;
hence thesis by A4,ABSVALUE:def 1;
end;
end;
theorem
y>x & x>=0 & m>=0 implies x/y <= (x+m)/(y+m)
proof
assume that
A1: y>x and
A2: x>=0 and
A3: m>=0;
y-x>0 by A1,XREAL_1:50;
then m*(y-x)>=0 by A3;
then (y*(x+m)-x*(m+y))/(y*(y+m))>=0 by A1,A2,A3;
then (x+m)/(y+m)-x/y>=0 by A1,A2,A3,XCMPLX_1:130;
then (x+m)/(y+m)-x/y+x/y>=0+x/y by XREAL_1:6;
hence thesis;
end;
theorem Th2:
(a+b)/2>=sqrt(a*b)
proof
(a+b)/2>=(2*sqrt(a*b))/2 by SIN_COS2:1,XREAL_1:72;
hence thesis;
end;
theorem
b/a+a/b>=2
proof
(a-b)^2>=0 by XREAL_1:63;
then a^2-2*a*b+b^2+2*a*b>=0+2*a*b by XREAL_1:7;
then (a^2+b^2)/(a*b)>=(2*(a*b))/(1*(a*b)) by XREAL_1:72;
then
A1: (a^2+b^2)/(a*b)>=2/1 by XCMPLX_1:91;
b/a+a/b = (b*b)/(a*b)+a/b by XCMPLX_1:91
.= (b*b)/(a*b)+(a*a)/(a*b) by XCMPLX_1:91
.= (b^2+a^2)/(a*b);
hence thesis by A1;
end;
theorem Th4:
((x+y)/2)^2>=x*y
proof
(x-y)^2>=0 by XREAL_1:63;
then x^2-2*x*y+y^2+2*x*y>=0+2*x*y by XREAL_1:7;
then x^2+ y^2+2*x*y>=2*x*y+2*x*y by XREAL_1:7;
then (x+y)^2/(2*2)>=4*(x*y)/4 by XREAL_1:72;
hence thesis;
end;
theorem
(x^2+y^2)/2>=((x+y)/2)^2
proof
(x-y)^2>=0 by XREAL_1:63;
then x^2-2*x*y+y^2+2*x*y>=0+2*x*y by XREAL_1:7;
then x^2+y^2+(x^2+y^2)>=2*x*y+(x^2+y^2) by XREAL_1:7;
then 2*(x^2+y^2)/4>=(x+y)^2/4 by XREAL_1:72;
hence thesis;
end;
theorem Th6:
x^2+y^2>=2*x*y
proof
(x-y)^2>=0 by XREAL_1:63;
then x^2-2*x*y+y^2+2*x*y>=0+2*x*y by XREAL_1:6;
hence thesis;
end;
theorem Th7:
(x^2+y^2)/2>=x*y
proof
(x^2+y^2)/2>=(2*x*y)/2 by Th6,XREAL_1:72;
hence thesis;
end;
theorem Th8: :: CSSPACE2:5
x^2+y^2>=2*|.x.|*|.y.|
proof
A1: x^2>=0 & y^2>=0 by XREAL_1:63;
then x^2+y^2>=2*sqrt(x^2*y^2) by SIN_COS2:1;
then x^2+y^2>=2*(sqrt(x^2)*sqrt(y^2)) by A1,SQUARE_1:29;
then x^2+y^2>=2*(sqrt(|.x.|^2)*sqrt(y^2)) by COMPLEX1:75;
then x^2+y^2>=2*(sqrt(|.x.|^2)*sqrt(|.y.|^2)) by COMPLEX1:75;
then x^2+y^2>=2*(|.x.|*sqrt(|.y.|^2)) by SQUARE_1:22;
then x^2+y^2>=2*(|.x.|*|.y.|) by SQUARE_1:22;
hence thesis;
end;
theorem Th9:
(x+y)^2>=4*x*y
proof
2*((x^2+y^2)/2)>=2*(x*y) by Th7,XREAL_1:64;
then x^2+y^2+2*x*y>=2*x*y+2*x*y by XREAL_1:6;
hence thesis;
end;
theorem Th10:
x^2+y^2+z^2>=x*y+y*z+x*z
proof
x^2+y^2>=2*x*y & y^2+z^2>=2*y*z by Th6;
then
A1: x^2+y^2+(y^2+z^2)>=2*x*y+2*y*z by XREAL_1:7;
z^2+x^2>=2*z*x by Th6;
then (x^2+y^2+(y^2+z^2))+(z^2+x^2)>=(2*x*y+2*y*z)+(2*z*x) by A1,XREAL_1:7;
then 2*(x^2+y^2+z^2)/2>=2*(x*y+y*z+z*x)/2 by XREAL_1:72;
hence thesis;
end;
theorem
(x+y+z)^2>=3*(x*y+y*z+x*z)
proof
x^2+y^2+z^2>=x*y+y*z+x*z by Th10;
then x^2+y^2+z^2+(2*x*y+2*y*z+2*z*x)>=x*y+y*z+x*z+(2*x*y+2*y*z+2*z*x) by
XREAL_1:6;
hence thesis;
end;
theorem Th12:
a|^3+b|^3+c|^3>=3*a*b*c
proof
A1: (a+c)|^3-(3*a^2*c+3*a*c^2)=a|^3+3*a^2*c+3*a*c^2+c|^3-(3*a^2*c+3*a*c^2)
by Lm5;
a*(b^2+c^2)>=a*(2*b*c) & b*(a^2+c^2)>=b*(2*a*c) by Th6,XREAL_1:64;
then
A2: b*(a^2+c^2)+a*(b^2+c^2)>=2*a*b*c+2*a*b*c by XREAL_1:7;
(a+c)^2*(a+c)>=4*a*c*(a+c) by Th9,XREAL_1:64;
then (a+c)|^2*(a+c)>=4*a*c*(a+c) by Lm1;
then
A3: (a+c)|^(2+1)>=4*a*c*(a+c) by NEWTON:6;
(b+c)^2*(b+c)>=4*b*c*(b+c) by Th9,XREAL_1:64;
then (b+c)|^2*(b+c)>=4*b*c*(b+c) by Lm1;
then
A4: (b+c)|^(2+1)>=4*b*c*(b+c) by NEWTON:6;
(a+b)^2*(a+b)>=4*a*b*(a+b) by Th9,XREAL_1:64;
then (a+b)|^2*(a+b)>=4*a*b*(a+b) by Lm1;
then (a+b)|^(2+1)>=4*a*b*(a+b) by NEWTON:6;
then (a+b)|^3+(b+c)|^3>=(4*a^2*b+4*a*b^2)+(4*b^2*c+4*b*c^2) by A4,XREAL_1:7;
then
((a+b)|^3+(b+c)|^3)+(a+c)|^3>=(4*a^2*b+4*a*b^2+4*b^2*c+4*b*c^2) +(4*a^2
*c+4*a*c^2) by A3,XREAL_1:7;
then
A5: (((a+b)|^3)+((b+c)|^3)+((a+c)|^3))+(-3*a^2*b-3*a*b^2-(3*b^2*c)-(3*b* c
^2 ) -(3*a^2*c)-(3*a*c^2))>=((4*a^2*b)+4*a*b^2+4*b^2*c+4*b*c^2+4*a^2*c+4*a*c^2)
+(-3*a^2*b-3*a*b^2-(3*b^2*c)-(3*b*c^2)-(3*a^2*c)-(3*a*c^2)) by XREAL_1:6;
c*(a^2+b^2)>=2*a*b*c by Th6,XREAL_1:64;
then
A6: (b*(a^2+c^2)+a*(b^2+c^2))+(c*(a^2+b^2))>=4*a*b*c+2*a*b*c by A2,XREAL_1:7;
(a+b)|^3-(3*a^2*b+3*a*b^2)=a|^3+3*a^2*b+3*a*b^2+b|^3-(3*a^2*b+3*a*b^2) &
(b+ c)|^3-(3*b^2*c+3*b*c^2)=b|^3+3*b^2*c+3*b*c^2+c|^3-(3*b^2*c+3*b*c^2) by Lm5;
then 2*(a|^3+b|^3+(c|^3))>=6*a*b*c by A1,A5,A6,XXREAL_0:2;
then (2*(a|^3+b|^3+(c|^3)))/2>=(6*a*b*c)/2 by XREAL_1:72;
hence thesis;
end;
theorem Th13:
(a|^3+b|^3+c|^3)/3>=a*b*c
proof
(a|^3+b|^3+c|^3)/3>=(3*a*b*c)/3 by Th12,XREAL_1:72;
hence thesis;
end;
theorem
(a/b)|^3+(b/c)|^3+(c/a)|^3>=b/a+c/b+a/c
proof
A1: 1=(a/a)*1*1 by XCMPLX_1:60
.=(a/a)*(b/b)*1 by XCMPLX_1:60
.=(a/a)*(b/b)*(c/c) by XCMPLX_1:60
.=(a/b)*(b/a)*(c/c)
.=(a/b)*((b/a)*(c/c))
.=(a/b)*((b/c)*(c/a))
.=(a/b)*(b/c)*(c/a);
(c/b)=(c/b)*1 .=(c/b)*(a/a) by XCMPLX_1:60
.=(a/b)*(c/a)*1;
then
A2: (c/b)<=((a/b)|^3+(c/a)|^3+1|^3)/3 by Th13;
(a/c)=(a/c)*1 .=(a/c)*(b/b) by XCMPLX_1:60
.=(a/b)*(b/c)*1;
then
A3: (a/c)<=((a/b)|^3+(b/c)|^3+1|^3)/3 by Th13;
(b/a)=(b/a)*1 .=(b/a)*(c/c) by XCMPLX_1:60
.=(b/c)*(c/a)*1;
then (b/a)<=((b/c)|^3+(c/a)|^3+1|^3)/3 by Th13;
then
(b/a)+(c/b)<=(((b/c)|^3)/3+((c/a)|^3)/3+1/3)+(((a/b)|^3)/3+ ((c/a)|^3)/3
+1/3) by A2,XREAL_1:7;
then
A4: (b/a)+(c/b)+(a/c)<=(b/c)|^3/3+(a/b)|^3/3+2*(c/a)|^3/3+2/3+ (((a/b)|^3)/
3+((b/c)|^3)/3+1/3) by A3,XREAL_1:7;
(a/b)*(b/c)*(c/a)<=((a/b)|^3+(b/c)|^3+(c/a)|^3)/3 by Th13;
then (b/a)+(c/b)+(a/c)+1<=2*(b/c)|^3/3+2*(a/b)|^3/3+2*(c/a)|^3/3+1+ (((a/b)
|^3)/3+((b/c)|^3)/3+((c/a)|^3)/3) by A1,A4,XREAL_1:7;
then (b/a)+(c/b)+(a/c)+1-1<=(b/c)|^3+(a/b)|^3+(c/a)|^3+1-1 by XREAL_1:9;
hence thesis;
end;
theorem Th15:
(a+b+c)>=3*(3-root(a*b*c))
proof
A1: (3 -Root(c))>0 by PREPOWER:def 2;
(3 -Root(a))>0 & (3 -Root(b))>0 by PREPOWER:def 2;
then (3 -Root(a))|^3+(3 -Root(b))|^3+(3 -Root(c))|^3>=3*(3 -Root(a)) *(3
-Root(b))*(3 -Root(c)) by A1,Th12;
then
a+(3 -Root(b))|^3+(3 -Root(c))|^3>=3*(3 -Root(a)) *(3 -Root(b))*(3 -Root
(c)) by PREPOWER:19;
then a+b+(3 -Root(c))|^3>=3*(3 -Root(a))*(3 -Root(b))*(3 -Root(c)) by
PREPOWER:19;
then a+b+c>=3*((3 -Root(a))*(3 -Root(b)))*(3 -Root(c)) by PREPOWER:19;
then a+b+c>=3*(3 -Root(a*b))*(3 -Root(c)) by PREPOWER:22;
then a+b+c>=3*((3 -Root(a*b))*(3 -Root(c)));
then a+b+c>=3*(3 -Root(a*b*c)) by PREPOWER:22;
hence thesis by POWER:def 1;
end;
theorem
(a+b+c)/3>=3-root(a*b*c)
proof
(a+b+c)/3>=(3*(3-root(a*b*c)))/3 by Th15,XREAL_1:72;
hence thesis;
end;
theorem
x+y+z=1 implies x*y+y*z+x*z<=1/3
proof
x^2+y^2>=2*x*y & x^2+z^2>=2*x*z by Th6;
then
A1: (x^2+y^2)+(x^2+z^2)>=2*x*y+2*x*z by XREAL_1:7;
y^2+z^2>=2*y*z by Th6;
then (x^2+y^2+x^2+z^2)+(y^2+z^2)>=2*x*y+2*x*z+2*y*z by A1,XREAL_1:7;
then 2*(x^2+y^2+z^2)/2>=2*(x*y+x*z+y*z)/2 by XREAL_1:72;
then
A2: x^2+y^2+z^2+2*(x*z+y*z+x*y)>=x*y+x*z+y*z+2*(x*z+y*z+x*y)by XREAL_1:7;
assume x+y+z =1;
then 1^2=(x+y)^2+2*(x+y)*z+z^2 by SQUARE_1:4
.=x^2+y^2+z^2+2*(x*z+y*z+x*y);
then 1/3>=3*(x*z+y*z+x*y)/3 by A2,XREAL_1:72;
hence thesis;
end;
theorem Th18:
x+y=1 implies x*y<=1/4
proof
(x-y)^2 >= 0 by XREAL_1:63;
then
A1: x^2-2*x*y+y^2-(x^2+2*x*y+y^2)>=0-(x^2+2*x*y+y^2)by XREAL_1:9;
assume x+y=1;
then 1^2=x^2+2*x*y+y^2 by SQUARE_1:4;
then -4*x*y>=-1 by A1;
then 4*(x*y)<=1 by XREAL_1:24;
then 4*(x*y)/4<=1/4 by XREAL_1:72;
hence thesis;
end;
theorem
x+y=1 implies x^2+y^2>=1/2
proof
(x-y)^2 >= 0 by XREAL_1:63;
then
A1: x^2-2*x*y+y^2+(x^2+2*x*y+y^2) >= 0+(x^2+2*x*y+y^2)by XREAL_1:7;
assume x+y=1;
then 1^2=x^2+2*x*y+y^2 by SQUARE_1:4;
then 2*(x^2+y^2)/2 >= 1/2 by A1,XREAL_1:72;
hence thesis;
end;
theorem
a+b=1 implies (1+1/a)*(1+1/b)>=9
proof
assume
A1: a+b=1;
then 1/(a*b) >= 1/(1/4) by Th18,XREAL_1:85;
then (1/(a*b))*(-2) <= 4*(-2) by XREAL_1:65;
then -(1/(a*b))*2 <= -8;
then (1/(a*b))*2 >= 8 by XREAL_1:24;
then
A2: 1+2*(1/(a*b)) >= 1+8 by XREAL_1:7;
(1+1/a)*(1+1/b)=1*1+1*(1/b)+(1/a)*(1/b)+(1/a)*1
.=1+1/b+1/(a*b)+1/a by XCMPLX_1:102
.=1+(1/b+1/a) +1/(a*b)
.=1+(1*a+b*1)/(a*b)+1/(a*b) by XCMPLX_1:116
.=1+1/(a*b)+1/(a*b) by A1
.=1+2*(1/(a*b));
hence thesis by A2;
end;
theorem
x+y=1 implies x|^3+y|^3>=1/4
proof
assume
A1: x+y=1;
then (x*y)*(-3)>=(1/4)*(-3) by Th18,XREAL_1:65;
then
A2: 1+(x*y)*(-3)>=(1/4)*(-3)+1 by XREAL_1:7;
x|^3 + y|^3=(x+y)*(x^2-x*y+y^2) by Lm6;
then x|^3 + y|^3 = x^2+2*x*y+y^2-3*x*y by A1
.=1^2-3*(x*y) by A1,SQUARE_1:4;
hence thesis by A2;
end;
theorem
a+b=1 implies a|^3+b|^3<1
proof
assume
A1: a+b=1;
A2: 1+(a*b)*(-3)<0+1 by XREAL_1:8;
a|^3 + b|^3=(a+b)*(a^2-a*b+b^2) by Lm6;
then a|^3 + b|^3 = a^2+2*a*b+b^2-3*a*b by A1
.=1^2-3*(a*b) by A1,SQUARE_1:4;
hence thesis by A2;
end;
theorem
a+b=1 implies (a+1/a)*(b+1/b)>=25/4
proof
assume
A1: a+b=1;
then
A2: a*b<=(1/2)^2 by Th4;
then 1-(a*b)>=1-(1/4) by XREAL_1:10;
then (1-(a*b))^2>=(3/4)^2 by SQUARE_1:15;
then 1+(1-(a*b))^2>=1+(9/16) by XREAL_1:6;
then
A3: 4*((1+((1-(a*b))^2)))>=4*(25/16) by XREAL_1:64;
((1-(a*b))^2)>=0 by XREAL_1:63;
then
A4: (1+((1-(a*b))^2)) /(a*b)>=((1+((1-(a*b))^2)))/(1/4) by A2,XREAL_1:118;
a^2+b^2=(a^2+2*a*b+b^2)-2*a*b;
then
A5: a^2+b^2=1^2-2*a*b by A1,SQUARE_1:4;
(a+(1/a))*(b+1/b)=((1+a^2)/a)*(b+1/b) by XCMPLX_1:113
.=((1+a^2)/a)*((1+b^2)/b) by XCMPLX_1:113
.=((1+a^2)*(1+b^2))/(a*b) by XCMPLX_1:76
.=((1+(1^2-2*(a*b)+a^2*b^2)))/(a*b) by A5
.=((1+((1-(a*b))^2)))/(a*b);
hence thesis by A4,A3,XXREAL_0:2;
end;
theorem
for x, a being Real st |.x.|<=a holds x^2<=a^2
proof
let x, a be Real;
assume
A1: |.x.|<=a;
per cases;
suppose
A2: x>=0;
x<=a by A1,ABSVALUE:def 1;
hence thesis by A2,SQUARE_1:15;
end;
suppose
A3: x<0;
then -x<=a by A1,ABSVALUE:def 1;
then (-x)^2<=a^2 by A3,SQUARE_1:15;
hence thesis;
end;
end;
theorem
|.x.|>=a implies x^2>=a^2
proof
assume
A1: |.x.|>=a;
per cases;
suppose
x>=0;
then x>=a by A1,ABSVALUE:def 1;
hence thesis by SQUARE_1:15;
end;
suppose
x<0;
then -x>=a by A1,ABSVALUE:def 1;
then (-x)^2>=a^2 by SQUARE_1:15;
hence thesis;
end;
end;
theorem
|.|.x.|-|.y.|.|<=|.x.|+|.y.|
proof
|.|.x.|-|.y.|.|<=|.x-y.| & |.x-y.|<=|.x.|+|.y.| by COMPLEX1:57,64;
hence thesis by XXREAL_0:2;
end;
theorem
a*b*c = 1 implies (1/a)+(1/b)+(1/c)>=sqrt(a)+sqrt(b)+sqrt(c)
proof
assume
A1: a*b*c =1;
(1/a+1/b)/2>=sqrt((1/a)*(1/b)) by Th2;
then (1/a+1/b)/2>=sqrt(1/(a*b)) by XCMPLX_1:102;
then
A2: (1/a+1/b)/2>=sqrt((1*c)/((a*b)*c)) by XCMPLX_1:91;
(1/c+1/a)/2>=sqrt((1/c)*(1/a)) by Th2;
then (1/c+1/a)/2>=sqrt(1/(c*a)) by XCMPLX_1:102;
then
A3: (1/c+1/a)/2>=sqrt((1*b)/((c*a)*b)) by XCMPLX_1:91;
(1/b+1/c)/2>=sqrt((1/b)*(1/c)) by Th2;
then (1/b+1/c)/2>=sqrt(1/(b*c)) by XCMPLX_1:102;
then (1/b+1/c)/2>=sqrt((1*a)/((b*c)*a)) by XCMPLX_1:91;
then (1/b+1/c)/2+(1/c+1/a)/2>=sqrt(a)+sqrt(b) by A1,A3,XREAL_1:7;
then (1/b+1/c)/2+(1/c+1/a)/2+(1/a+1/b)/2>=sqrt(a)+sqrt(b)+sqrt(c) by A1,A2,
XREAL_1:7;
hence thesis;
end;
theorem
x>0 & y>0 & z<0 & x+y+z=0 implies (x|^2+y|^2+z|^2)|^3>=6*(x|^3+y|^3+z |^3)^2
proof
assume that
A1: x>0 & y>0 and
A2: z<0 and
A3: x+y+z=0;
3 -Root(((x^2*y^2*z^2))/4)>0 by A1,A2,PREPOWER:def 2;
then
A4: 3-root(((x^2*y^2*z^2))/4)>0 by A1,A2,POWER:def 1;
x*(x+y)/2+y*(x+y)/2+x*y>=3*(3-root((x*(x+y)/2)*(y*(x+y)/2)*(x*y))) by A1,Th15
;
then x*(x+y)/2+y*(x+y)/2+x*y>=3*(3-root(((x^2*y^2*((x+y)*(x+y))))/4));
then
A5: x*(x+y)/2+y*(x+y)/2+x*y>=3*(3-root(((x^2*y^2*(-z)^2))/4)) by A3;
(3*(3-root(((x^2*y^2*z^2))/4)))|^3 =3|^3*(3-root(((x^2*y^2*z^2))/4))|^3
by NEWTON:7
.=27*(3 -Root(((x^2*y^2*z^2))/4))|^3 by A1,A2,Lm3,POWER:def 1
.=27*(((x^2*y^2*z^2))/4) by A1,A2,PREPOWER:19;
then (x*(x+y)/2+y*(x+y)/2+x*y)|^3>=27*(((x^2*y^2*z^2))/4) by A5,A4,PREPOWER:9
;
then
A6: 8*(x*(x+y)/2+y*(x+y)/2+x*y)|^3>=8*(27*(((x^2*y^2*z^2))/4)) by XREAL_1:64;
(x^2+y^2)/2>=x*y by Th7;
then (x|^2+y^2)/2>=x*y by Lm1;
then (x|^2+y|^2)/2>=x*y by Lm1;
then (x|^2+x*y)/2+(x*y+y|^2)/2+(x|^2+y|^2)/2>=(x|^2+x*y)/2+(x*y+y|^2)/2+x*y
by XREAL_1:6;
then (x|^2+x*y)/2+(x*y+y|^2)/2+(x|^2+y|^2)/2>=(x^2+x*y)/2+(x*y+y|^2)/2+x*y
by Lm1;
then
(x|^2+x*y)/2+(x*y+y|^2)/2+(x|^2+y|^2)/2>=(x*x+x*y)/2+(x*y+y^2)/2+x*y by Lm1;
then
((x|^2+x*y)/2+(x*y+y|^2)/2+(x|^2+y|^2)/2)|^3>=(x*(x+y)/2+y*(x+y)/2+x*y)
|^3 by A1,PREPOWER:9;
then
8*((x|^2+x*y)/2+(x*y+y|^2)/2+(x|^2+y|^2)/2)|^3>=8*(x*(x+y)/2 +y*(x+y)/2
+x*y)|^3 by XREAL_1:64;
then 8*(x|^2+x*y+y|^2)|^3>=54*(x^2*y^2*z^2) by A6,XXREAL_0:2;
then (2*(x|^2+x*y+y|^2))|^3>=54*(x^2*y^2*z^2) by Lm2,NEWTON:7;
then ((x|^2+2*x*y+y|^2)+x|^2+y|^2)|^3>=54*(x^2*y^2*z^2);
then ((x^2+2*x*y+y|^2)+x|^2+y|^2)|^3>=54*(x^2*y^2*z^2) by Lm1;
then ((x^2+2*x*y+y|^2)+x^2+y|^2)|^3>=54*(x^2*y^2*z^2) by Lm1;
then ((x^2+2*x*y+y^2)+x^2+y|^2)|^3>=54*(x^2*y^2*z^2) by Lm1;
then
A7: ((x^2+2*x*y+y^2)+x^2+y^2)|^3>=54*(x^2*y^2*z^2) by Lm1;
A8: z=-(x+y) by A3;
then z|^3 = -((x+y)|^3) by Lm4
.=-(x|^3+3*x^2*y+3*x*y^2+y|^3) by Lm5;
then (z|^2+x^2+y^2)|^3>=6*(x|^3+y|^3+z|^3)^2 by A8,A7,Lm1;
then (z|^2+x|^2+y^2)|^3>=6*(x|^3+y|^3+z|^3)^2 by Lm1;
then (z|^2+x|^2+y|^2)|^3>=6*(x|^3+y|^3+z|^3)^2 by Lm1;
hence thesis;
end;
theorem
a>=1 implies (a to_power b)+(a to_power c)>=2*(a to_power sqrt(b*c))
proof
A1: (b+c)/2>=(2*sqrt(b*c))/2 by SIN_COS2:1,XREAL_1:72;
set p=a to_power c;
set o=a to_power b;
o>0 & p>0 by POWER:34;
then
(a to_power b)+(a to_power c)>=2*sqrt((a to_power b)*(a to_power c)) by
SIN_COS2:1;
then
(a to_power (b+c))>0 & (a to_power b)+(a to_power c)>=2*(sqrt(a to_power
(b+ c))) by POWER:27,34;
then
(a to_power b)+(a to_power c)>=2*((a to_power (b+c)) to_power (1/2)) by
ASYMPT_1:83;
then
A2: (a to_power b)+(a to_power c)>=2*((a to_power ((1/2)*(b+c)))) by POWER:33;
assume a>=1;
then a #R ((b+c)/2) >= a #R (sqrt(b*c)) by A1,PREPOWER:82;
then a to_power ((b+c)/2) >= a #R (sqrt(b*c)) by POWER:def 2;
then a to_power ((b+c)/2) >= a to_power (sqrt(b*c)) by POWER:def 2;
then 2*(a to_power ((b+c)/2)) >= 2*(a to_power (sqrt(b*c))) by XREAL_1:64;
hence thesis by A2,XXREAL_0:2;
end;
theorem
a>=b & b>=c implies (a to_power a)*(b to_power b)*(c to_power c)>=(a*b
*c) to_power ((a+b+c)/3)
proof
assume that
A1: a>=b and
A2: b>=c;
A3: ((b/c) to_power ((b-c)/3)) =((b/c) #R ((b-c)/3)) by POWER:def 2;
b/c>=1 & b-c>=c-c by A2,XREAL_1:9,181;
then
A4: ((b/c) to_power ((b-c)/3))>=1 by A3,PREPOWER:85;
A5: ( (a/b) to_power ((a-b)/3))=((a/b) #R ((a-b)/3)) by POWER:def 2;
a/b>=1 & a-b>=b-b by A1,XREAL_1:9,181;
then ((a/b) to_power ((a-b)/3))>=1 by A5,PREPOWER:85;
then
A6: ((a/b) to_power ((a-b)/3))*((b/c) to_power ((b-c)/3))>=1*1 by A4,XREAL_1:66
;
a>=c by A1,A2,XXREAL_0:2;
then
A7: a/c>=1 & a-c>=c-c by XREAL_1:9,181;
((a/c) to_power ((a-c)/3))=((a/c) #R ((a-c)/3)) by POWER:def 2;
then ((a/c) to_power ((a-c)/3))>=1 by A7,PREPOWER:85;
then ((a/b) to_power ((a-b)/3))*((b/c) to_power ((b-c)/3))* ((a/c) to_power
((a-c)/3))>=1 by A6,XREAL_1:66;
then ((a to_power ((a-b)/3))/(b to_power ((a-b)/3)))*((b/c) to_power ((b-c)
/3))* ((a/c) to_power ((a-c)/3))>=1 by POWER:31;
then
A8: ((a to_power ((a-b)/3))/(b to_power ((a-b)/3)))*((b to_power ((b-c)/3)
)/ (c to_power ((b-c)/3)))*((a/c) to_power ((a-c)/3))>=1 by POWER:31;
set t=b to_power ((a+b+c)/3);
set s=b to_power b;
set r=c to_power ((a+b+c)/3);
set q=c to_power c;
set p=a to_power ((a+b+c)/3);
set o=a to_power a;
set j=c to_power ((a-c)/3);
set i=a to_power ((a-c)/3);
set h=c to_power ((b-c)/3);
set w=b to_power ((b-c)/3);
set v=b to_power ((a-b)/3);
set u=a to_power ((a-b)/3);
A9: p>0 & r>0 by POWER:34;
A10: t>0 by POWER:34;
((a to_power ((a-b)/3))/(b to_power ((a-b)/3)))*((b to_power ((b-c)/3))
/ (c to_power ((b-c)/3)))*((a to_power ((a-c)/3))/(c to_power ((a-c)/3))) =(u*w
)/(v*h)*(i/j) by XCMPLX_1:76
.=(u*w*i)/(v*h*j) by XCMPLX_1:76
.=((a to_power ((a-b)/3))*(a to_power ((a-c)/3))*(b to_power ((b-c)/3)))
/ ((b to_power ((a-b)/3))*(c to_power ((a-c)/3))*(c to_power ((b-c)/3)))
.=((a to_power (((a-b)/3)+((a-c)/3)))*(b to_power ((b-c)/3)))/ ((b
to_power ((a-b)/3))*(c to_power ((a-c)/3))*(c to_power ((b-c)/3))) by POWER:27
.=((a to_power ((2*a-b-c)/3))*(b to_power ((b-c)/3)))/ ((b to_power ((a-
b)/3))*((c to_power ((a-c)/3))*(c to_power ((b-c)/3))))
.=((a to_power ((2*a-b-c)/3))*(b to_power ((b-c)/3)))/ ((b to_power ((a-
b)/3))*((c to_power (((a-c)/3)+((b-c)/3))))) by POWER:27
.=((a to_power ((2*a-b-c)/3))/(c to_power ((a+b-2*c)/3)))* ((b to_power
((b-c)/3))/(b to_power ((a-b)/3))) by XCMPLX_1:76
.=((a to_power ((2*a-b-c)/3))/(c to_power ((a+b-2*c)/3)))* (b to_power (
(b-c)/3-(a-b)/3)) by POWER:29
.=(1/(c to_power ((a+b-2*c)/3)))* (b to_power ((2*b-a-c)/3))*(a to_power
((2*a-b-c)/3))
.=(c to_power (-((a+b-2*c)/3)))* (b to_power ((2*b-a-c)/3))*(a to_power
((2*a-b-c)/3)) by POWER:28
.=(a to_power ((3*a)/3-(a+b+c)/3))*(c to_power ((3*c)/3-(a+b+c)/3))* (b
to_power ((3*b)/3-(a+b+c)/3))
.=((a to_power ((3*a)/3))/(a to_power ((a+b+c)/3))) *(c to_power ((3*c)/
3-(a+b+c)/3))* (b to_power ((3*b)/3-(a+b+c)/3)) by POWER:29
.=((a to_power ((3*a)/3))/(a to_power ((a+b+c)/3))) *((c to_power ((3*c)
/3))/(c to_power ((a+b+c)/3)))* (b to_power ((3*b)/3-(a+b+c)/3)) by POWER:29
.=((a to_power a)/(a to_power ((a+b+c)/3)))* ((c to_power c)/(c to_power
((a+b+c)/3)))* ((b to_power b)/(b to_power ((a+b+c)/3))) by POWER:29
.=(o*q)/(p*r)*(s/t) by XCMPLX_1:76
.=((a to_power a)*(c to_power c)*(b to_power b))/((a to_power ((a+b+c)/3
)) *(c to_power ((a+b+c)/3))*(b to_power ((a+b+c)/3))) by XCMPLX_1:76;
then (o*q*s)/(p*r*t)>=1 by A8,POWER:31;
then (o*q*s)/(p*r*t)*(p*r*t)>=1*(p*r*t) by A9,A10,XREAL_1:64;
then ((a to_power a)*(c to_power c)*(b to_power b))>=((a to_power ((a+b+c)/
3)) *(c to_power ((a+b+c)/3))*(b to_power ((a+b+c)/3))) by A9,A10,XCMPLX_1:87
;
then
(a to_power a)*(c to_power c)*(b to_power b)>= ((a*c) to_power ((a+b+c)
/3))*(b to_power ((a+b+c)/3)) by POWER:30;
then
(a to_power a)*((b to_power b)*(c to_power c))>=(a*c*b) to_power ((a+b+
c)/3) by POWER:30;
hence thesis;
end;
theorem Th31:
for a,b being non negative Real holds (a+b)|^(n+2)>=a|^
(n+2)+(n+2)*(a|^(n+1))*b
proof
let a,b be non negative Real;
defpred X[Nat] means (a+b)|^($1+2)>=a|^($1+2)+($1+2)*(a|^($1+1))*
b;
A1: for n st X[n] holds X[n+1]
proof
let n;
a|^(n+1)>=0
proof
per cases;
suppose
a=0;
hence thesis;
end;
suppose
a>0;
hence thesis by PREPOWER:6;
end;
end;
then
A2: a|^(n+3)+(n+3)*(a|^(n+2))*b<=(n+2)*(a|^(n+1))*(b^2)+ (a|^(n+3)+(n+3)*
(a|^(n+2))*b) by XREAL_1:31;
assume (a+b)|^(n+2)>=a|^(n+2)+(n+2)*(a|^(n+1))*b;
then (a+b)|^(n+2)*(a+b)>=(a|^(n+2)+(n+2)*(a|^(n+1))*b)*(a+b) by XREAL_1:64;
then (a+b)|^(n+2+1)>=(a|^(n+2)+(n+2)*(a|^(n+1))*b)*(a+b) by NEWTON:6;
then (a+b)|^(n+3)>=a|^(n+2)*a+b*a|^(n+2)+(n+2)*(a+b)*(a|^(n+1))*b;
then (a+b)|^(n+3)>=a|^(n+2+1)+b*a|^(n+2)+(n+2)*(a+b)*(a|^(n+1))*b by
NEWTON:6;
then
(a+b)|^(n+3)>=a|^(n+3)+a|^(n+2)*b+(n+2)*(a*(a|^(n+1)))*b+ (n+2)*(a|^(
n+1))*(b*b);
then
(a+b)|^(n+3)>=a|^(n+3)+a|^(n+2)*b+(n+2)*((a|^(n+1+1)))*b+ (n+2)*(a|^(
n+1))*(b*b) by NEWTON:6;
hence thesis by A2,XXREAL_0:2;
end;
A3: a|^(0+2)+(0+2)*a|^(0+1)*b = a^2+2*a|^1*b by Lm1
.=a^2+2*a*b;
(a+b)|^(0+2) = (a+b)^2 by Lm1
.=a^2+2*a*b+b^2;
then
A4: X[0] by A3,XREAL_1:31;
for n holds X[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem
(a|^n+b|^n)/2 >= ((a+b)/2)|^n
proof
defpred X[Nat] means (a|^$1+b|^$1)/2 >= ((a+b)/2)|^$1;
A1: for n st X[n] holds X[n+1]
proof
let n;
assume X[n];
then
A2: ((a|^n+b|^n)/2)*(a+b)>= (((a+b)/2)|^n)*(a+b) by XREAL_1:64;
per cases;
suppose
A3: a-b>=0;
then a-b+b>=0+b by XREAL_1:6;
then a|^n >= b|^n by PREPOWER:9;
then a|^n-b|^n>=0 by XREAL_1:48;
then (a-b)*(a|^n-b|^n)>=0 by A3;
then a|^n*a-a|^n*b-(b|^n*a-b|^n*b)>=0;
then a|^(n+1)-a|^n*b-(b|^n*a-b|^n*b)>=0 by NEWTON:6;
then a|^(n+1)-a|^n*b-b|^n*a+b|^n*b>=0;
then a|^(n+1)-a|^n*b-b|^n*a+b|^(n+1)>=0 by NEWTON:6;
then a|^(n+1)-a|^n*b-b|^n*a+b|^(n+1)+(a|^n*b+b|^n*a)>=0+(a|^n*b+b|^n*a)
by XREAL_1:6;
then
a|^(n+1)+b|^(n+1)+(a|^(n+1)+b|^(n+1))>=a|^n*b+b|^n*a+(a|^(n+1)+b|^(
n+ 1)) by XREAL_1:6;
then 2*a|^(n+1)+2*b|^(n+1)>=a|^(n+1)+a|^n*b+b|^n*a+b|^(n+1);
then 2*a|^(n+1)+2*b|^(n+1)>=a|^n*a+a|^n*b+b|^n*a+b|^(n+1) by NEWTON:6;
then 2*a|^(n+1)+2*b|^(n+1)>=a|^n*a+a|^n*b+b|^n*a+b|^n*b by NEWTON:6;
then (2*(a|^(n+1)+b|^(n+1)))/2>=((a|^n+b|^n)*(a+b))/2 by XREAL_1:72;
then (a|^(n+1)+b|^(n+1))>=(((a+b)/2)|^n)*(a+b) by A2,XXREAL_0:2;
then (a|^(n+1)+b|^(n+1))>=((a+b)|^n/2|^n)*(a+b) by PREPOWER:8;
then (a|^(n+1)+b|^(n+1))>=((a+b)|^n*(a+b))/2|^n;
then (a|^(n+1)+b|^(n+1))>=((a+b)|^(n+1))/2|^n by NEWTON:6;
then (a|^(n+1)+b|^(n+1)) /2>=(((a+b)|^(n+1))/2|^n)/2 by XREAL_1:72;
then (a|^(n+1)+b|^(n+1)) /2>=((a+b)|^(n+1))/(2|^n*2) by XCMPLX_1:78;
then (a|^(n+1)+b|^(n+1)) /2>=((a+b)|^(n+1))/(2|^(n+1)) by NEWTON:6;
hence thesis by PREPOWER:8;
end;
suppose
A4: a-b<0;
then a-b+b<0+b by XREAL_1:6;
then a|^n <= b|^n by PREPOWER:9;
then a|^n-b|^n<=0 by XREAL_1:47;
then (a-b)*(a|^n-b|^n)>=0 by A4;
then a|^n*a-a|^n*b-(b|^n*a-b|^n*b)>=0;
then a|^(n+1)-a|^n*b-(b|^n*a-b|^n*b)>=0 by NEWTON:6;
then a|^(n+1)-a|^n*b-b|^n*a+b|^n*b>=0;
then a|^(n+1)-a|^n*b-b|^n*a+b|^(n+1)>=0 by NEWTON:6;
then a|^(n+1)-a|^n*b-b|^n*a+b|^(n+1)+(a|^n*b+b|^n*a)>=0+(a|^n*b+b|^n*a)
by XREAL_1:6;
then
a|^(n+1)+b|^(n+1)+(a|^(n+1)+b|^(n+1))>=a|^n*b+b|^n*a+(a|^(n+1)+b|^(
n+ 1)) by XREAL_1:6;
then 2*a|^(n+1)+2*b|^(n+1)>=a|^(n+1)+a|^n*b+b|^n*a+b|^(n+1);
then 2*a|^(n+1)+2*b|^(n+1)>=a|^n*a+a|^n*b+b|^n*a+b|^(n+1) by NEWTON:6;
then 2*a|^(n+1)+2*b|^(n+1)>=a|^n*a+a|^n*b+b|^n*a+b|^n*b by NEWTON:6;
then (2*(a|^(n+1)+b|^(n+1)))/2>=((a|^n+b|^n)*(a+b))/2 by XREAL_1:72;
then (a|^(n+1)+b|^(n+1))>=(((a+b)/2)|^n)*(a+b) by A2,XXREAL_0:2;
then (a|^(n+1)+b|^(n+1))>=((a+b)|^n/2|^n)*(a+b) by PREPOWER:8;
then (a|^(n+1)+b|^(n+1))>=((a+b)|^n*(a+b))/2|^n;
then (a|^(n+1)+b|^(n+1))>=((a+b)|^(n+1))/2|^n by NEWTON:6;
then (a|^(n+1)+b|^(n+1)) /2>=(((a+b)|^(n+1))/2|^n)/2 by XREAL_1:72;
then (a|^(n+1)+b|^(n+1)) /2>=((a+b)|^(n+1))/(2|^n*2) by XCMPLX_1:78;
then (a|^(n+1)+b|^(n+1)) /2>=((a+b)|^(n+1))/(2|^(n+1)) by NEWTON:6;
hence thesis by PREPOWER:8;
end;
end;
(a|^0+b|^0)/2 = (1+b|^0)/2 by NEWTON:4
.= (1+1)/2 by NEWTON:4
.= ((a+b)/2)|^0 by NEWTON:4;
then
A5: X[0];
for n holds X[n] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th33:
(for n holds s.n>0) implies for n holds (Partial_Sums s).n>0
proof
defpred X[Nat] means (Partial_Sums s).$1>0;
assume
A1: for n holds s.n>0;
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: (Partial_Sums s).(n+1)=(Partial_Sums s).n+s.(n+1) by SERIES_1:def 1;
assume (Partial_Sums s).n>0;
hence thesis by A1,A3,XREAL_1:34;
end;
(Partial_Sums s).0=s.0 by SERIES_1:def 1;
then
A4: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th34:
(for n holds s.n>=0) implies for n holds (Partial_Sums s).n>=0
proof
defpred X[Nat] means (Partial_Sums(s)).$1>=0;
assume
A1: for n holds s.n>=0;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: (Partial_Sums(s)).n>=0;
(Partial_Sums(s)).(n+1)=(Partial_Sums(s)).n+s.(n+1) & s.(n+1)>=0 by A1,
SERIES_1:def 1;
hence thesis by A3;
end;
(Partial_Sums(s)).0=s.0 by SERIES_1:def 1;
then
A4: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th35:
(for n holds s.n<0) implies (Partial_Sums s).n<0
proof
defpred X[Nat] means (Partial_Sums(s)).$1<0;
assume
A1: for n holds s.n<0;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: (Partial_Sums(s)).n<0;
(Partial_Sums(s)).(n+1)=(Partial_Sums(s)).n+s.(n+1) & s.(n+1)<0 by A1,
SERIES_1:def 1;
hence thesis by A3;
end;
(Partial_Sums(s)).0=s.0 by SERIES_1:def 1;
then
A4: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th36:
s=s1(#)s1 implies for n holds (Partial_Sums s).n>=0
proof
defpred X[Nat] means (Partial_Sums s).$1>=0;
assume
A1: s=s1(#)s1;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: (Partial_Sums(s)).n>=0;
A4: (s1.(n+1))^2>=0 by XREAL_1:63;
(Partial_Sums s).(n+1)=(Partial_Sums(s)).n+s.(n+1) by SERIES_1:def 1
.=(Partial_Sums s).n+(s1.(n+1))^2 by A1,SEQ_1:8;
hence thesis by A3,A4;
end;
(Partial_Sums s).0=s.0 by SERIES_1:def 1
.=(s1.0)^2 by A1,SEQ_1:8;
then
A5: X[0] by XREAL_1:63;
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem
(for n holds s.n>0 & s.n>s.(n-1)) implies (n+1)*s.(n+1) > ( Partial_Sums s).n
proof
defpred X[Nat] means ($1+1)*s.($1+1)>(Partial_Sums s).$1;
assume
A1: for n holds s.n>0 & s.n>s.(n-1);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume (n+1)*s.(n+1)>(Partial_Sums s).n;
then
A3: (Partial_Sums(s)).n+s.(n+1)<(n+1)*s.(n+1)+s.(n+1) by XREAL_1:6;
s.(n+2)>s.((n+2)-1) by A1;
then (n+2)*s.(n+2)>(n+2)*s.(n+1) by XREAL_1:68;
then (Partial_Sums s).n+s.(n+1)<(n+2)*s.(n+2) by A3,XXREAL_0:2;
hence thesis by SERIES_1:def 1;
end;
s.1>s.(1-1) by A1;
then
A4: X[0] by SERIES_1:def 1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th38:
(for n holds s.n>0 & s.n>=s.(n-1)) implies (n+1)*s.(n+1) >= (
Partial_Sums s).n
proof
defpred X[Nat] means ($1+1)*s.($1+1)>=(Partial_Sums s).$1;
assume
A1: for n holds s.n>0 & s.n>=s.(n-1);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume (n+1)*s.(n+1)>=(Partial_Sums s).n;
then
A3: (Partial_Sums(s)).n+s.(n+1)<=(n+1)*s.(n+1)+s.(n+1) by XREAL_1:6;
s.(n+2)>=s.((n+2)-1) by A1;
then (n+2)*s.(n+2)>=(n+2)*s.(n+1) by XREAL_1:64;
then (Partial_Sums s).n+s.(n+1)<=(n+2)*s.(n+2) by A3,XXREAL_0:2;
hence thesis by SERIES_1:def 1;
end;
s.1>=s.(1-1) by A1;
then
A4: X[0] by SERIES_1:def 1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
(s=s1(#)s2 & for n holds s1.n>=0 & s2.n>=0) implies for n holds (
Partial_Sums s).n<= (Partial_Sums(s1).n)*(Partial_Sums(s2).n)
proof
assume that
A1: s=s1(#)s2 and
A2: for n holds s1.n>=0 & s2.n>=0;
defpred X[Nat] means (Partial_Sums(s)).$1<= (Partial_Sums(s1).$1)
*(Partial_Sums(s2).$1);
A3: for n st X[n] holds X[n+1]
proof
let n;
set j=(Partial_Sums(s)).n;
set u=Partial_Sums(s1).n;
set v=Partial_Sums(s2).n;
set w=s1.(n+1);
set h=s2.(n+1);
A4: (Partial_Sums(s1).(n+1))*(Partial_Sums(s2).(n+1)) =(Partial_Sums(s1).n
+s1.(n+1))*(Partial_Sums(s2).(n+1)) by SERIES_1:def 1
.=(u+w)*(v+h) by SERIES_1:def 1
.=u*v+u*h+w*v+w*h;
assume (Partial_Sums(s)).n<= (Partial_Sums(s1).n)*(Partial_Sums(s2).n);
then
A5: j+w*h<=u*v+w*h by XREAL_1:6;
A6: w>=0 & h>=0 by A2;
u>=0 & v>=0 by A2,Th34;
then
A7: (u*v+w*h)<=(u*v+w*h)+(u*h+w*v) by A6,XREAL_1:31;
(Partial_Sums(s)).(n+1) =(Partial_Sums(s)).n+s.(n+1) by SERIES_1:def 1
.=(Partial_Sums(s)).n+s1.(n+1)*s2.(n+1) by A1,SEQ_1:8;
hence thesis by A4,A5,A7,XXREAL_0:2;
end;
A8: (Partial_Sums(s1).0)*(Partial_Sums(s2).0) =s1.0*(Partial_Sums(s2).0) by
SERIES_1:def 1
.=s1.0*s2.0 by SERIES_1:def 1;
(Partial_Sums(s)).0 = s.0 by SERIES_1:def 1
.=s1.0*s2.0 by A1,SEQ_1:8;
then
A9: X[0] by A8;
for n holds X[n] from NAT_1:sch 2(A9,A3);
hence thesis;
end;
theorem
(s=s1(#)s2 & for n holds s1.n<0 & s2.n<0) implies (Partial_Sums s).n<=
(Partial_Sums(s1).n)*(Partial_Sums(s2).n)
proof
assume that
A1: s=s1(#)s2 and
A2: for n holds s1.n<0 & s2.n<0;
defpred X[Nat] means (Partial_Sums s).$1<= (Partial_Sums(s1).$1)*
(Partial_Sums(s2).$1);
A3: for n st X[n] holds X[n+1]
proof
let n;
set j=(Partial_Sums(s)).n;
set u=Partial_Sums(s1).n;
set v=Partial_Sums(s2).n;
set w=s1.(n+1);
set h=s2.(n+1);
A4: (Partial_Sums(s1).(n+1))*(Partial_Sums(s2).(n+1)) =(Partial_Sums(s1).n
+s1.(n+1))*(Partial_Sums(s2).(n+1)) by SERIES_1:def 1
.=(u+w)*(v+h) by SERIES_1:def 1
.=u*v+u*h+w*v+w*h;
assume (Partial_Sums(s)).n<= (Partial_Sums(s1).n)*(Partial_Sums(s2).n);
then
A5: j+w*h<=u*v+w*h by XREAL_1:6;
A6: w<0 & h<0 by A2;
u<0 & v<0 by A2,Th35;
then
A7: (u*v+w*h)<=(u*v+w*h)+(u*h+w*v) by A6,XREAL_1:31;
(Partial_Sums(s)).(n+1) =(Partial_Sums(s)).n+s.(n+1) by SERIES_1:def 1
.=(Partial_Sums(s)).n+s1.(n+1)*s2.(n+1) by A1,SEQ_1:8;
hence thesis by A4,A5,A7,XXREAL_0:2;
end;
A8: (Partial_Sums(s1).0)*(Partial_Sums(s2).0) =s1.0*(Partial_Sums(s2).0) by
SERIES_1:def 1
.=s1.0*s2.0 by SERIES_1:def 1;
(Partial_Sums s).0 = s.0 by SERIES_1:def 1
.=s1.0*s2.0 by A1,SEQ_1:8;
then
A9: X[0] by A8;
for n holds X[n] from NAT_1:sch 2(A9,A3);
hence thesis;
end;
theorem Th41:
for n holds |.(Partial_Sums s).n.|<=(Partial_Sums (abs s)).n
proof
set s1=abs s;
defpred X[Nat] means |.(Partial_Sums s).$1.|<=(Partial_Sums s1).
$1;
let n;
A1: for n st X[n] holds X[n+1]
proof
let n;
assume |.(Partial_Sums(s)).n.|<=(Partial_Sums(s1)).n;
then
A2: |.(Partial_Sums(s)).n.|+|.s.(n+1).|<=(Partial_Sums(s1)).n + |.s.(
n+1).| by XREAL_1:6;
(Partial_Sums(s1)).(n+1)=(Partial_Sums(s1)).n + s1.(n+1) by SERIES_1:def 1;
then
A3: (Partial_Sums(s1)).(n+1)=(Partial_Sums(s1)).n + |.s.(n+1).| by SEQ_1:12;
|.(Partial_Sums(s)).(n+1).|=|.(Partial_Sums(s)).n + s.(n+1).| & |.
( Partial_Sums(s)).n + s.(n+1).|<=|.(Partial_Sums(s)).n.| + |.s.(n+1).|
by COMPLEX1:56,SERIES_1:def 1;
hence thesis by A3,A2,XXREAL_0:2;
end;
s1.0=|.s.0.| by SEQ_1:12;
then (Partial_Sums s1).0=|.s.0.| by SERIES_1:def 1;
then
A4: X[0] by SERIES_1:def 1;
for n holds X[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem
(Partial_Sums s).n<=(Partial_Sums abs s).n
proof
set s1=abs s;
(Partial_Sums s).n<=|.(Partial_Sums s).n.| & |.(Partial_Sums s).n.|<=(
Partial_Sums s1).n by Th41,ABSVALUE:4;
hence thesis by XXREAL_0:2;
end;
definition
let s;
func Partial_Product(s) -> Real_Sequence means
:Def1:
it.0=s.0 & for n holds it.(n+1) = it.n * s.(n+1);
existence
proof
deffunc U(Nat,Real) = In($2 * s.($1+1),REAL);
consider f being sequence of REAL such that
A1: f.0 = s.0 & for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:
sch 12;
reconsider f as Real_Sequence;
take f;
thus f.0 = s.0 by A1;
let n be Nat;
f.(n+1) = U(n,f.n) by A1;
hence thesis;
end;
uniqueness
proof
let s1,s2;
assume that
A2: s1.0=s.0 and
A3: for n holds s1.(n+1)=s1.n * s.(n+1) and
A4: s2.0=s.0 and
A5: for n holds s2.(n+1)=s2.n * s.(n+1);
defpred X[Nat] means s1.$1=s2.$1;
A6: for n st X[n] holds X[n+1]
proof
let n;
assume s1.n =s2.n;
hence s1.(n+1)=s2.n * s.(n+1) by A3
.=s2.(n+1) by A5;
end;
A7: X[0] by A2,A4;
for n holds X[n] from NAT_1:sch 2(A7,A6);
then for n being Element of NAT holds X[n];
hence s1=s2 by FUNCT_2:63;
end;
end;
theorem Th43:
(for n holds s.n>0) implies (Partial_Product s).n>0
proof
defpred X[Nat] means (Partial_Product s).$1>0;
assume
A1: for n holds s.n>0;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: (Partial_Product s).n>0;
(Partial_Product s).(n+1) = (Partial_Product s).n*s.(n+1) & s.(n+1)>0
by A1,Def1;
hence thesis by A3;
end;
s.0>0 by A1;
then
A4: X[0] by Def1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th44:
(for n holds s.n>=0) implies (Partial_Product s).n>=0
proof
defpred X[Nat] means (Partial_Product s).$1>=0;
assume
A1: for n holds s.n>=0;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: (Partial_Product s).n>=0;
(Partial_Product s).(n+1) = (Partial_Product s).n*s.(n+1) & s.(n+1)>=0
by A1,Def1;
hence thesis by A3;
end;
s.0>=0 by A1;
then
A4: X[0] by Def1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
(for n holds s.n>0 & s.n<1) implies for n holds (Partial_Product s).n>
0 & (Partial_Product s).n<1
proof
defpred X[Nat] means (Partial_Product s).$1>0 & (Partial_Product
s).$1<1;
assume
A1: for n holds s.n>0 & s.n<1;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: (Partial_Product s).n>0 & (Partial_Product s).n<1;
(Partial_Product s).(n+1)=((Partial_Product s).n)*(s.(n+1)) & s.(n+1)>
0 by A1,Def1;
hence thesis by A1,A3,XREAL_1:162;
end;
(Partial_Product s).0=s.0 by Def1;
then
A4: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
(for n holds s.n>=1) implies for n holds (Partial_Product s).n>=1
proof
defpred X[Nat] means (Partial_Product s).$1>=1;
assume
A1: for n holds s.n>=1;
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: (Partial_Product s).(n+1)=((Partial_Product s).n)*(s.(n+1)) by Def1;
assume
A4: (Partial_Product s).n>=1;
then ((Partial_Product s).n)<=((Partial_Product s).n)*(s.(n+1)) by A1,
XREAL_1:151;
hence thesis by A4,A3,XXREAL_0:2;
end;
(Partial_Product s).0=s.0 by Def1;
then
A5: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem
(for n holds s1.n>=0 & s2.n>=0) implies for n holds (Partial_Product
s1).n+(Partial_Product s2).n<= (Partial_Product(s1+s2)).n
proof
set s=s1+s2;
defpred X[Nat] means (Partial_Product s1).$1+ (Partial_Product s2
).$1<=(Partial_Product s).$1;
A1: (Partial_Product s).0 = s.0 by Def1
.=s1.0+s2.0 by SEQ_1:7;
assume
A2: for n holds s1.n>=0 & s2.n>=0;
A3: for n st X[n] holds X[n+1]
proof
let n;
set u=(Partial_Product s1).n;
set v=(Partial_Product s2).n;
set w=(Partial_Product s).n;
set h=s1.(n+1);
set j=s2.(n+1);
A4: h>=0 & j>=0 by A2;
u>=0 & v>=0 by A2,Th44;
then
A5: u*h+v*j<=(u*h+v*j)+(u*j+v*h) by A4,XREAL_1:31;
A6: (Partial_Product s).(n+1) =(Partial_Product s).n*s.(n+1) by Def1
.=w*(h+j) by SEQ_1:7;
assume
(Partial_Product s1).n+(Partial_Product s2).n<= (Partial_Product s ).n;
then
A7: (u+v)*(h+j)<=w*(h+j) by A4,XREAL_1:64;
(Partial_Product s1).(n+1)+(Partial_Product s2).(n+1) =(
Partial_Product s1).n*s1.(n+1)+(Partial_Product s2).(n+1) by Def1
.=u*h+v*j by Def1;
hence thesis by A7,A6,A5,XXREAL_0:2;
end;
(Partial_Product s1).0+(Partial_Product s2).0 =s1.0+(Partial_Product s2)
.0 by Def1
.=s1.0+s2.0 by Def1;
then
A8: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A8,A3);
hence thesis;
end;
theorem
(for n holds s.n=(2*n+1)/(2*n+2)) implies (Partial_Product s).n<=1/
sqrt(3*n+4)
proof
defpred X[Nat] means (Partial_Product s).$1<=1/sqrt(3*$1+4);
assume
A1: for n holds s.n=(2*n+1)/(2*n+2);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume (Partial_Product s).n<=1/sqrt(3*n+4);
then
(Partial_Product s).n*((2*n+3)/(2*n+4))<=1/sqrt(3*n+4)*((2*n+3)/(2*n+
4 )) by XREAL_1:64;
then
A3: (Partial_Product s).n*((2*n+3)/(2*n+4))<=(1*(2*n+3))/(sqrt(3*n+4)* (2*
n+ 4)) by XCMPLX_1:76;
111*n<=112*n by XREAL_1:64;
then 111*n+63<=112*n+64 by XREAL_1:7;
then (12*n|^3+64*n^2)+(111*n+63)<=(12*n|^3+64*n^2)+(112*n+64) by XREAL_1:6;
then
12*n|^(2+1)+36*(n*n)+27*n+28*n^2+84*n+63<=12*n|^(2+1)+48*n^2+48*n+16*
n ^2 +64*n+64;
then
12*((n|^2)*(n|^1))+36*(n*n)+27*n+28*n^2+84*n+63<=12*n|^(2+1)+48*(n*n)
+ 48*n+16*n^2+64*n+64 by NEWTON:8;
then
4*(n|^2)*3*(n|^1)+36*n*n+27*n+28*n^2+84*n+63<=12*n|^(2+1)+48*n*n+ 48*
n+16*n^2+64*n+64;
then
4*(n|^2)*3*n+36*n*n+27*n+28*n^2+84*n+63<=12*n|^(2+1)+48*n*n+ 48*n+16*
n^2+64*n+64;
then
4*(n^2)*3*n+36*n*n+27*n+28*n^2+84*n+63<=12*n|^(2+1)+48*n*n+ 48*n+16*n
^2+64*n+64 by Lm1;
then 4*(n^2)*3*n+36*n*n+27*n+28*n^2+84*n+63<=12*(n|^2*n|^1)+48*n*n+ 48*n+
16*n^2+64*n+64 by NEWTON:8;
then
4*(n^2)*3*n+36*n*n+27*n+28*n^2+84*n+63<=12*(n^2*n|^1)+48*n*n+ 48*n+16
*n^2+64*n+64 by Lm1;
then 4*(n^2)*3*n+36*n*n+27*n+28*n^2+84*n+63<=12*(n^2*n)+48*n*n+ 48*n+16*n
^2+64*n+64;
then sqrt(((2*n+3)^2)*((3*n)+7))<=sqrt(((2*n)+4)^2 *((3*n)+4)) by
SQUARE_1:26;
then sqrt((2*n+3)^2)*sqrt((3*n)+7)<=sqrt(((2*n)+4)^2 *((3*n)+4)) by
SQUARE_1:29;
then sqrt((2*n+3)^2)*sqrt((3*n)+7)<=sqrt((2*n+4)^2)*sqrt((3*n+4)) by
SQUARE_1:29;
then (2*n+3)*sqrt((3*n)+7)<=sqrt((2*n+4)^2)*sqrt((3*n+4)) by SQUARE_1:22;
then
A4: (2*n+3)*sqrt((3*n)+7)<=((2*n+4)*sqrt((3*n+4)))*1 by SQUARE_1:22;
sqrt(3*n+4)>0 & sqrt(3*n+7)>0 by SQUARE_1:25;
then 1*(2*n+3)/((2*n+4)*sqrt((3*n+4)))<=1/sqrt((3*n)+7) by A4,XREAL_1:102;
then
(Partial_Product s).n*((2*(n+1)+1)/(2*(n+1)+2))<=1/sqrt(3*(n+1)+4) by A3,
XXREAL_0:2;
then (Partial_Product s).n*s.(n+1)<=1/sqrt(3*(n+1)+4) by A1;
hence thesis by Def1;
end;
(Partial_Product s).0 =s.0 by Def1
.=(2*0+1)/(2*0+2) by A1
.=1/sqrt(3*0+4) by SQUARE_1:20;
then
A5: X[0];
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
Lm8: (for n holds s.n>-1 & s.n<0) implies for n holds (Partial_Sums(s).n)*s.(n
+1)>=0
proof
defpred X[Nat] means (Partial_Sums(s).$1)*(s.($1+1))>=0;
A1: (Partial_Sums(s).0)*(s.1) = (s.0)*(s.1) by SERIES_1:def 1;
assume
A2: for n holds s.n>-1 & s.n<0;
A3: for n st X[n] holds X[n+1]
proof
let n;
assume
A4: (Partial_Sums(s).n)*(s.(n+1))>=0;
s.(n+1)<0 by A2;
then
A5: (Partial_Sums(s).n)*1<=0 by A4;
A6: (Partial_Sums(s).(n+1))*(s.(n+2)) =(Partial_Sums(s).n + s.(n+1))*(s.(
n+2)) by SERIES_1:def 1
.=(Partial_Sums(s).n)*(s.(n+2))+(s.(n+1))*(s.(n+2));
s.(n+2)<=0 & s.(n+1)<=0 by A2;
hence thesis by A5,A6;
end;
let n;
s.0<0 & s.1<0 by A2;
then
A7: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A7,A3);
hence thesis;
end;
theorem :: Bernoulli Inequality(1)
(for n holds s1.n=1+s.n & s.n>-1 & s.n<0) implies for n holds 1+
Partial_Sums(s).n<=(Partial_Product s1).n
proof
defpred X[Nat] means 1+Partial_Sums(s).$1<=(Partial_Product s1).
$1;
assume
A1: for n holds s1.n=1+s.n & s.n>-1 & s.n<0;
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: ((Partial_Product(s1)).n)*(1+s.(n+1))=((Partial_Product s1).n)*s1.(n+
1) by A1;
s.(n+1)>-1 by A1;
then
A4: s.(n+1)+1>-1+1 by XREAL_1:8;
assume 1+Partial_Sums(s).n<=(Partial_Product s1).n;
then
(1+Partial_Sums(s).n)*(1+s.(n+1))<=((Partial_Product s1).n)*(1+s.( n+1
)) by A4,XREAL_1:64;
then
A5: (1+Partial_Sums(s).n)*(1+s.(n+1))<=(Partial_Product s1).(n+1) by A3,Def1;
(Partial_Sums(s).n)*(s.(n+1))>=0 by A1,Lm8;
then
A6: (Partial_Sums(s).n)*(s.(n+1))+(1+s.(n+1)+Partial_Sums(s).n)>= 0+(1+s.
(n+1)+Partial_Sums(s).n) by XREAL_1:6;
1+Partial_Sums(s).(n+1)=1+(Partial_Sums(s).n+s.(n+1)) by SERIES_1:def 1;
hence thesis by A5,A6,XXREAL_0:2;
end;
let n;
Partial_Sums(s).0=s.0 & (Partial_Product s1).0=s1.0 by Def1,SERIES_1:def 1;
then
A7: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A7,A2);
hence thesis;
end;
Lm9: (for n holds s.n>=0) implies for n holds (Partial_Sums(s).n)*(s.(n+1))>=
0
proof
assume
A1: for n holds s.n>=0;
let n;
Partial_Sums(s).n>=0 & s.(n+1)>=0 by A1,Th34;
hence thesis;
end;
theorem :: Bernoulli Inequality(2)
(for n holds s1.n=1+s.n & s.n>=0) implies for n holds 1+Partial_Sums(s
).n<=(Partial_Product s1).n
proof
defpred X[Nat] means 1+Partial_Sums(s).$1<=(Partial_Product s1).
$1;
assume
A1: for n holds s1.n=1+s.n & s.n>=0;
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: ((Partial_Product s1).n)*(1+s.(n+1))=((Partial_Product s1).n)*s1.(n+1
) by A1;
s.(n+1)>-1 by A1;
then
A4: s.(n+1)+1>-1+1 by XREAL_1:8;
assume 1+Partial_Sums(s).n<=(Partial_Product(s1)).n;
then
(1+Partial_Sums(s).n)*(1+s.(n+1))<=((Partial_Product s1).n)*(1+s.( n+1
)) by A4,XREAL_1:64;
then
A5: (1+Partial_Sums(s).n)*(1+s.(n+1))<=(Partial_Product s1).(n+1) by A3,Def1;
(Partial_Sums(s).n)*(s.(n+1))>=0 by A1,Lm9;
then
A6: (Partial_Sums(s).n)*(s.(n+1))+(1+s.(n+1)+Partial_Sums(s).n)>= 0+(1+s.
(n+1)+Partial_Sums(s).n) by XREAL_1:6;
1+Partial_Sums(s).(n+1)=1+(Partial_Sums(s).n+s.(n+1)) by SERIES_1:def 1;
hence thesis by A5,A6,XXREAL_0:2;
end;
Partial_Sums(s).0=s.0 & (Partial_Product s1).0=s1.0 by Def1,SERIES_1:def 1;
then
A7: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A7,A2);
hence thesis;
end;
theorem :: Cauchy Inequality
s3=s1(#)s2 & s4=s1(#)s1 & s5=s2(#)s2 implies for n holds ((
Partial_Sums s3).n)^2<=(Partial_Sums s4).n*(Partial_Sums s5).n
proof
assume that
A1: s3=s1(#)s2 and
A2: s4=s1(#)s1 and
A3: s5=s2(#)s2;
let n;
A4: (Partial_Sums s3).0 =s3.0 by SERIES_1:def 1
.=s1.0 * s2.0 by A1,SEQ_1:8;
defpred X[Nat] means ((Partial_Sums s3).$1)^2<=(Partial_Sums s4).
$1* (Partial_Sums s5).$1;
A5: for n st X[n] holds X[n+1]
proof
let n;
set u=(Partial_Sums s3).n;
set v=(Partial_Sums s4).n;
set w=(Partial_Sums s5).n;
set h=s1.(n+1);
set j=s2.(n+1);
assume
A6: ((Partial_Sums s3).n)^2<=(Partial_Sums s4).n*(Partial_Sums s5).n;
then |.u.|<=sqrt(v*w) by Lm7;
then
A7: (2*(|.j.|*|.h.|))*sqrt(v*w)>=(2*(|.j.|*|.h.|))*|.u.| by XREAL_1:64;
A8: w>=0 by A3,Th36;
then
A9: w=(sqrt w)^2 by SQUARE_1:def 2;
((sqrt v)*j)^2+((sqrt w)*h)^2>=2*|.(sqrt v)*j.|*|.(sqrt w)*h.| by Th8;
then ((sqrt v)*j)^2+((sqrt w)*h)^2>=2*(|.sqrt v.|*|.j.|)*|.(sqrt w)*h.|
by COMPLEX1:65;
then
A10: ((sqrt v)*j)^2+((sqrt w)*h)^2>=2*(|.sqrt v.|*|.j.|) *(|.(sqrt w).|*
|.h.|) by COMPLEX1:65;
A11: v>=0 by A2,Th36;
then sqrt v>=0 by SQUARE_1:def 2;
then
A12: ((sqrt v)*j)^2+((sqrt w)*h)^2>=2*(sqrt v*|.j.|)*(|.(sqrt w).|*|.h.|)
by A10,ABSVALUE:def 1;
sqrt w>=0 by A8,SQUARE_1:def 2;
then ((sqrt v)*j)^2+((sqrt w)*h)^2>=2*(sqrt v*|.j.|)*((sqrt w)*|.h.|) by
A12,ABSVALUE:def 1;
then
A13: ((sqrt v)*j)^2+((sqrt(w))*h)^2>=2*(sqrt v*(sqrt(w)))*|.j.|*|.h.|;
v=(sqrt(v))^2 by A11,SQUARE_1:def 2;
then v*j^2+w*h^2>=2*(sqrt(v*w))*|.j.|*|.h.| by A11,A8,A9,A13,SQUARE_1:29;
then v*j^2+w*h^2>=2*(|.u.|*|.j.|)*|.h.| by A7,XXREAL_0:2;
then v*j^2+w*h^2>=2*(|.u*j.|)*|.h.| by COMPLEX1:65;
then v*j^2+w*h^2>=2*((|.u*j.|)*|.h.|);
then
A14: v*j^2+w*h^2>=2*|.u*j*h.| by COMPLEX1:65;
2*|.u*j*h.|>=2*(u*j*h) by ABSVALUE:4,XREAL_1:64;
then v*j^2+w*h^2>=2*u*j*h by A14,XXREAL_0:2;
then
A15: v*j^2+w*h^2-2*u*j*h>=0 by XREAL_1:48;
v*w-u^2>=0 by A6,XREAL_1:48;
then
A16: v*w-u^2+(v*j^2+w*h^2-2*u*j*h)>=0 by A15;
((Partial_Sums(s3)).(n+1))=u+s3.(n+1) by SERIES_1:def 1;
then ((Partial_Sums(s3)).(n+1))=u+h*s2.(n+1) by A1,SEQ_1:8;
then
A17: ((Partial_Sums(s3)).(n+1))^2 =u^2+2*u*(h*j)+(h*j)^2;
(Partial_Sums(s4)).(n+1)*(Partial_Sums(s5)).(n+1)= ((Partial_Sums(s4)
).n+s4.(n+1))*(Partial_Sums(s5)).(n+1) by SERIES_1:def 1;
then
(Partial_Sums(s4)).(n+1)*(Partial_Sums(s5)).(n+1)= (v+s4.(n+1))*(w+s5
.(n+1)) by SERIES_1:def 1
.=(v+h*h)*(w+s5.(n+1)) by A2,SEQ_1:8
.=(v+h*h)*(w+s2.(n+1)*s2.(n+1)) by A3,SEQ_1:8
.=v*w+v*j^2+w*h^2+h^2*j^2;
then
(Partial_Sums s4).(n+1)*(Partial_Sums(s5)).(n+1)- ((Partial_Sums s3).
(n+1))^2 =v*w-u^2+v*j^2+w*h^2+h^2*j^2-2*u*(h*j)-(h*j)^2 by A17
.=v*w-u^2+v*j^2+w*h^2-2*u*h*j;
then
(Partial_Sums s4).(n+1)*(Partial_Sums s5).(n+1)- ((Partial_Sums s3).(
n+1))^2+((Partial_Sums s3).(n+1))^2>= 0+((Partial_Sums s3).(n+1))^2 by A16,
XREAL_1:6;
hence thesis;
end;
(Partial_Sums s4).0*(Partial_Sums(s5)).0 =(s4.0)*(Partial_Sums(s5)).0 by
SERIES_1:def 1
.=(s4.0)*(s5.0) by SERIES_1:def 1
.=(s1.0)*(s1.0)*(s5.0) by A2,SEQ_1:8
.=(s1.0)^2*(s2.0)^2 by A3,SEQ_1:8;
then
A18: X[0] by A4;
for n holds X[n] from NAT_1:sch 2(A18,A5);
hence thesis;
end;
Lm10: (for n holds s.n=(s1.n+s2.n)^2) implies (Partial_Sums s).n>=0
proof
assume
A1: for n holds s.n=(s1.n+s2.n)^2;
now
let n;
s.n=(s1.n+s2.n)^2 by A1;
hence s.n>=0 by XREAL_1:63;
end;
hence thesis by Th34;
end;
theorem :: Minkowski Inequality
(s4=s1(#)s1 & s5=s2(#)s2 & for n holds s1.n>=0 & s2.n>=0 & s3.n=(s1.n+
s2.n)^2) implies for n holds sqrt((Partial_Sums s3).n) <= sqrt((Partial_Sums s4
).n) + sqrt((Partial_Sums s5).n)
proof
assume that
A1: s4=s1(#)s1 and
A2: s5=s2(#)s2 and
A3: for n holds s1.n>=0 & s2.n>=0 & s3.n=(s1.n+s2.n)^2;
A4: s1.0>=0 by A3;
defpred X[Nat] means sqrt((Partial_Sums(s3)).$1)<=sqrt((
Partial_Sums(s4)) .$1)+sqrt((Partial_Sums(s5)).$1);
A5: for n st X[n] holds X[n+1]
proof
let n;
assume
A6: sqrt((Partial_Sums s3).n)<=sqrt((Partial_Sums s4).n)+ sqrt((
Partial_Sums s5).n);
set j=s2.(n+1);
set h=s1.(n+1);
set w=(Partial_Sums s5).n;
set v=(Partial_Sums s4).n;
set u=(Partial_Sums s3).n;
A7: w>=0 by A2,Th36;
A8: j^2>=0 by XREAL_1:63;
then
A9: sqrt(w+j^2)>=0 by A7,SQUARE_1:def 2;
A10: v>=0 by A1,Th36;
then
A11: sqrt(v*w)>=0 by A7,SQUARE_1:def 2;
A12: u>=0 by A3,Lm10;
then sqrt(u)>=0 by SQUARE_1:def 2;
then (sqrt u)^2<=(sqrt(v)+sqrt(w))^2 by A6,SQUARE_1:15;
then u<=(sqrt(v))^2+2*sqrt(v)*sqrt(w)+(sqrt(w))^2 by A12,SQUARE_1:def 2;
then u<=v+2*sqrt(v)*sqrt(w)+(sqrt(w))^2 by A10,SQUARE_1:def 2;
then u<=v+2*sqrt(v)*sqrt(w)+w by A7,SQUARE_1:def 2;
then u+2*h*j<=v+w+2*(sqrt(v)*sqrt(w))+2*h*j by XREAL_1:6;
then
A13: u+2*h*j<=v+w+2*sqrt(v*w)+2*h*j by A10,A7,SQUARE_1:29;
A14: h>=0 by A3;
A15: j>=0 by A3;
A16: h^2>=0 by XREAL_1:63;
then
A17: sqrt(v+h^2)>=0 by A10,SQUARE_1:def 2;
h^2*w+j^2*v>=2*sqrt((h^2*w)*(j^2*v)) by A10,A7,A16,A8,SIN_COS2:1;
then h^2*w+j^2*v>=2*sqrt((h^2*j^2)*(w*v));
then h^2*w+j^2*v>=2*(sqrt(h^2*j^2)*sqrt(w*v)) by A10,A7,A16,A8,SQUARE_1:29;
then h^2*w+j^2*v>=2*sqrt(h^2*j^2)*sqrt(w*v);
then h^2*w+j^2*v>=2*(sqrt(h^2)*sqrt(j^2))*sqrt(w*v) by A16,A8,SQUARE_1:29;
then h^2*w+j^2*v>=2*sqrt(h^2)*sqrt(j^2)*sqrt(w*v);
then h^2*w+j^2*v>=2*h*sqrt(j^2)*sqrt(w*v) by A14,SQUARE_1:22;
then h^2*w+j^2*v>=2*h*j*sqrt(w*v) by A15,SQUARE_1:22;
then (h^2*w+j^2*v)+(v*w+h^2*j^2)>=2*h*j*sqrt(w*v)+(v*w+h^2*j^2) by
XREAL_1:6;
then v*w+j^2*v+h^2*w+h^2*j^2>=v*w+2*(sqrt(w*v))*(h*j)+h^2*j^2;
then
((sqrt(v*w))+h*j)^2>=0 & (v+h^2)*(w+j^2)>=(sqrt(v*w))^2+2*(sqrt(w*v))
*(h*j)+ (h*j)^2 by A10,A7,SQUARE_1:def 2,XREAL_1:63;
then sqrt(((sqrt(v*w))+h*j)^2)<=sqrt((v+h^2)*(w+j^2)) by SQUARE_1:26;
then (sqrt(v*w))+h*j<=sqrt((v+h^2)*(w+j^2)) by A14,A15,A11,SQUARE_1:22;
then 2*((sqrt(v*w))+h*j)<=2*(sqrt((v+h^2)*(w+j^2))) by XREAL_1:64;
then
(v+w)+(2*(sqrt(v*w))+2*h*j)<=(v+w)+(2*(sqrt((v+h^2)*(w+j^2)))) by XREAL_1:6;
then u+2*h*j<=v+w+2*(sqrt((v+h^2)*(w+j^2))) by A13,XXREAL_0:2;
then
(u+2*h*j)+(h^2+j^2)<=(v+w+2*(sqrt((v+h^2)*(w+j^2))))+(h^2+j^2) by XREAL_1:6;
then u+(h^2+2*h*j+j^2)<=(v+h^2)+2*sqrt((v+h^2)*(w+j^2))+(w+j^2);
then
u+(h+j)^2<=(sqrt(v+h^2))^2+2*sqrt((v+h^2)*(w+j^2))+(w+j^2) by A10,A16,
SQUARE_1:def 2;
then
u+(h+j)^2<=(sqrt(v+h^2))^2+2*sqrt((v+h^2)*(w+j^2))+(sqrt(w+j^2))^2 by A7,A8
,SQUARE_1:def 2;
then
(h+j)^2>=0 & u+(h+j)^2<=(sqrt(v+h^2))^2+2*(sqrt(v+h^2)*sqrt(w+j^2))+(
sqrt(w+ j^2)) ^2 by A10,A7,A16,A8,SQUARE_1:29,XREAL_1:63;
then
A18: sqrt(u+(h+j)^2)<=sqrt((sqrt(v+h^2)+sqrt(w+j^2))^2) by A12,SQUARE_1:26;
A19: sqrt((Partial_Sums s3).(n+1)) =sqrt((Partial_Sums s3).n+s3.(n+1)) by
SERIES_1:def 1
.=sqrt(u+(h+j)^2) by A3;
sqrt((Partial_Sums s4).(n+1))+sqrt((Partial_Sums(s5)).(n+1)) =sqrt((
Partial_Sums s4).n+s4.(n+1))+sqrt((Partial_Sums(s5)).(n+1)) by SERIES_1:def 1
.=sqrt(v+s4.(n+1))+sqrt(w+s5.(n+1)) by SERIES_1:def 1
.=sqrt(v+s1.(n+1)*s1.(n+1))+sqrt(w+s5.(n+1)) by A1,SEQ_1:8
.=sqrt(v+h^2)+sqrt(w+j^2) by A2,SEQ_1:8;
hence thesis by A19,A17,A9,A18,SQUARE_1:22;
end;
A20: s2.0>=0 by A3;
sqrt((Partial_Sums(s4)).0)+sqrt((Partial_Sums(s5)).0) =sqrt(s4.0)+sqrt((
Partial_Sums(s5)).0) by SERIES_1:def 1
.=sqrt(s4.0)+sqrt(s5.0) by SERIES_1:def 1
.=sqrt(s1.0*s1.0)+sqrt(s5.0) by A1,SEQ_1:8
.=sqrt((s1.0)^2)+sqrt(s2.0*s2.0) by A2,SEQ_1:8
.=s1.0+sqrt((s2.0)^2) by A4,SQUARE_1:22
.=s1.0+s2.0 by A20,SQUARE_1:22
.=sqrt((s1.0+s2.0)^2) by A4,A20,SQUARE_1:22
.=sqrt(s3.0) by A3
.=sqrt((Partial_Sums s3).0) by SERIES_1:def 1;
then
A21: X[0];
for n holds X[n] from NAT_1:sch 2(A21,A5);
hence thesis;
end;
Lm11: (for n holds s.n>0) implies (n+1)-root((Partial_Product s).n)>0
proof
assume for n holds s.n>0;
then
A1: (Partial_Product s).n>0 by Th43;
A2: n+1>=0+1 by XREAL_1:6;
then
(n+1)-root((Partial_Product s).n) =(n+1) -Root((Partial_Product s).n) by A1,
POWER:def 1;
hence thesis by A1,A2,PREPOWER:def 2;
end;
Lm12: (for n holds s.n>0 & s.n>=s.(n-1)) implies (s.(n+1)-(((Partial_Sums s).n
)/(n+1)))/(n+2)>=0
proof
assume for n holds s.n>0 & s.n>=s.(n-1);
then ((n+1)*s.(n+1))/(n+1)>=((Partial_Sums s).n)/(n+1) by Th38,XREAL_1:72;
then s.(n+1)>=((Partial_Sums s).n)/(n+1) by XCMPLX_1:89;
then s.(n+1)-(((Partial_Sums s).n)/(n+1))>=0 by XREAL_1:48;
hence thesis;
end;
theorem
(for n holds s.n>0 & s.n>=s.(n-1)) implies (Partial_Sums s).n>=(n+1)*(
(n+1)-root((Partial_Product s).n))
proof
defpred X[Nat] means (Partial_Sums s).$1>= ($1+1)*(($1+1)-root((
Partial_Product s).$1));
A1: (Partial_Sums s).0=s.0 by SERIES_1:def 1;
assume
A2: for n holds s.n>0 & s.n>=s.(n-1);
A3: for n st X[n] holds X[n+1]
proof
let n;
set u=(Partial_Sums s).n;
set v=s.(n+1);
set w=((u/(n+1))+(v-(u/(n+1)))/(n+2))|^(n+2);
set h=((n+1)-root((Partial_Product s).n));
set j=u/(n+1);
A4: v>0 by A2;
A5: n+1>=0+1 by XREAL_1:6;
then (n+1)+1>=1+1 by XREAL_1:6;
then
A6: n+2>=1 by XXREAL_0:2;
assume (Partial_Sums s).n>=(n+1)*((n+1)-root((Partial_Product s).n));
then u/(n+1)>=((n+1)* ((n+1)-root((Partial_Product s).n)))/(n+1) by
XREAL_1:72;
then ((n+1)-root((Partial_Product s).n))<=u/(n+1) by XCMPLX_1:89;
then
A7: h|^(n+1)<=j|^(n+1) by A2,Lm11,PREPOWER:9;
A8: (Partial_Product(s)).n>0 by A2,Th43;
then h=((n+1) -Root((Partial_Product s).n)) by A5,POWER:def 1;
then (Partial_Product s).n<=j|^(n+1) by A7,A8,A5,PREPOWER:19;
then ((Partial_Product s).n)*v<=(j|^(n+1))*v by A4,XREAL_1:64;
then
A9: ((Partial_Product s).(n+1))<=(j|^(n+1))*v by Def1;
A10: (Partial_Product s).(n+1)>=0 by A2,Th43;
u>0 & (v-(u/(n+1)))/(n+2)>=0 by A2,Lm12,Th33;
then
w>=(u/(n+1))|^((n+1)+1)+(n+2)*((u/(n+1))|^(n+1))* ((v-(u/(n+1)))/(n+2
)) by Th31;
then
w>=(u/(n+1))|^((n+1))*(u/(n+1))+((u/(n+1))|^(n+1))* ((v-(u/(n+1)))/(n
+2)*(n+2)) by NEWTON:6;
then
A11: w>=(u/(n+1))|^((n+1))*(u/(n+1))+((u/(n+1))|^(n+1))* (v-(u/(n+1))) by
XCMPLX_1:87;
A12: (Partial_Sums s).(n+1)>0 by A2,Th33;
((Partial_Sums s).(n+1))/(n+2) =(1*(Partial_Sums s).n+s.(n+1))/(n+2)
by SERIES_1:def 1
.=((n+1)/(n+1)*(Partial_Sums s).n+s.(n+1))/(n+2) by XCMPLX_1:60
.=((((n+2)-1)*(Partial_Sums s).n)/(n+1)+s.(n+1))/(n+2);
then ((Partial_Sums s).(n+1))/(n+2) =(((n+2)*u-u)/(n+1)+v)/(n+2)
.=((((n+2)*u)/(n+1)-u/(n+1))+v)/(n+2)
.=(((n+2)*u)/(n+1)-u/(n+1))/(n+2)+v/(n+2)
.=((n+2)*u)/(n+1)/(n+2)-(u/(n+1))/(n+2)+v/(n+2)
.=((n+2)*u)/((n+1)*(n+2))-(u/(n+1))/(n+2)+v/(n+2) by XCMPLX_1:78
.=u/(n+1)-(u/(n+1))/(n+2)+v/(n+2) by XCMPLX_1:91
.=u/(n+1)+(v/(n+2)-(u/(n+1))/(n+2))
.=u/(n+1)+(v-(u/(n+1)))/(n+2);
then (((Partial_Sums s).(n+1))/(n+2))|^(n+2)>= (Partial_Product s).(n+1)
by A11,A9,XXREAL_0:2;
then (n+2) -Root((((Partial_Sums s).(n+1))/(n+2))|^(n+2))>= (n+2) -Root((
Partial_Product s).(n+1)) by A6,A10,PREPOWER:27;
then
(((Partial_Sums s).(n+1))/(n+2))>= (n+2) -Root((Partial_Product s).(n
+1)) by A6,A12,PREPOWER:19;
then
(((Partial_Sums s).(n+1))/(n+2))>= (n+2)-root((Partial_Product s).(n+
1)) by A6,A10,POWER:def 1;
then ((Partial_Sums s).(n+1))/(n+2)*(n+2)>= (n+2)*((n+2)-root((
Partial_Product s).(n+1))) by XREAL_1:64;
hence thesis by XCMPLX_1:87;
end;
(0+1)*((0+1)-root((Partial_Product s).0)) =((0+1)-root(s.0)) by Def1
.=(Partial_Sums s).0 by A1,POWER:9;
then
A13: X[0];
for n holds X[n] from NAT_1:sch 2(A13,A3);
hence thesis;
end;