基于矩形区域剖分的不等式机器证明方法---以Zirakzadeh的一个几何不等式为例

曾振柄; 张景中

doi:10.12341/jssms09280

PDF(742 KB)

系统科学与数学 ›› 2010, Vol. 30 ›› Issue (11) : 1430-1458. DOI: 10.12341/jssms09280

论文

基于矩形区域剖分的不等式机器证明方法---以Zirakzadeh的一个几何不等式为例

曾振柄(1), 张景中(2)

作者信息 +

A Mechanical Proof to a Geometric Inequality of Zirakzadeh Through Rectangular Partition of Polyhedra

ZENG Zhenbing(1), ZHANG Jingzhong(2)

Author information +

文章历史 +

摘要

1988年,张景中,陶懋颀用细致的人工估计, 用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式, 其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形, 在每个小矩形上用数值方法验证若干三角函数不等式的正确性. 这个工作后来没有发表. 将Zirskzadeh不等式转化为一个有3个变元的根式不等式, 形如

\sqrt{m_{1}} + \sqrt{m_{2}} + \sqrt{m_{3}} \geq 3 \sqrt{m_{4}}

, 其变量所在区域为一由6个线性不等式限制形成的多面体

P

(有14个顶点, 21个棱和9个面), 先用幂级数展开方法证明讨论的根式不等式在小长方体邻域

[- 0.1, 0.1]^{3} \subset P

成立, 次将这个邻域以外的集合分割成有限多个边长不小于

\frac{1}{1280}

的小长方体或多面体, 在每个小凸体上通过计算函数在顶点的取值和函数偏导数范围证明根式不等式的正确性. 文章给出的验证数引理, 可根据连续可微函数在长方体或一般凸多面体

V

的顶点的值, 及函数偏导数的绝对值在集合

V

的上界, 证明函数在

V

上的正定性. 给出计算多项式在三维空间凸多面体上的最大值和最小值, 以及估计根式函数的验证数的机械化方法.

Abstract

In this paper is concerned with a machine proof to the following geometric inequality, which was presented by

A

. Zirakzadeh in 1964: given any triangle

A B C

and three points

P, Q, R,

which divide the perimeter of

A B C

into three equal parts, the perimeter of

P Q R

is equal to or greater than the one half of that of

A B C

. By representing the Zirakzadeh inequality as radical problem of form

f (u, v, w) = \sqrt{m_{1}} + \sqrt{m_{2}} + \sqrt{m_{3}} - 3 \sqrt{m_{4}} \geq 0

,
where

m_{1}, m_{2}, m_{3}, m_{4}

are cubic polynomials of

u, u, w

and

(u, v, w)

belongs to a polyhedron

P

R^{3}

with 14 vertices, 21 edges and 9 faces, we first construct a cube

B^{*} = [- 0.1, 0.1]^{3} \subset P

and a polynomial

g (u, v, w)

of total degree 8 so that

f (u, v, w) \geq g (u, v, w)

and

g (u, v, w) \geq 0

B^{*}

, then we prove two lemmas on error analysis for testing the positive definiteness of a continuous differentiable function on a rectangular region or a polytope through its values at the vertices, and finally we show the inequality

f (u, v, w) > 0

for

(u, v, w) \in P ∖ B^{*}

by partitioning the polyhedron into a finitely many small rectangular sets which edges are

\frac{1}{1280}

or larger and the values of

f (u, v, w)

at the vertices of
the rectangular sets exceed the test numbers for positive definiteness. The total computation time for the third step is 159.124 hours on personal computers. %(on an IBM Thinkpad T61 machine with one Intel Duo 2 CPU and an IBM workstation with two Intel Xeon CPUs). We also establish a mechanical method for computing the lower and upper bounds of polynomials and the test numbers of radical expressions over polyhedra in

R^{3}

导出引用

曾振柄 , 张景中. 基于矩形区域剖分的不等式机器证明方法---以Zirakzadeh的一个几何不等式为例. 系统科学与数学, 2010, 30(11): 1430-1458. https://doi.org/10.12341/jssms09280

ZENG Zhenbing , ZHANG Jingzhong. A Mechanical Proof to a Geometric Inequality of Zirakzadeh Through Rectangular Partition of Polyhedra. Journal of Systems Science and Mathematical Sciences, 2010, 30(11): 1430-1458 https://doi.org/10.12341/jssms09280

中图分类号： 68W30 52B10 51M16 41A10 41A05

PDF(742 KB)

253

Accesses

Citation

Detail

段落导航

摘要
Abstract
关键词
Key words
引用本文

收稿日期	修回日期	出版日期
2010-10-10	1900-01-01	2010-11-25
发布日期
2010-11-25

选择文件类型/文献管理软件名称

选择包含的内容

摘要

Abstract

关键词

Key words

引用本文

{{custom_sec.title}}

{{custom_sec.title}}

{{custom_fnGroup.title_cn}}

脚注

扫码分享

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

摘要

Abstract

关键词

Key words

引用本文

{{custom_sec.title}}

{{custom_sec.title}}

{{custom_fnGroup.title_cn}}

脚注