On the partial product of series and related basic inequalities

of

MATHEMATICSBia󰀮lystok,2005

13,Number3,Pages413–416

OnthePartialProductofSeriesand

RelatedBasicInequalities

FuguoGe

QingdaoUniversityofScience

andTechnology

China

XiquanLiang

QingdaoUniversityofScience

andTechnology

China

Summary.Thisarticledescribesdefinitionofpartialproductofseries,

introducedsimilarlytoitsrelatedpartialsum,aswellasseveralimportantin-equalitiestrueforchosenspecialseries.

MMLidentifier:SERIES3,version:7.5.014.39.921

Thenotationandterminologyusedinthispaperareintroducedinthefollowingarticles:[1],[9],[10],[5],[2],[4],[6],[7],[8],and[3].

Forsimplicity,weadoptthefollowingconvention:a,b,carepositiverealnumbers,m,x,y,zarerealnumbers,nisanaturalnumber,ands,s1,s2,s3,s4,s5aresequencesofrealnumbers.

Letusconsiderx.Notethat|x|isnonnegative.Wenowstateanumberofpropositions:

x+m

(1)Ify>xandx≥0andm≥0,thenxy≤y+m.√b

≥a·b.(2)a+2b

+a(3)ab≥2.y2

(4)(x+2)≥x·y.

yx+y2

≥((5)x+22).

(6)x2+y2≥2·x·y.

2

22

2

y

(7)x+≥x·y.2(8)x2+y2≥2·|x|·|y|.(9)(x+y)2≥4·x·y.

(10)x2+y2+z2≥x·y+y·z+x·z.

413

c󰀁

2005UniversityofBia󰀮lystokISSN1426–2630

414fuguogeandxiquanliang

(11)(x+y+z)2≥3·(x·y+y·z+x·z).(12)a3+b3+c3≥3·a·b·c.(13)

a3+b3+c3

≥a·b·c.3b3c3b3(ab)+(c)+(√a)≥a(14)

a

+cb+c.

(15)a+b+c≥3·3a·b·c.√a+b+c

≥3a·b·c.(16)31

(17)Ifx+y+z=1,thenx·y+y·z+x·z≤3.

(18)Ifx+y=1,thenx·y≤14.

1(20)Ifa+b=1,then(1+a)·(1+1b)≥9.1

.(19)Ifx+y=1,thenx2+y2≥21.(21)Ifx+y=1,thenx3+y3≥4(22)Ifa+b=1,thena3+b3<1.(24)If|x|≤a,thenx2≤a2.(26)||x|−|y||≤|x|+|y|.(27)Ifa·b·c=1,then

1

(23)Ifa+b=1,then(a+a)·(b+1b)≥25

4.

(25)If|x|≥a,thenx2≥a2.

1a+

1b+

1c(28)Ifx>0andy>0andz<0andx+y+z=0,then(x2+y2+z2)3≥

6·(x3+y3+z3)2.(29)Ifa≥1,then

ab

+ac

(30)Ifa≥bandb≥c,thenaa·bb·cc≥(a·b·c)

an+bn

2bn

≥(a+2).

≥

√

a+

√

b+

√

c.≥2·a

√

b·c.

a+b+c

3.

(31)(a+b)n+2≥an+2+(n+2)·an+1·b.(32)

󰀁

(33)Ifforeverynholdss(n)>0,thenforeverynholds(κα=0s(α))κ∈N(n)>

0.

󰀁

(34)Ifforeverynholdss(n)≥0,thenforeverynholds(κα=0s(α))κ∈N(n)≥

0.

󰀁

(35)Ifforeverynholdss(n)<0,then(κ=0s(α))κ∈N(n)<0.󰀁α(36)Ifs=s1s1,thenforeverynholds(κα=0s(α))κ∈N(n)≥0.(37)Ifforeverynholdss(n)>0ands(n)>s(n−1),then(n+1)·s(n+1)>

󰀁κ

(α=0s(α))κ∈N(n).(38)Ifs=s1s2andforeverynholdss1(n)≥0ands2(n)≥0,

󰀁κ󰀁

thenforeverynholds(κs(α))(n)≤(κ∈Nα=0α=0(s1)(α))κ∈N(n)·󰀁κ

(α=0(s2)(α))κ∈N(n).(39)Ifs=s1s2andforeverynholdss1(n)<0ands2(n)<0,then

󰀁κ󰀁κ󰀁κ

