何燈，李云杰

（福清第三中學(xué)，福建福清350315）

單變元三角函數(shù)不等式的發(fā)現(xiàn)與自動證明

何燈，李云杰

（福清第三中學(xué)，福建福清350315）

借助于級數(shù)理論和maple數(shù)學(xué)軟件，本文研究單變元三角函數(shù)不等式的發(fā)現(xiàn)及機(jī)器自動證明，根據(jù)算法所編寫的程序hdtrig2015能夠在極短的時間內(nèi)實現(xiàn)三角函數(shù)不等式的自動驗證.豐富的實例表明本文的算法具有極大的優(yōu)越性，能夠成批實現(xiàn)三角函數(shù)不等式的機(jī)器自動驗證.

三角函數(shù)；不等式；泰勒展開；機(jī)器證明；實根隔離

0　引言

不等式的發(fā)現(xiàn)與機(jī)器證明，一直是數(shù)學(xué)機(jī)械化、自動推理及智能系統(tǒng)領(lǐng)域的研究難點和熱點問題，近年來得到了長足的發(fā)展[1-17].特別是楊路教授提出了降維算法[2-3，9，14]，據(jù)之編寫的通用程序BOTTEMA能夠成批驗證和發(fā)現(xiàn)不等式.BOTTEMA的開發(fā)極大地影響著不等式研究者的研究方式和研究方法，但B0TTEMA只能處理代數(shù)不等式或先把幾何不等式轉(zhuǎn)化為代數(shù)不等式，尚不能解決一般的超越不等式自動證明問題，楊路教授也曾指出：B0TTEMA目前尚不適合處理類似sinx＜x＜tanx（0＜x＜/2）這樣的超越不等式，這是值得進(jìn)一步研究的課題[14].

三角函數(shù)不等式的證明是初等不等式證明問題的難點，因為不僅要運用代數(shù)不等式的方法，而且要使用三角函數(shù)的許多性質(zhì)，如正余弦函數(shù)的有界性、三角函數(shù)的單調(diào)性等，各種三角函數(shù)之間的變換在證明不等式過程中的目的性、規(guī)律性不強(qiáng)，還有一些特殊方法不易機(jī)械化[5]，受這種種因素的限制，三角函數(shù)不等式的自動證明研究一直進(jìn)展緩慢.

文獻(xiàn)[16]中基于區(qū)間分析算法的InequalityProve程序能夠?qū)崿F(xiàn)一些三角函數(shù)不等式的自動驗證，可是針對性不強(qiáng)，適用范圍并不廣泛（InequalityProve驗證本文例9的問題，需借助手動分析而無法實現(xiàn)完全的機(jī)械式自動推理）.

文獻(xiàn)[17]中基于萬能代換及級數(shù)理論的算法能夠解決較大范圍的問題，但對一些較復(fù)雜的不等式，代換后的結(jié)果將極其復(fù)雜，從而給自動驗證增加了一定的難度，也在一定程度上降低了效率.

本文繼續(xù)探討單變元三角函數(shù)不等式的發(fā)現(xiàn)及機(jī)器自動證明，提出了基于級數(shù)理論及待定系數(shù)法的三角函數(shù)不等式的自動發(fā)現(xiàn)算法，基于級數(shù)理論及多項式實根隔離的三角函數(shù)不等式自動驗證算法，并由此編寫了自動驗證程序hdtrig2015，例舉了豐富的實例進(jìn)行了程序測試，這些例子充分體現(xiàn)出本文的算法具有極大的優(yōu)越性，能夠成批實現(xiàn)三角函數(shù)不等式的機(jī)器自動驗證，且驗證過程簡單易懂，是“可讀”的.

1　三角函數(shù)不等式的發(fā)現(xiàn)—模型法

本章節(jié)介紹在maple平臺上，借助于待定系數(shù)法和三角函數(shù)的泰勒展開式，實現(xiàn)三角函數(shù)不等式發(fā)現(xiàn)的一個算法.

步驟一（泰勒展開）：在maple中執(zhí)行泰勒展開式命令taylor（F1，x=0，10），可得以a，b，c，d，e，f為系數(shù)的展開式A0+A1x2+A2x4+A3x6+A4x8+O（x9）.

步驟二（解方程組）：在maple中執(zhí)行解方程組命令

步驟三（賦值化簡）：將方程組的解代入F1中并化簡，得

