tthnew's blog: KIỂM TRA TÍNH ĐÚNG ĐẮN CỦA BẤT ĐẲNG THỨC

KIỂM TRA TÍNH ĐÚNG ĐẮN CỦA BẤT ĐẲNG THỨC

VỚI SỰ TRỢ GIÚP CỦA MÁY VI TÍNH

tthnew

1. Mở đầu

Sự phát triển của công nghệ đã làm biến chuyển cuộc sống của con người. Bất đẳng thức nói riêng và toán học nói chung cũng thế$,$ máy tính đã giúp con người giải quyết nhiều bài toán khó nhằn nếu chỉ làm bằng tay.

Với sự trợ giúp của máy tính$,$ và nhiều công trình nghiên cứu của các giáo sư Ji Chen$,$ Sui Zhen Lin$,$ Liu BaoQian$,..$ con người đã có thể viết một bất đẳng thức về dạng tổng bình phương một cách nhanh chóng với sự trợ giúp của máy tính.

Tuy nhiên, nếu không biết tính đúng sai của bài toán mà đã vội cho máy tính để SOS thì thật lãng phí thời gian mà đôi khi chẳng cho kết quả.

May mắn thay$,$ bài toán này đã được giải quyết hoàn toàn bởi $\text{Wen - Tsun Wu}$ cùng các đồng nghiệp. Giáo sư $\text{Yang Lu}$ và các đồng nghiệp của mình đã dựa trên "giải thuật" của Wu để viết nên chương trình Bottema2009$,$ hoạt động trên Maple.

Sau đó một thời gian ngắn$,$ $\text{Jingjun Han}$ cũng đã viết một chương trình psdgcd^[2]$,$ cũng là phần mềm hoạt động trên Maple.

Bài viết này chủ yếu giới thiệu về chương trình Bottema2009 do tính toàn diện của nó so với psdgcd và nhiều chương trình khác. (mình chỉ giới thiệu cách thực hiện$,$ vì kiến thức rất hạn hẹp không thể hiểu chi tiết chương trình).

Mình cũng sẽ đề cập đến chương trình agl2009 và mã nguồn của nó trong bài viết này.

Chương trình Bottema2009 được viết trên phiên bản Maple cũ$,$ nên chương trình không tương thích với các phiên bản Maple mới hơn do có sự thay đổi về cú pháp lập trình ở các phiên bản.

Ví dụ.

Cho $x,y,z>0.$ Chứng minh rằng$:$ $$\displaystyle \sum {\frac { \left( z+x \right) \left( x+y \right) }{ \left( y+z \right) \left( 3\,{x}^{2}+4\,yz \right) }} \geqslant \frac{18}{7(x+y+z)}+\frac{x^3+y^3+z^3-3xyz}{(x+y+z)^4} $$

Rõ ràng bài này quy đồng lên là một đa thức bậc $11$$,$ nếu đưa vào máy tính để SOS ngay cũng khó để ra kết quả mặt khác ta chưa biết tính đúng sai của nó.

Bằng lệnh xprove(ineq,[ineq(s)]) của chương trình Bottema2009$,$ ta kiểm tra được bất đẳng thức này sai với [a = 2, b = 1/2, c = 1] sau 0.041s.

Nếu bạn có Maple$,$ hãy download file này về để xem các ví dụ khác.

https://drive.google.com/uc?id=1NeXrQnZOHgf2W3KRLv2uy02Tm0qFG0Ak&export=download

2. Bottema2009

a) Trước hết$,$ ta định nghĩa các biến sau trong Bottema. (các biến trong Bottema được dùng thống nhất)

a$,$ b$,$ c là độ dài $3$ cạnh tam giác.

$s=\frac{a+b+c}{2}$ là nửa chu vi.

$x,y,z$ với $x\equiv s-a,..$

$\text{R}$ là vòng tròn

$r$ là bán kính

$r_a,r_b,r_c$ là bán kính của các đường tròn ngoại tiếp tương ứng.

$h_a,h_b,h_c$ là chiều cao tương ứng.

$w_a,w_b,w_c$ là các đường phân giác của các góc tương ứng.

$S$ là diện tích tam giác.

$d$ là khoảng cách từ tâm đường tròn đến tâm của tam giác.

$p:=4r(R-2r),q:=s^2-16Rr+5r^2$

$A,B,C$ là các góc tương ứng.

$\sin (A),..$ là $\sin$ của các góc tương ứng.

Các hàm lượng giác khác được ký hiệu tương tự.

b) Các lệnh chính trong Bottema2009

2.1. prove(ineq,[ineq(s)])

Mục đích: Chứng minh bất đẳng thức hình học trong tam giác hoặc các bất đẳng thức đại số tương đương nó.

Trong đó: ineq là bất đẳng thức cần chứng minh$,$ [ineq(s)] là tập hợp các bất đẳng thức được cho ở giả thiết, được biểu diễn dưới dạng các biến hình học trong danh sách trên.

2.2. xprove(ineq,[ineq(s)])

Mục đích: Chứng minh các bất đẳng thức đại số với các biến không âm.

Trong đó: ineq là bất đẳng thức cần chứng minh$,$ [ineq(s)] là tập hợp các bất đẳng thức đại số cho ở giả thiết.

