:: On the Partial Product of Series and Related Basic Inequalities :: by Fuguo Ge and Xiquan Liang :: :: Received July 6, 2005 :: Copyright (c) 2005-2021 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; 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; end; theorem :: SERIES_3:1 y>x & x>=0 & m>=0 implies x/y <= (x+m)/(y+m); theorem :: SERIES_3:2 (a+b)/2>=sqrt(a*b); theorem :: SERIES_3:3 b/a+a/b>=2; theorem :: SERIES_3:4 ((x+y)/2)^2>=x*y; theorem :: SERIES_3:5 (x^2+y^2)/2>=((x+y)/2)^2; theorem :: SERIES_3:6 x^2+y^2>=2*x*y; theorem :: SERIES_3:7 (x^2+y^2)/2>=x*y; theorem :: SERIES_3:8 :: CSSPACE2:5 x^2+y^2>=2*|.x.|*|.y.|; theorem :: SERIES_3:9 (x+y)^2>=4*x*y; theorem :: SERIES_3:10 x^2+y^2+z^2>=x*y+y*z+x*z; theorem :: SERIES_3:11 (x+y+z)^2>=3*(x*y+y*z+x*z); theorem :: SERIES_3:12 a|^3+b|^3+c|^3>=3*a*b*c; theorem :: SERIES_3:13 (a|^3+b|^3+c|^3)/3>=a*b*c; theorem :: SERIES_3:14 (a/b)|^3+(b/c)|^3+(c/a)|^3>=b/a+c/b+a/c; theorem :: SERIES_3:15 (a+b+c)>=3*(3-root(a*b*c)); theorem :: SERIES_3:16 (a+b+c)/3>=3-root(a*b*c); theorem :: SERIES_3:17 x+y+z=1 implies x*y+y*z+x*z<=1/3; theorem :: SERIES_3:18 x+y=1 implies x*y<=1/4; theorem :: SERIES_3:19 x+y=1 implies x^2+y^2>=1/2; theorem :: SERIES_3:20 a+b=1 implies (1+1/a)*(1+1/b)>=9; theorem :: SERIES_3:21 x+y=1 implies x|^3+y|^3>=1/4; theorem :: SERIES_3:22 a+b=1 implies a|^3+b|^3<1; theorem :: SERIES_3:23 a+b=1 implies (a+1/a)*(b+1/b)>=25/4; theorem :: SERIES_3:24 for x, a being Real st |.x.|<=a holds x^2<=a^2; theorem :: SERIES_3:25 |.x.|>=a implies x^2>=a^2; theorem :: SERIES_3:26 |.|.x.|-|.y.|.|<=|.x.|+|.y.|; theorem :: SERIES_3:27 a*b*c = 1 implies (1/a)+(1/b)+(1/c)>=sqrt(a)+sqrt(b)+sqrt(c); theorem :: SERIES_3:28 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; theorem :: SERIES_3:29 a>=1 implies (a to_power b)+(a to_power c)>=2*(a to_power sqrt(b*c)); theorem :: SERIES_3:30 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); theorem :: SERIES_3:31 for a,b being non negative Real holds (a+b)|^(n+2)>=a|^ (n+2)+(n+2)*(a|^(n+1))*b; theorem :: SERIES_3:32 (a|^n+b|^n)/2 >= ((a+b)/2)|^n; theorem :: SERIES_3:33 (for n holds s.n>0) implies for n holds (Partial_Sums s).n>0; theorem :: SERIES_3:34 (for n holds s.n>=0) implies for n holds (Partial_Sums s).n>=0; theorem :: SERIES_3:35 (for n holds s.n<0) implies (Partial_Sums s).n<0; theorem :: SERIES_3:36 s=s1(#)s1 implies for n holds (Partial_Sums s).n>=0; theorem :: SERIES_3:37 (for n holds s.n>0 & s.n>s.(n-1)) implies (n+1)*s.(n+1) > ( Partial_Sums s).n ; theorem :: SERIES_3:38 (for n holds s.n>0 & s.n>=s.(n-1)) implies (n+1)*s.(n+1) >= ( Partial_Sums s).n; theorem :: SERIES_3:39 (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); theorem :: SERIES_3:40 (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); theorem :: SERIES_3:41 for n holds |.(Partial_Sums s).n.|<=(Partial_Sums (abs s)).n; theorem :: SERIES_3:42 (Partial_Sums s).n<=(Partial_Sums abs s).n; definition let s; func Partial_Product(s) -> Real_Sequence means :: SERIES_3:def 1 it.0=s.0 & for n holds it.(n+1) = it.n * s.(n+1); end; theorem :: SERIES_3:43 (for n holds s.n>0) implies (Partial_Product s).n>0; theorem :: SERIES_3:44 (for n holds s.n>=0) implies (Partial_Product s).n>=0; theorem :: SERIES_3:45 (for n holds s.n>0 & s.n<1) implies for n holds (Partial_Product s).n> 0 & (Partial_Product s).n<1; theorem :: SERIES_3:46 (for n holds s.n>=1) implies for n holds (Partial_Product s).n>=1; theorem :: SERIES_3:47 (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; theorem :: SERIES_3:48 (for n holds s.n=(2*n+1)/(2*n+2)) implies (Partial_Product s).n<=1/ sqrt(3*n+4); theorem :: SERIES_3:49 :: 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; theorem :: SERIES_3:50 :: 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; theorem :: SERIES_3:51 :: 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; theorem :: SERIES_3:52 :: 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); theorem :: SERIES_3:53 (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));