步驟四（預(yù)判）：在maple中執(zhí)行畫圖命令plot（F1，x=0..Pi/2），觀察圖象，可猜測的上界.

從而猜測如下雙邊不等式成立（證明見文獻(xiàn)[19]）

依據(jù)上述步驟，可編寫maple程序，實現(xiàn)此類三角函數(shù)不等式的自動發(fā)現(xiàn).

2　三角函數(shù)不等式的自動證明

2.1引理及證明

證明記Si（x）=sin x-s2i+1（x）=sin x-，下面利用數(shù)學(xué)歸納法證明Si（x）≥0.

當(dāng)i=0時，S0（x）=sinx-s1（x）=sinx-注意到

設(shè)i=l（l∈N+）時，

綜上，對任意i∈N，Si（x）=sinx-s2i+1（x）≥0.同理，可證s2i（x）-sinx≥0成立.

由sinx≥s2i+1（x）可得

2.2第一類型不等式的驗證

在maple中執(zhí)行求導(dǎo)命令FF:=diff（15*F2，x）及去分母命令numer（FF），轉(zhuǎn)化為證明

步驟二（積化和差）：將待證式子積化和差（maple中的命令combine可實現(xiàn)三角函數(shù)的積化和差），等價于證明F3＞0，其中

步驟三（縮小為多項式）：借助于泰勒展開式和引理，將F3縮小為F4，其中

注1將待證式積化和差，轉(zhuǎn)化為形如F3的形式，使得泰勒展開后的式子在保證高精度的情況下能夠達(dá)到最大限度的簡化.

注2在利用引理對F3進(jìn)行放縮時，可取定i為一個較大的自然數(shù)（如i=3），以避免i從0開始逐個循環(huán)，從而能減少循環(huán)次數(shù)，縮短程序運行時間.

步驟四（系數(shù)有理化）：由于步驟五中的實根隔離命令realroot要求多項式的系數(shù)必須為有理數(shù)，當(dāng)步驟三中所得多項式的系數(shù)出現(xiàn)無理數(shù)（含根號或等，maple中的命令whattype命令檢驗系數(shù)是否為整數(shù)、分?jǐn)?shù)，是否含根號、等）時，需對這些無理系數(shù)進(jìn)行放縮.設(shè)某項的無理系數(shù)為λ，實際編程中可取λ的不足近似值其中[x]表示不超過x的最大整數(shù)，由0≤x-［x］＜1可得來替代λ以達(dá)到縮?。ㄓ欣砘┑哪康模ˇ说倪^剩近似（同樣由0≤x-［x］＜1可得來替代λ以達(dá)到放大（有理化）的目的.設(shè)經(jīng)過系數(shù)有理化處理后，最終所得有理系數(shù)多項式為F5.

注3此例中F4的系數(shù)均為有理數(shù)，經(jīng)步驟四處理以后，所得的多項式F5＝F4.

步驟五（實根隔離）：借助于maple中的實根隔離命令realroot（隔離精度為萬分之一），得到F5的實根區(qū)間為

經(jīng)第四步處理后，得F5=F4，經(jīng)第五步求得F5的實根隔離區(qū)間為

注5為了避免出現(xiàn)死循環(huán)，可限定循環(huán)的次數(shù)以及循環(huán)的時間，以使得程序能在規(guī)定的次數(shù)或規(guī)定的時間內(nèi)結(jié)束運行.

注6以上六個步驟適用第一類中以x=0為取等條件的情形（因為步驟三中默認(rèn)正余弦函數(shù)在x=0處進(jìn)行泰勒展開），當(dāng)需驗證以x=/2為取等條件的不等式時，可作代換x=/2-x，將待證不等式轉(zhuǎn)化為以x=0為取等條件的情形進(jìn)行求證.

2.3第二類型不等式的驗證

2.2中的算法適用于單個區(qū)間端點為取等條件的情形，若待證不等式為第二類型不等式時（區(qū)間的兩端點均可取等），則可將區(qū)間分為兩個小區(qū)間（0，0.8），（/2-0.8，/2），（顯然兩區(qū)間的并區(qū)間為（0，/2））.當(dāng)x∈（0，0.8）時，此時待證不等式為第一類型不等式（x=0為取等條件），可類似于2.2中的步驟驗證之.當(dāng)x∈（/2-0.8，π/2），此時待證不等式為第一類型不等式（x=/2為取等條件），可作代換x=/2-x，將待證不等式轉(zhuǎn)化為x=0為取等條件的情形進(jìn)行求解.

