奇妙な含意

今回は,古典一階の論理式 $\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$ は同…

本日の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

本日の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\ \righ…

本日の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,…

Mathematica 12.3.1

Cloud 版より早く Wolfram Engine のリビジョンが上がりました. $ sudo bash ./WolframEngine_12.3.1_LINUX.sh ----------------------------------------------------------------------------------------------------------------- Wolfram Engine 12.3 …

本日の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{(…

本日の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 ce…

本日のC.A.D.

今回は,第一種 Chebyshev 多項式 $T_4(x)=64x^7-112x^5+56x^3-7x$ に関する $\exists a\ \exists b\ \exists c\ \forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x\le m\,)\quad \cdots\quad (*)$ が $1\le m $ と等価であるという性質です.まず $\f…

本日のC.A.D.

A.W.Strzebonski "Cylindrical Algebraic Decomposition using validated numerics" の 7.2. Randomly generated systems で使用された入力です.元の code では CylindricalDecomposition ですが,変数順序を heuristic に委ねるため,無指定の Reduce で実…

本日のC.A.D.

CAD において,変数順序の選定は非常に重要です. 例えば ? projs([x1,x2,x3,x4],[-218 + 955*x1^2*x2*x3 + 520*x2*x3^3 + 1017*x3^4 + 250*x1*x2*x4 - 391*x2^3*x4 - 525*x1*x3*x4^2]); *** using Lazard's method (MPP17). [x4,1] [x3,3] [x2,4] [x1,4] ti…

Taxicab number $\operatorname{Ta}(4)$

今回は「 $x^3+y^3=a,\ 1\le x\le y$ を満たす格子点 $(x,\ y)$ の個数が $4$ である」ような $a$ の最小値,および,それに対応する $4$ 個の格子点を求める問題です.処理時間とメモリーとのバランスから,適当な上界を与え,出現をカウントしつつ,$x^3+y…

本日のC.A.D.

Quantified Formula: QE(forall a b c d) ((a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0 and -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -…

本日のC.A.D.

$\exists a\ \exists b\ \exists c\ \forall x\ \forall y\ [\ \neg[a=0 \land b=0] \land\, [\,ax+by+c=0\ \to\ dx^2+exy+fy^2=1\,]\,]$ C.W.Brown "Simple CAD Construction and its Applications" ? tst12([ex,ex,ex,all,all],[d,e,f,a,b,c,x,y],(f1,f2,f…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ,ma, mb, mc がその各辺の中点と対頂点との距離(つまり,中線の長さ)ならば ${\displaystyle\frac{3}{4}}(a+b+c) 8.1 Bottema, et. al. "GEOMETRIC INEQUALITIES"等式制約は中線定理,非退化 3 角形の存在条件は WLOG …

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ,ha, hb, hc がその各辺と対頂点との距離(つまり,高さ)ならば $2(h_a+h_b+h_c)\le\sqrt{3}(a+b+c)$ 6.1 Bottema, et. al. "GEOMETRIC INEQUALITIES"3 角形の面積を d/2 とおくと ? tst12([ex,ex,ex,ex],[x,a,b,c,d],a…

本日のC.A.D.

t が実数,a, b, c がある 3 角形の 3 辺の長さならば $(a^2+b^2+c^2) (a^{t-2} b^{t-2}+b^{t-2} c^{t-2}+c^{t-2} a^{t-2}) 1.22 Bottema, et. al. "GEOMETRIC INEQUALITIES" 今回も指数に変数が含まれるので(比の値の範囲ではなく)大小関係の特定に十分な…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ,F がその 3 角形の面積,a*ha=b*hb=c*hc=2*F,そして,t が実数のとき,Mt が t-power mean( https://en.wikipedia.org/wiki/Generalized_mean )ならば $\begin{eqnarray} & &2F\min\{ (abc)^{-2/3}, (\min\{a,b,c\} …

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ,s=(a+b+c)/2 ならば $\sqrt{s} 1.20 Bottema, et. al. "GEOMETRIC INEQUALITIES"まず,a,b,c に対する不等式制約は 0<a,0<b,a<b+c,b<c+a,c<a+b とし,s>0 により,s=1(つまり,a/s,b/s,c/s を改めて a,…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ,s=(a+b+c)/2,d=(a^2+b^2+c^2-ab-bc-ca)^(1/2) ならば $25abc 1.13 Bottema, et. al. "GEOMETRIC INEQUALITIES" (原著に 25abc はありません)今回も 0<a, 0<b を制約に加え,不要な cell の生成を抑制します. ? ts…

Mathematica 12.3.0

Mathematica の Reduce の次のような bug に遭遇,Wolfram Research の algorithms developer である Adam Strzebonski さんにお伝えしたのは,今年の 2 月でした. Wolfram Language 12.2.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Res…

本日のC.A.D.

t が実数,a, b, c がある 3 角形の 3 辺の長さ,s=(a+b+c)/2 ならば $a^t(s-a)+b^t(s-b)+c^t(s-c)\le(1/2)abc(a^{t-2}+b^{t-2}+c^{t-2})$ 1.10 Bottema, et. al. "GEOMETRIC INEQUALITIES"今回は指数に変数が含まれるので(比の値の範囲ではなく)大小関係…

3 角形の辺の長さと C.A.D.

前回の benchmark における変数順序,a, b, c についての不等式制約,各問題の処理時間とそれらの合計(ms)は,次の通りです. [m, a, b, c] a

realgeom benchmark

https://github.com/kovzol/realgeom/blob/master/src/test/resources/benchmark.csv 上記の各 LHS,RHS の s に (a+b+c)/2 を代入し,LHS-m*RHS を通分した有理式の分子 P に対する tst12([ex,ex], [m,b,c], andx, "P|_{a=1}=0, 1

GeoGebra Discovery

いわゆる対話型幾何学ソフト(https://en.wikipedia.org/wiki/List_of_interactive_geometry_software)における"証明"のサポートは,形式的証明の作成支援とシンボリックな座標計算への翻訳とに大別できます.今回の GeoGebra Discovery はこの後者であり,…

本日のC.A.D.

前回は S、T が ¬(0∈S) ∨ ¬(0∈T) を満たす場合でしたが,一般には ∃s∃t(z=s*t ∧ s∈S ∧ t∈T) ⇔ ∃s∃t(z=s*t ∧ s∈S ∧ t∈T ∧ (s≠0 ∨ s=0)) ⇔ ∃s∃t(z/s=t ∧ s∈S ∧ t∈T) ∨ ∃s∃t(z=0 ∧ s=0 ∧ s∈S ∧ t∈T) ⇔ ∃s(s∈S ∧ z/s∈T) ∨ (z=0 ∧ 0∈S ∧ T≠{})のように選言とな…

本日のC.A.D.

複素平面上の 2 つの集合 S,T に対して,集合 { s*t ; s∈S,t∈T }(S,T の積)を求めるのが今回の話題です.この集合に z が属する条件の複素変数での定式化 ∃s∃t(z=s*t ∧ s∈S ∧ t∈T) ……… (1) は,S,T に対して対称ですが,例えば,T が ¬(0∈T) を満…

本日のC.A.D.

? f(x)=x^3+3*x^2-9*x; ? g=strjoin(["y<x,x<a",concat([f(x),">",((x-y)*f(a)+(a-x)*f(y))/(a-y)])],",") %2 = "y<x,x<a,x^3+3*x^2-9*x>(y^2+(a+3)*y+(a^2+3*a-9))*x+(-a*y^2+(-a^2-3*a)*y)" ? tst12([all,all],[a,x,y],(f1,f2,f3)->imp(f1*f2,f3),g);Ans() *** using Lazard's method (MPP17). [y,2] [x</x,x<a,x^3+3*x^2-9*x></x,x<a",concat([f(x),">…

本日のC.A.D.

Kahan’s ellipse problem (SIGSAM Bulletin, 9, 11, 1975) 楕円周が単位開円板に含まれるための条件a^2>0 ∧ b^2>0 ∧ ∀x∀y({(x-c)^2}/{a^2}+{(y-d)^2}/{b^2}=1 → x^2+y^2<1) を a^2,b^2,c^2,d^2 についての多項式による不等式の連言で表すには少なくと…

msolve

julia> using GroebnerBasis, Singular julia> R, (a, b, c) = PolynomialRing(QQ, ["a", "b", "c"]); julia> I(n) = Ideal(R, [(a+b)^n+c-3, (b+c)^n+a-2, (2*c+a)^n+b-1]); julia> for n = 5:15 print(n,":"); @time msolve(I(n), get_param = true) end; …

MomentTools

_ _ _(_)_ | Documentation: https://docs.julialang.org (_) | (_) (_) | _ _ _| |_ __ _ | Type "?" for help, "]?" for Pkg help. | | | | | | |/ _` | | | | |_| | | | (_| | | Version 1.6.0 (2021-03-24) _/ |\__'_|_|_|\__'_| | Official https://jul…