:: On the Partial Product and Partial Sum of Series and Related Basic :: Inequalities :: by Fuguo Ge and Xiquan Liang :: :: Received November 23, 2005 :: Copyright (c) 2005-2018 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, SEQ_1, NEWTON, ARYTM_1, RELAT_1, SQUARE_1, ARYTM_3, POWER, COMPLEX1, CARD_1, FUNCT_1, SERIES_1, SERIES_3, NAT_1, REAL_1; notations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, NAT_1, SQUARE_1, NEWTON, SEQ_1, POWER, SERIES_1, SERIES_3; constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, NEWTON, SERIES_1, SERIES_3, VALUED_1, ABIAN; registrations XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, NEWTON, SERIES_3, NUMBERS, VALUED_0, RELSET_1, FUNCT_2, ORDINAL1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; begin reserve a,b,c,d for positive Real, m,u,w,x,y,z for Real, n,k for Nat, s,s1 for Real_Sequence; theorem :: SERIES_5:1 (a+b)*(1/a+1/b)>=4; theorem :: SERIES_5:2 a|^4+b|^4>=a|^3*b+a*b|^3; theorem :: SERIES_5:3 a1; theorem :: SERIES_5:16 a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d)<2; theorem :: SERIES_5:17 a+b>c & b+c>a & a+c>b implies 1/(a+b-c)+1/(b+c-a)+1/(c+a-b)>=9/(a+b+c); theorem :: SERIES_5:18 sqrt((a+b)*(c+d))>=sqrt(a*c)+sqrt(b*d); theorem :: SERIES_5:19 (a*b+c*d)*(a*c+b*d)>=4*a*b*c*d; theorem :: SERIES_5:20 a/b+b/c+c/a>=3; theorem :: SERIES_5:21 a*b+b*c+c*a=1 implies a+b+c>=sqrt 3; theorem :: SERIES_5:22 (b+c-a)/a+(c+a-b)/b+(a+b-c)/c>=3; theorem :: SERIES_5:23 (a+1/a)*(b+1/b)>=(sqrt(a*b)+1/sqrt(a*b))^2; theorem :: SERIES_5:24 (b*c)/a+(a*c)/b+(a*b)/c>=a+b+c; theorem :: SERIES_5:25 x>y & y>z implies x^2*y+y^2*z+z^2*x>x*y^2+y*z^2+z*x^2; theorem :: SERIES_5:26 a>b & b>c implies b/(a-b)>c/(a-c); theorem :: SERIES_5:27 b>a & c>d implies c/(c+a)>d/(d+b); theorem :: SERIES_5:28 m*x+z*y<=sqrt(m^2+z^2)*sqrt(x^2+y^2); theorem :: SERIES_5:29 (m*x+u*y+w*z)^2<=(m^2+u^2+w^2)*(x^2+y^2+z^2); theorem :: SERIES_5:30 (9*a*b*c)/(a^2+b^2+c^2)<=a+b+c; theorem :: SERIES_5:31 a+b+c<=sqrt((a^2+a*b+b^2)/3)+sqrt((b^2+b*c+c^2)/3)+sqrt((c^2+c*a+a^2)/ 3); theorem :: SERIES_5:32 sqrt((a^2+a*b+b^2)/3)+sqrt((b^2+b*c+c^2)/3)+sqrt((c^2+c*a+a^2)/3) <= sqrt((a^2+b^2)/2)+sqrt((b^2+c^2)/2)+sqrt((c^2+a^2)/2); theorem :: SERIES_5:33 sqrt((a^2+b^2)/2)+sqrt((b^2+c^2)/2)+sqrt((c^2+a^2)/2) <=sqrt(3*(a^2+b ^2+c^2)); theorem :: SERIES_5:34 sqrt(3*(a^2+b^2+c^2))<=(b*c)/a+(c*a)/b+(a*b)/c; theorem :: SERIES_5:35 a+b=1 implies (1/a^2-1)*(1/b^2-1)>=9; theorem :: SERIES_5:36 a+b=1 implies a*b+1/(a*b)>=17/4; theorem :: SERIES_5:37 a+b+c = 1 implies 1/a+1/b+1/c>=9; theorem :: SERIES_5:38 a+b+c = 1 implies (1/a-1)*(1/b-1)*(1/c-1)>=8; theorem :: SERIES_5:39 a+b+c = 1 implies (1+1/a)*(1+1/b)*(1+1/c)>=64; theorem :: SERIES_5:40 x+y+z=1 implies x^2+y^2+z^2>=1/3; theorem :: SERIES_5:41 x+y+z=1 implies x*y+y*z+z*x<=1/3; theorem :: SERIES_5:42 a>b & b>c implies (a to_power (2*a))*(b to_power (2*b))*(c to_power (2 *c)) > (a to_power (b+c))*(b to_power (a+c))*(c to_power (a+b)); theorem :: SERIES_5:43 n>=1 implies a|^(n+1)+b|^(n+1)>=a|^n*b+a*b|^n; theorem :: SERIES_5:44 a^2+b^2=c^2 & n>=3 implies a|^(n+2)+b|^(n+2)=1 implies (1+1/(n+1))|^n<(1+1/n)|^(n+1); theorem :: SERIES_5:46 n>=1 & k>=1 implies (a|^k+b|^k)*(a|^n+b|^n)<=2*(a|^(k+n)+b|^(k+n)); theorem :: SERIES_5:47 (for n holds s.n=1/sqrt(n+1)) implies for n holds (Partial_Sums s).n<2 *sqrt(n+1); theorem :: SERIES_5:48 (for n holds s.n=1/((n+1)^2)) implies for n holds (Partial_Sums s).n<=2-1/(n+1); theorem :: SERIES_5:49 (for n holds s.n=1/((n+1)^2)) implies (Partial_Sums s).n<2; theorem :: SERIES_5:50 (for n holds s.n<1) implies for n holds Partial_Sums(s).n0 & s.n<1) implies for n holds Partial_Product(s).n>= Partial_Sums(s).n-n; theorem :: SERIES_5:52 (for n being Nat holds s.n>0 & s1.n=1/s.n) implies for n holds Partial_Sums(s1).n>0; theorem :: SERIES_5:53 (for n being Nat holds s.n>0 & s1.n=1/s.n) implies for n holds Partial_Sums(s).n*Partial_Sums(s1).n>=(n+1)^2; theorem :: SERIES_5:54 (for n st n>=1 holds s.n=sqrt(n) & s.0=0) implies for n st n>=1 holds Partial_Sums(s).n<1/6*(4*n+3)*sqrt(n); theorem :: SERIES_5:55 (for n st n>=1 holds s.n=sqrt(n) & s.0=0) implies for n st n>=1 holds Partial_Sums(s).n>(2/3)*n*sqrt(n); theorem :: SERIES_5:56 (for n st n>=1 holds s.n=1+1/(2*n+1) & s.0=1) implies for n st n>=1 holds Partial_Product(s).n>(1/2)*sqrt(2*n+3); theorem :: SERIES_5:57 (for n st n>=1 holds s.n=sqrt(n*(n+1)) & s.0=0) implies for n st n>=1 holds Partial_Sums(s).n>(n*(n+1))/2;