2.4hdtrig2015程序模塊介紹

依據(jù)上述算法分析，筆者編寫了自動驗證程序hdtrig2015，該程序由tlsin、tlcos、jinsi、dxssx、geli、hprove這六個模塊構(gòu)成.

tlsin及tlcos模塊利用了2.1的引理，可實現(xiàn)正余弦函數(shù)的放縮（2.2步驟三）.

jinsi模塊可實現(xiàn)無理系數(shù)的放縮（2.2步驟四）.

dxssx模塊包含了tlsin、tlcos、jinsi三個模塊，可實現(xiàn)將一個三角函數(shù)式縮小為一個有理系數(shù)多項式（2.2步驟三和步驟四）.

geli模塊可實現(xiàn)一個有理系數(shù)多項式的實根隔離，并判定實根區(qū)間是否在給定的區(qū)間內(nèi)（2.2步驟五和步驟六）

hprove模塊是程序的主要模塊，包含了dxssx、geli兩個模塊，綜合實現(xiàn)了2.2中的六個步驟.

3　hdtrig2015程序運行實例

在maple15平臺上，筆者利用hdtrig2015驗證了Jordan不等式、Huygens不等式、Wilker不等式、Kober不等式等經(jīng)典三角函數(shù)不等式及其改進(jìn)，下面是一些有代表性的例子.所用計算機(jī)硬件環(huán)境為Intel（R）Core（TM）i3-2310MCPU@2.10 GHz.

3.1第一類型的例子

證明該左邊不等式耗時0.483 s，進(jìn)行了一次循環(huán).證明右邊不等式耗時0.436 s，進(jìn)行了一次循環(huán).

例2[18]設(shè)x∈（0，/2），則

證明該左邊不等式耗時0.764 s，進(jìn)行了一次循環(huán).證明右邊不等式耗時0.297 s，進(jìn)行了一次循環(huán).

例3[20]設(shè)x∈（0，/2），則，對G3（x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時0.967 s，進(jìn)行了一次循環(huán).

例4[19]設(shè)x∈（0，/2），則

證明該不等式耗時1.326 s，進(jìn)行了兩次循環(huán).例5[21]339（Huygens不等式）設(shè)x∈（0，/2），則2sinx+tanx＞3x.證明該不等式耗時0.432 s，進(jìn)行了一次循環(huán).

例6[22]設(shè)x∈（0，/2），則

證明該不等式耗時0.967 s，進(jìn)行了一次循環(huán).

例7[22]設(shè)x∈（0，/2），則

證明該不等式耗時1.045 s，進(jìn)行了一次循環(huán).

例8[21]339（Wilker不等式）設(shè)x∈（0，/2），則

證明該不等式耗時0.437s，進(jìn)行了一次循環(huán).

例9[23]設(shè)x∈（0，/2），則記對G9（x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時0.967 s，進(jìn)行了兩次循環(huán).

例10[22]設(shè)x∈（0，/2），則記G10（x對G1（0x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時0.936 s，進(jìn)行了一次循環(huán).

例11[22]設(shè)x∈（0，/2），則

記G11（x），對G11（x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時1.076 s，進(jìn)行了一次循環(huán).

例12[24]（Wilker型不等式）設(shè)x∈（0，/2），則

證明該不等式耗時0.702 s，進(jìn)行了一次循環(huán).

例13[25]設(shè)x∈（0，/2），則

證明該不等式耗時0.640 s，進(jìn)行了一次循環(huán).

例14[22]設(shè)x∈（0，/2），則

證明該不等式耗時0.281 s，進(jìn)行了一次循環(huán).

例15[22]設(shè)x∈（0，/2），則

證明該不等式耗時0.999 s，進(jìn)行了一次循環(huán).

3.2第二類型的例子

例16[20]設(shè)x∈（0，/2），則

證明該不等式耗時（0.780+0.967）s，各進(jìn)行了一次循環(huán).

例17[19]設(shè)x∈（0，/2），則

證明該不等式耗時（0.967+1.248）s，各進(jìn)行了一次循環(huán).

例18[26]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.608+0.609）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.296+0.281）s，各進(jìn)行了一次循環(huán).

例19[27]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.655+0.593）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.249+0.343）s，各進(jìn)行了一次循環(huán).

例20[28]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.624+0.566）s，各進(jìn)行了一次循環(huán).右端不等式證明見例19.