(α=0s(α))κ∈N(n)≤(α=0(s1)(α))κ∈N(n)·(α=0(s2)(α))κ∈N(n).

󰀁󰀁κ

(40)Foreverynholds|(κs(α))(n)|≤(κ∈Nα=0α=0|s|(α))κ∈N(n).

onthepartialproductofseriesandrelated...

(41)(

󰀁κ

󰀁κ

s(α))(n)≤(κ∈Nα=0α=0|s|(α))κ∈N(n).

415

Letusconsiders.Thepartialproductofsyieldingasequenceofreal

numbersisdefinedbytheconditions(Def.1).

(Def.1)(i)(Thepartialproductofs)(0)=s(0),and

(ii)foreverynholds(thepartialproductofs)(n+1)=(thepartialproductofs)(n)·s(n+1).

Wenowstateanumberofpropositions:

(42)Ifforeverynholdss(n)>0,then(thepartialproductofs)(n)>0.(43)Ifforeverynholdss(n)≥0,then(thepartialproductofs)(n)≥0.(44)Supposethatforeverynholdss(n)>0ands(n)<1.Letgivenn.Then

(thepartialproductofs)(n)>0and(thepartialproductofs)(n)<1.(45)Ifforeverynholdss(n)≥1,thenforeverynholds(thepartialproduct

ofs)(n)≥1.

(46)Supposethatforeverynholdss1(n)≥0ands2(n)≥0.Letgivenn.

Then(thepartialproductofs1)(n)+(thepartialproductofs2)(n)≤(thepartialproductofs1+s2)(n).

2·n+1

(47)Ifforeverynholdss(n)=2·n+2,then(thepartialproductofs)(n)≤

√1.3·n+4(48)Ifforeverynholdss1(n)=1+s(n)ands(n)>−1ands(n)<0,then

󰀁

foreverynholds1+(κα=0s(α))κ∈N(n)≤(thepartialproductofs1)(n).(49)Ifforeverynholdss1(n)=1+s(n)ands(n)≥0,thenforeverynholds

󰀁κ

1+(α=0s(α))κ∈N(n)≤(thepartialproductofs1)(n).

(50)Ifs3=s1s2ands4=s1s1ands5=s2s2,thenforeverynholds

󰀁󰀁󰀁κ

2≤(κ(s)(α))(κ(s)(α))(n)(n)·(34κ∈Nκ∈Nα=0α=0α=0(s5)(α))κ∈N(n).

(51)Ifs4=s1s1ands5=s2s2andforeverynholdss1(n)≥

0ands2(n)󰀂≥0ands3(n)=(s1(n)󰀂+s2(n))2,thenforev-󰀁κ󰀁κerynholds((s)(α))(n)≤(κ∈Nα=03α=0(s4)(α))κ∈N(n)+󰀂󰀁κ(α=0(s5)(α))κ∈N(n).(52)Ifforeverynholdss(n)󰀂>0ands(n)>s(n−1),then

󰀁κ

n+1

(thepartialproductofs)(n).(α=0s(α))κ∈N(n)≥(n+1)·

References

[1]GrzegorzBancerek.Theordinalnumbers.FormalizedMathematics,1(1):91–96,1990.

[2]Czes󰀿lawByli´nski.Thecomplexnumbers.FormalizedMathematics,1(3):507–513,1990.[3]Czes󰀿lawByli´nski.Functionsfromasettoaset.FormalizedMathematics,1(1):153–164,

1990.[4]Jaros󰀿lawKotowicz.Realsequencesandbasicoperationsonthem.FormalizedMathemat-ics,1(2):269–272,1990.[5]Rafa󰀿lKwiatek.FactorialandNewtoncoefficients.FormalizedMathematics,1(5):887–890,

1990.

[6]LibraryCommitteeoftheAssociationofMizarUsers.Binaryoperationsonnumbers.To

appearinFormalizedMathematics.

416fuguogeandxiquanliang

[7]KonradRaczkowskiandAndrzejN¸edzusiak.Realexponentsandlogarithms.Formalized

Mathematics,2(2):213–216,1991.[8]KonradRaczkowskiandAndrzejN¸edzusiak.Series.FormalizedMathematics,2(4):449–

452,1991.

[9]AndrzejTrybulec.Subsetsofcomplexnumbers.ToappearinFormalizedMathematics.[10]AndrzejTrybulecandCzes󰀿lawByli´nski.Somepropertiesofrealnumbers.Formalized

Mathematics,1(3):445–449,1990.

ReceivedJuly6,2005