奇妙な含意

今回は,古典一階の論理式

$\exists x\left(p(x)\to q\right)\land\exists x\left(q\to p(x)\right)\to\exists x\left(\left(p(x)\to q\right)\land\left(q\to p(x)\right)\right)$

は定理式か?と云うお話です.

量化だけを見ると,前件の $2$ つの $x$ は同じとは限らないので,後件のようにはまとめられず,定理式ではなさそうですが,量化されているのは含意とその逆,しかも,$q$ は $x$ の出現をもたないという辺り...かなり訴えています.

まず,後件内の含意の連言を,定理式

$\left(A\land B\right)\lor\left(\neg{A}\land\neg{B}\right)\to\left(A\to B\right)\land\left(B\to A\right)$

により,存在量化が分配できる選言に繰り上げます.つまり,後件は

$\exists x\left(p(x)\land q\right)\lor\exists x\left(\neg{p(x)}\land\neg{q}\right)$

で十分であり,これは定理式 $q\lor\neg{q}$ による場合分けが使える形で,前件のうち,$q$ に対しては $\exists x\left(q\to p(x)\right)$,$\neg{q}$ に対しては $\exists x\left(p(x)\to q\right)$ を用いれば得られます.

本日のC.A.D.

区間 $x\ge0$ を定義域とする関数 $\sqrt{x}$ は,Lipschitz 連続ではありません.

In[1]:= Reduce[ForAll[{x,y},And[0<=x,0<=y],Abs[Sqrt[x]-Sqrt[y]]<=L*Abs[x-y]],Reals]                              

Out[1]= False

しかし,一様連続です.

In[2]:= Reduce[ForAll[e,0<e,Exists[d,0<d,ForAll[{x,y},And[0<=x,0<=y,Abs[x-y]<d],Abs[Sqrt[x]-Sqrt[y]]<e]]],Reals] 

Out[2]= True

そのこころは...

In[3]:= Reduce[0<e && 0<d && ForAll[{x,y},And[0<=x,0<=y,Abs[x-y]<d],Abs[Sqrt[x]-Sqrt[y]]<e],Reals]               

Out[3]= e > 0 && Inequality[0, Less, d, LessEqual, e^2]

さらに,Hölder 連続です.

In[4]:= Reduce[ForAll[{x,y},And[0<=x,0<=y],Abs[Sqrt[x]-Sqrt[y]]<=L*Sqrt[Abs[x-y]]],Reals]                        

Out[4]= L >= 1

本日のC.A.D.

$a,\ b,\ c$ が実数のとき,次の $(1),\ (2)$ は等価です.

$\displaystyle a>1\ \land\ b>1\ \land\ c>1\ \land\ 1>\frac{1}{a}+\frac{1}{a}+\frac{1}{c}\ \ \cdots\ \ (1)$

$\forall x\ \forall y\ \forall z\ \left(\ x+y+z=1\to ax^2+by^2+cz^2>1\ \right)\ \ \cdots\ \ (2)$

? tst12([all,all,all,all,all],[a,b,c,x,y],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"1<a,1<b,1<c,a*b+b*c+c*a<a*b*c,a*x^2+b*y^2+c*(1-x-y)^2>1",23);Ans();
[[],[[a,1,5],[b,1,5],[c,1,10],[x,2,4],[y,2,4]]]
 *** reordering by degree+occurrence.
 *** using Lazard's method (MPP17).
[y,1]
[x,2]
[b,5]
[a,6]
[c,5]
time = 86 ms.
11 125(0,12) 1165(0,139) 6989(568,224) 26427(2822,0) 
 *** combined adjacent 26426 cells.
1[true,true,true,true,true]
time = 3,781 ms.

? tst12([ex,ex,ex,all,all],[a,b,c,x,y],and,"a*x^2+b*y^2+c*(1-x-y)^2>1,a<=1");Ans();
 *** using Lazard's method (MPP17).
[y,1]
[x,2]
[c,7]
[b,8]
[a,7]
time = 56 ms.
12 172(0,22) 2194(0,244) 11434(904,376) 0(302,0) 
1[false]
time = 1,227 ms.

? tst12([ex,ex,ex,all,all],[a,b,c,x,y],and,"a*x^2+b*y^2+c*(1-x-y)^2>1,a*b*c<=a*b+b*c+c*a");Ans();
 *** using Lazard's method (MPP17).