例21[28]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.640+0.670）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.281+0.452）s，各進(jìn)行了一次循環(huán).

例22[30]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.655+0.671）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.281+0.468）s，各進(jìn)行了一次循環(huán).

例23[30]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.671+0.671）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.328+0.406）s，各進(jìn)行了一次循環(huán).

例24[31]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.656+1.138）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.484+0.406）s，各進(jìn)行了一次循環(huán).

例25[31]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.967+1.217）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.546+0.640）s，各進(jìn)行了一次循環(huán).

例26[32]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.795+1.030）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.608+0.858）s，各進(jìn)行了一次循環(huán).

例27[33]設(shè)x∈（0，/2），則

證明左端不等式耗時（1.061+1.420）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.577+0.718）s，各進(jìn)行了一次循環(huán).

例28[21]329（Kober不等式）設(shè)x∈（0，/2），則

證明左端不等式耗時（0.702+0.390）s，各進(jìn)行了一次循環(huán).證明右端不等式（第一類型不等式）耗時0.265 s，進(jìn)行了一次循環(huán).

例29[34]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.593+0.406）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.234+0.296）s，各進(jìn)行了一次循環(huán).

例30[34]設(shè)x∈（0，/2），則

證明左端不等式耗時（0.593+0.453）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時（0.280+0.297）s，各進(jìn)行了一次循環(huán).

4　結(jié)語

借助于maple數(shù)學(xué)軟件和級數(shù)理論，本文研究了三角函數(shù)不等式的發(fā)現(xiàn)與機(jī)器自動證明，提出了基于級數(shù)理論及多項式實根隔離的三角函數(shù)不等式自動驗證算法.該算法雖然不完備，但根據(jù)算法編寫的試探性程序hdtrig2015能夠在極短時間內(nèi)實現(xiàn)三角函數(shù)不等式的自動驗證，且驗證過程簡單易懂，是“可讀”的，足見算法的優(yōu)越性.相較文獻(xiàn)[16]的區(qū)間分析的方法及文獻(xiàn)[17]的萬能公式代換結(jié)合泰勒展開的方法，本文的方法更為簡單、直接、高效、具有更大的適用范圍，我們希望能進(jìn)一步發(fā)展此算法，以期解決更多傳統(tǒng)方法難以解決的問題.

[1]楊路，侯曉榮，曾振柄.多項式的完全判別系統(tǒng)[J].中國科學(xué)：E輯，1996，26（5）：424-441.

[2]楊路.不等式機(jī)器證明的降維算法與通用程序[J].高技術(shù)通訊，1998，7：20-25.

[3]楊路，夏時洪.一類構(gòu)造性幾何不等式的機(jī)器證明[J].計算機(jī)學(xué)報，2003，26（7）：769-778.

[4]陳世平，張景中.初等不等式的可讀證明的自動生成[J].四川大學(xué)學(xué)報（工程科學(xué)版），2003，35（4）：86-93.

[5]陳世平，張景中.三角不等式的自動證明[J].四川大學(xué)學(xué)報（自然科學(xué)版），2003，40（4）：686-690.

[6]陳勝利，黃方劍.三元對稱形式的Schur分拆與不等式的可讀證明[J].數(shù)學(xué)學(xué)報，2006，49（3）：491-502.

[7]楊路.差分代換與不等式機(jī)器證明[J].廣州大學(xué)學(xué)報（自然科學(xué)版），2006，5（2）：1-7.

[8]黃方劍.一類多項式不等式的證明研究[J].科學(xué)技術(shù)與工程，2007，7（15）：3856-3859.

[9]楊路，夏壁燦.不等式機(jī)器證明與自動發(fā)現(xiàn)[M].北京：科學(xué)出版社，2008.

[10]徐嘉，姚勇.一類根式不等式的有理化算法與機(jī)器證明[J].計算機(jī)學(xué)報，2008，31（2）：24-31.

[11]陳勝利，姚勇，徐嘉.分拆降維方法和機(jī)器證明[J].系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（1）：26-34.

[12]楊路，姚勇.差分代換矩陣與多項式的非負(fù)性判定[J].系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（9）：1169-1177.

[13]姚勇.基于列隨機(jī)矩陣的逐次差分代換與正半定型的機(jī)械化判定[J].中國科學(xué)：數(shù)學(xué)，2010，40（3）：251-264.

[14]楊路，郁文生.常用基本不等式的機(jī)器證明[J].智能系統(tǒng)學(xué)報，2011，6（5）：377-390.