Ví dụ. xprove( sqrt(u^2+v^2)+sqrt((1-u)^2+(1-v)^2) >= sqrt(2),[ u <= 1,v <= 1 ] );

Lưu ý: xprove được mặc định là các biến không âm nên không cần viết thêm vào [ineq(s)]

2.3. yprove(ineq,[ineq(s)])

Mục đích: Chứng minh bất đẳng thức đại số với biến thực.

Trong đó: ineq là bất đẳng thức cần chứng minh$,$ [ineq(s)] là tập hợp các bất đẳng thức đại số cho ở giả thiết.

Ví dụ. >f:=(x^2+y^2+z^2-x*y-y*z-z*x)^2+((3/7)*(147+56*sqrt(7))^(1/3)-3/(147+56*sqrt(7))^(1/3)+3)*(x^3*y+y^3*z+z^3*x);

>yprove(f >= 0, []);

2.4. sprove(ineq)

Mục đích: Chứng minh bất đẳng thức đa thức đối xứng với các biến không âm.

Ví dụ. >f:=x^3*y*z-x^4*y-x^4*z+x^5+y^3*z*x-y^4*z-y^4*x+y^5+z^3*x*y-z^4*x-z^4*y+z^5;

>sprove(f>=0);

2.5. cmin(ineq,[ineqs],var)

Mục đích: Chứng minh bất đẳng thức hình học phụ thuộc vào tham số var. Khi var là hằng số$,$ nó thuộc loại bất đẳng thức mà hàm prove $(\,\text{2.1}\,)$ có thể xử lí.

Ví dụ. cmin( wa^2+wb^2+wc^2 <= 4*R^2+11*r^2+k*r*(R-2*r),[],k );

Ta nhận được $\text{k}$ là một nghiệm của phương trình $81\,{k}^{3}-846\,{k}^{2}+2428\,k-1116=0\,\,(\frac{1}{2} \leqslant k \leqslant 1)$

2.6. ccmin(ineq,[ineqs],var)

Mục đích: ccmin có chức năng tương tự như cmin nhưng nó chỉ được áp dụng nếu ta biết rằng giá trị nhỏ nhất chỉ có thể đạt được khi được lấy trên tam giác cân. Tức là hàm cmin tổng quát hơn!

Ví dụ. ccmin( wa^2+wb^2+wc^2 <= 4*R^2+11*r^2+k*r*(R-2*r),[],k );

2.7. xmin(ineq,[ineqs],var)

Mục đích. Đối với một bất đẳng thức đại số phụ thuộc vào tham số var$,$ tìm giá trị nhỏ nhất của var để bất đẳng thức đúng.

Ví dụ. xmin((32/27)*(a+b+c)^3-2*a*b^2-6*b*c^2-8*c*a^2-13*a*b*c+k*b*(a-2*c)^2 >= 0, [], k)

Ta tìm được $k_{\min}=-\frac{1}{2}.$ Ngoài ra đây là bài làm chặt của một bất đẳng thức của anh Huyện.

2.8. xmax(ineq,[ineqs],var)

Mục đích. Đối với một bất đẳng thức đại số phụ thuộc vào tham số var$,$ tìm giá trị lớn nhất của var để bất đẳng thức đúng.

Ví dụ. xmax((a^2+b^2+c^2)/(a*b+b*c+a*c)+8*k*a*b*c/((a+b)*(b+c)*(c+a))-1-k >= 0, [], k)

Ta tìm được $k_{\max} =1.$

$(\ast)$ Chú ý.

$+)$ Các lệnh $(\,\text{2.7}\,)$ và $(\,\text{2.8}\,)$ chỉ dùng cho các biến không âm.

Việc tìm hằng số tốt cho bất đẳng thức với biến thực ta vẫn có thể dùng các lệnh $(\,\text{2.7}\,)$ và $(\,\text{2.8}\,)$ tuy nhiên cần xét $8$ trường hợp^[6].

$+)$ Trên đây chỉ là các lệnh chính chứ không phải tất cả.

3. Chương trình agl2009

a) Sơ lược về agl2009.

Chương trình agl2009 do giáo sư Liu BaoQian phát triển dựa trên sự thay thế khác biệt với các ràng buộc.

Phiên bản nâng cấp của chương trình$,$ agl2009$,$ có đề cập về việc áp dụng phép thay thế vi phân với các ràng buộc trong việc chứng minh các bất đẳng

thức căn bản. Một số bất đẳng thức hình học đẹp được phát hiện với chương trình agl.

b) Cách sử dụng.

Về cơ bản (không phải tất cả)$,$ việc dùng agl2009 dường như đơn giản hơn bottema. Sau đây là một vài lệnh chính cần biết$,$

Đầu tiên khởi chạy chương trình agl2009 bằng lệnh:

> read "Đường dẫn/agl2009.txt"

Tiếp theo$,$ nhập bất đẳng thức cần chứng minh.

>g := wb*wc/(2*ra+wa)-(2*(b+c))*a*r/((a+b)*(c+a))

Nhập auto(g) và làm theo hướng dẫn của chương trình.

Đối với bài này$,$ chương trinh bảo chúng ta "you only run agl(w1),if Inequality forms is a>=b"

Vậy nhập$:$ >agl(w1);

Tiếp theo nhập eq(g) để tìm dấu đẳng thức.

c) Công bố mã nguồn chương trình agl2009.