[y,1]
[x,2]
[c,7]
[b,8]
[a,7]
time = 81 ms.
15 219(0,26) 1094(0,295) 6340(552,324) 0(654,0) 
1[false]
time = 768 ms.

なお,今回の主張自体は,例えば,$(1)\ \to\ (2)$ では Cauchy–Schwarz の不等式,$(2)\ \to\ (1)$ では $x,\ y,\ z$ として $1,\ 0,\ 0$ や $\frac{1/a}{(1/a)+(1/b)+(1/c)},\ \frac{1/b}{(1/a)+(1/b)+(1/c)},\ \frac{1/c}{(1/a)+(1/b)+(1/c)}$ などを用いれば見易いです.

本日のC.A.D.

? tst12([ex,ex,ex],[v,a,b,c],andx,"0<=c,c<=1,0<=a+b+c,a+b+c<=1,0<=4*a+2*b+c,4*a+2*b+c<=1,v==9*a^6+3*b^6+c^6",23);Ans();
[[[v,1,1]],[[a,6,5],[b,6,5],[c,6,7]]]
 *** reordering by degree+occurrence.
 *** using Lazard's method (MPP17).
[b,5]
[a,9]
[c,45]
[v,427]
time = 41min, 59,024 ms.
1119 36599(1178,2462) 877137(6767,32575) 871(11910,24420) 
 *** combined adjacent 870 cells.
1[[v,1] <= v <= [v-202,1],true,true,true]
time = 12min, 56,787 ms.

Mathematica 12.3.1

Cloud 版より早く Wolfram Engine のリビジョンが上がりました.
f:id:ehito:20210723182107j:plain

$ sudo bash ./WolframEngine_12.3.1_LINUX.sh

-----------------------------------------------------------------------------------------------------------------
                                         Wolfram Engine 12.3 Installer 
-----------------------------------------------------------------------------------------------------------------

Copyright (c) 1988-2021 Wolfram Research, Inc. All rights reserved.

WARNING: Wolfram Engine is protected by copyright law and international treaties. Unauthorized reproduction
or distribution may result in severe civil and criminal penalties and will be prosecuted to the maximum
extent possible under law.

Enter the installation directory, or press ENTER to select /usr/local/Wolfram/WolframEngine/12.3:
> 

The selected directory contains files and/or directories that may be overwritten during installation. If
you have any files you wish to keep in this directory, you should exit the installer and move the files to
a separate directory before continuing.

Overwrite directory (y/n)?
> y

Now installing...

[**************************************************************************************************************]

Type the directory path in which the Wolfram Engine script(s) will be created, or press ENTER to select
/usr/local/bin:
> 

  (1) Overwrite
  (2) Rename
  (3) Cancel

Type your selection, or press ENTER to select (1):
> 


Installing WolframScript system integration...

Installation complete.

$ wolfram
Wolfram Language 12.3.1 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= $Version                                                                                                 

Out[1]= "12.3.1 for Linux x86 (64-bit) (June 24, 2021)"

In[2]:= Reduce[ForAll[{x,y},x^2+y^2<=b,x^4+y^4+2*a*x*y<=1],{a,b},Reals] // Timing                                

Out[2]= 
{3.987473, (a <= -Sqrt[2/3] && b <= a + Sqrt[2 + a^2]) || 
  (Inequality[-Sqrt[2/3], Less, a, LessEqual, Sqrt[2/3]] && b <= Sqrt[2 - a^2]/Sqrt[2]) || 
  (a > Sqrt[2/3] && b <= -a + Sqrt[2 + a^2])}

本日のC.A.D.