[15]楊路，郁文生，袁如意.一類積分不等式的機(jī)器判定[J].中國科學(xué)：信息科學(xué)，2011，41（1）：48-65.

[16]邵俊偉，侯曉榮.InequalityProve及一個公開問題的求解[J].計算機(jī)工程與科學(xué)，2011，33（6）：114-117.

[17]陳世平.三角函數(shù)不等式的自動證明[J].四川大學(xué)學(xué)報（自然科學(xué)版），2013，50（3）：537-540.

[18]李明，何燈.關(guān)于的較強(qiáng)上下界及其應(yīng)用[J].北京聯(lián)合大學(xué)學(xué)報（自然科學(xué)版），2010，24（2）：47-48.

[19]何燈，王少光，吳善和.關(guān)于Jordan不等式的拓廣及應(yīng)用[J].汕頭大學(xué)學(xué)報（自然科學(xué)版），2014，29（1）：24-32.

[20]Yang Z H.Unification and refinements of Jordan,Adamovi-Mitrinoviand and Cusa’s Inequalities[J/OL]. [2012-03-28].http：//arxiv.org/abs/1304.3180,2013.

[21]匡繼昌.常用不等式[M].4版.濟(jì)南：山東科學(xué)技術(shù)出版社，2010.

[22]CHEN C P，CHEUNG W S.Sharpness of Wilker and Huygens type inequalities[J/OL].Journal of Inequalities and Applications.[2013-04-11].http：//www.journalofinequalitiesandapplications.com/content/2012/1/72.

[23]ZHANGL，ZHUL.AnewelementaryproofofWilker’sinequalities[J].MathematicalInequalities&Applications, 2007,11（1）：149-151.

[24]WU S H，SRIVASTAVA H M.A weighted and exponential generalization of Wilker’s inequality and its applications[J].Integral Transforms and Special Functions，2007，18（8）：529-535.

[25]王梓華.介紹一個Wilker型不等式[J].宜賓學(xué)院學(xué)報（自然科學(xué)版），2007，7（6）：21-22.

[26]祁鋒.Jordan和Kober不等式的拓廣與加強(qiáng)[J].工科教學(xué)，1996，12（4）：98-102.

[27]ZHUL.SharpeningJordan’s inequalityand the YangLe inequality[J].Applied Mathematics Letters，2006，19（3）：240-243.

[28]WU S H.Sharpness and generalization of Jordan’s inequality and its application[J].Taiwanese Journal of Mathematics，2008，12（2）：325-336.

[29]姜衛(wèi)東，華云.Jordan不等式的改進(jìn)及應(yīng)用[J].高等數(shù)學(xué)研究，2006，9（5）：60-61.

[30]ZHUL.SharpeningJordan’sinequalityandtheYangLeinequality,Ⅱ[J].AppliedMathematicsLetters,2006,19（9）：990-994.

[31]何燈，沈志軍.Jordan不等式的拓廣及應(yīng)用[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報（自然科學(xué)版），2011，29（5）：45-50.

[32]何燈，沈志軍.Jordan不等式的新型拓廣及應(yīng)用[J].廣東第二師范學(xué)院學(xué)報，2011，31（5）：23-30.

[33]何燈，沈志軍.Jordan不等式的拓廣及應(yīng)用Ⅱ[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報（自然科學(xué)版），2012，30（1）：19-23.

[34]祁峰，郭白妮.關(guān)于Kober不等式的推廣[J].焦作礦業(yè)學(xué)院學(xué)報，1993，12（4）：101-103.

The Finding and Automated Proving of the Univatiate Trigonometric Function Inequality

HE Deng,LI Yunjie
（Number 3 Middle School,Fuqing 350315,Fujian,China）

With the help of series theory and mathematical software-Maple，this paper studies the finding and automated proving of the univatiate trigonometric inequality.According to the algorithm program hdtrig 2015，the automatic proving is realized for the trigonometric function inequality.Many examples show that this algorithm has great superiority and can realize the machine automatic proving for a batch of trigonometric function inequality.

trigonometricfunction;inequality;Taylor expansion;machineproving;realrootisolation

O 211.67

A

1001-4217（2016）01-0024-11

2015-03-09

何燈（1984-），男，福建福清人，學(xué)士，中學(xué)教師，全國不等式研究會成員.研究方向：解析不等式及不等式機(jī)器證明.E-mail：hedeng123@163.com