座標平面において,原点 $(0,\ 0)$ が $3$ 点 $(3,\ 0)$,$(-1,\ \sqrt{3})$,$(-2,\ -2\sqrt{3})$ を頂点とする $3$ 角形の Fermat 点 ( https://en.wikipedia.org/wiki/Fermat_point ) であることを示します.

$\forall x\ \forall y \ \left( 9\le\sqrt{(x-3)^2+y^2}+\sqrt{(x+1)^2+(y-\sqrt{3})^2}+\sqrt{(x+2)^2+(y+2\sqrt{3})^2}\ \right )\ \land\ 9=3+2+4 $

? tst12([ex,ex,ex,ex,ex,ex],[r,a,b,c,x,y],andx,"0<r,r^2==3,0<=a,0<=b,0<=c,a^2==(x-3)^2+y^2,b^2==(x+1)^2+(y-r)^2,c^2==(x+2)^2+(y+2*r)^2,9>a+b+c",23);Ans();
[[],[[r,2,6],[a,2,3],[b,2,3],[c,2,3],[x,2,6],[y,2,5]]]
 *** reordering by degree.
 *** using Lazard's method (MPP17).
[c,3]
[b,4]
[a,6]
[y,13]
[x,76]
[r,1554]
time = 43min, 49,542 ms.
1 171(4,5) 5715(68,128) 5715(356,6960) 5715(4,2606) 0(2,1012) 
1[false]
time = 49,278 ms.

? tst12([ex,ex,ex,ex],[r,a,b,c],andx,"0<r,r^2==3,0<=a,0<=b,0<=c,a^2==(0-3)^2+0^2,b^2==(0+1)^2+(0-r)^2,c^2==(0+2)^2+(0+2*r)^2,9==a+b+c");Ans();
 *** using Lazard's method (MPP17).
[c,3]
[b,4]
[a,7]
[r,8]
time = 91 ms.
1 1(0,2) 1(0,2) 1(0,2) 
 *** combined adjacent 0 cells.
1[true,true,true,true]
time = 4 ms.

$\forall x\ \forall y \ \left( 9=\sqrt{(x-3)^2+y^2}+\sqrt{(x+1)^2+(y-\sqrt{3})^2}+\sqrt{(x+2)^2+(y+2\sqrt{3})^2}\ \to\ x=0\ \land\ y=0\ \right )$

? tst12([ex,ex,ex,ex,ex,ex],[r,x,y,a,b,c],andx,"0<r,r^2==3,0<=a,0<=b,0<=c,a^2==(x-3)^2+y^2,b^2==(x+1)^2+(y-r)^2,c^2==(x+2)^2+(y+2*r)^2,9==a+b+c,0<x^2+y^2");Ans();
 *** using Lazard's method (MPP17).
[c,3]
[b,4]
[a,6]
[y,14]
[x,89]
[r,1675]
time = 52min, 2,991 ms.
1 175(8,7) 5814(70,129) 5814(364,7074) 5814(4,2644) 0(2,1026) 
1[false]
time = 51,849 ms

本日のC.A.D.

? tst12([all,all],[a,b,c,d,x,y],eq,"y<(x+a)^15+b,y<(x+c)^15+d");Ans(1);
 *** using Lazard's method (MPP17).
[y,2]
[x,1]
[d,4]
[c,7]
[b]
[a,1]
time = 1min, 36,784 ms.
3 3(0,0) 37(84,7) 535(26,54) 1647(52,12) 9(0,6) 
 *** combined adjacent 8 cells.
1[true,true,c = [a-c,1],d = [b-d,1],true,true]
time = 9,594 ms.
Wolfram Language 12.3.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^5+b,y<(x+c)^5+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing   

Out[1]= {0.104536, c == a && d == a^5 + b - c^5}

In[2]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^6+b,y<(x+c)^6+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing   

Out[2]= {0.476967, c == a && d == a^6 + b - c^6}

In[3]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^7+b,y<(x+c)^7+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing   

Out[3]= 
{0.528524, (a < 0 && c == a && d == a^7 + b - c^7) || (a == 0 && c == 0 && d == b) || 
  (a > 0 && c == a && d == a^7 + b - c^7)}

In[4]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^8+b,y<(x+c)^8+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing   

Out[4]= {36.708199, c == a && d == a^8 + b - c^8}

In[5]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^9+b,y<(x+c)^9+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing   

Out[5]= {4.41101, c == a && d == a^9 + b - c^9}

In[6]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^10+b,y<(x+c)^10+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing 

Out[6]= {368.027142, c == a && d == a^10 + b - c^10}

In[7]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^11+b,y<(x+c)^11+d]],{a,b,c,d},Reals,WorkingPrecision->30]//Timing 

Reduce::cadpr: The cylindrical algebraic decomposition algorithm used by Reduce
     failed due to a too low WorkingPrecision. Increasing the value of WorkingPrecision may allow the algorithm
     to succeed.
^C
Interrupt> a

Out[7]= $Aborted

In[8]:= Reduce[ForAll[{x,y},Equivalent[y<(x+a)^11+b,y<(x+c)^11+d]],{a,b,c,d},Reals,WorkingPrecision->60]//Timing 

Out[8]= {27.447685, c == a && d == a^11 + b - c^11}