Mathematica为什么算不出最后的结论 - 第2页 - 数学软件 - 数学研发论坛

dlsh 发表于 2021-10-6 22:37:00

从上面的程序中的结果人工变形后，可以利用向量商证明有关结论。当然，纯几何方法不难。
$\frac{b - d}{b - c}=\frac{1}{(-1 + a o2)^2}，可变换为\frac{b - d}{b - c}=\frac{1}{a^2(1/a -o2)^2}=\frac{b^2}{(b -o2)^2}$
即$\frac{\overrightarrow{BD}}{\overrightarrow{BC}}=(\frac{\overrightarrow{O_1B}}{\overrightarrow{O_2B}})^2,易于推出比值等于半径平方，∠DBC=2∠O_2BO_1$

TSC999 发表于 2021-10-6 23:16:31

本帖最后由 TSC999 于 2021-10-6 23:59 编辑

由于 mathematica 处理复数的能力十分有限，有时算式中不可避免的会有根式，咋办？我想到一个折中的方法，就是直角坐标与复数坐标相结合。
程序运行后所显示的坐标虽然是复数，但是实部与虚部是分开的。 mathematica 对于这种复数的处理能力还是不错的，有根式也不怕，下面的程序不用 1 秒钟就可运行完毕。
为什么要结合复数？因为坐标的复数表达式有许多是已知的，其表达式很简单。下面程序中的复数坐标公式是由楼主 dlsh 提供的，程序中直接引用了。
关于程序中的共轭复数，并不需要对每一个点都计算其共轭复数，只有当算式中出现共轭复数时，才有必要计算其共轭复数，否则无须计算。

Clear["Global`*"];
XA = (-R^2 + u^2 + 1)/(
2 u); YA = Sqrt[-R^4 + 2 R^2 (u^2 + 1) - (u^2 - 1)^2]/(2 u); a =
XA + I YA;
XB = (-R^2 + u^2 + 1)/(
2 u); YB = -(Sqrt[-R^4 + 2 R^2 (u^2 + 1) - (u^2 - 1)^2]/(2 u)); b =
XB + I YB;
\!$\*OverscriptBox[\(b$, $_$]\) = XB - I YB;
XO1 = 0; YO1 = 0;XO2 = u; YO2 = 0;o1 = XO1 + I YO1; o2 =
XO2 + I YO2;

d = Simplify[(a - u)/(1 - a u)] ;
XD = Factor@
Together@
ComplexExpand@
   Re -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
YD = Factor@
Together@
ComplexExpand@
   Im -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
d = Simplify + I Simplify;
c = Simplify;
XC = Factor@
Together@
ComplexExpand@
   Re -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
YC = Factor@
Together@
ComplexExpand@
   Im -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
c = Simplify + I Simplify;
e = Simplify[(c - u)/(b (
\!$\*OverscriptBox[\(b$, $_$]\) - u))];
XE = Factor@
Together@
ComplexExpand@
   Re -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
YE = Factor@
Together@
ComplexExpand@
   Im -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
e = Simplify + I Simplify;
f = Simplify[b d (
\!$\*OverscriptBox[\(b$, $_$]\) - u) + u];
XF = Factor@
Together@
ComplexExpand@
   Re -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
YF = Factor@
Together@
ComplexExpand@
   Im -> v] /.
v -> Sqrt[-R^4 + 2 (u^2 + 1) R^2 - (u^2 - 1)^2];
f = Simplify + I Simplify;
m = Simplify@
Solve[{(y - YA)/(x - XA) == (y - YD)/(x - XD), (y - YE)/(
   x - XE) == (y - YO1)/(x - XO1)}, {x, y}];
XM = Part, 1], 2];
YM = Part, 2], 2];
m = XM + I YM;
n = Simplify@
Solve[{(y - YA)/(x - XA) == (y - YC)/(x - XC), (y - YF)/(
   x - XF) == (y - YO2)/(x - XO2)}, {x, y}];
XN = Part, 1], 2];
YN = Part, 2], 2];
n = XN + I YN;
q = Simplify@
Solve[{x == XA, (y - YM)/(x - XM) == (y - YN)/(x - XN)}, {x, y}];
XQ = Part, 1], 2];
YQ = Part, 2], 2];
q = XQ + I YQ;
Print["a = ", a]; Print["b = ", b];
Print["c = ", c]; Print["d = ", d];
Print["e = ", e]; Print["f = ", f];
Print["m = ", m]; Print["n = ", n];
Print["q = ", q];
DB = Simplify]; BC =
Simplify];
MQ = Simplify]; NQ =
Simplify];
Print["DB = ", DB]; Print["BC = ", BC];
Print["MQ = ", MQ]; Print["NQ = ", NQ];
k1 = Simplify; k2 =
Simplify;
Print["DB/BC = ", k1]; Print["MQ/NQ = ", k2];
If[k1 == k2,
Print["由于二者之比都等于 1/\!$\*SuperscriptBox[\(R$, $2$]\)，所以DB/BC = \
MQ/NQ"]]

程序运行结果：

a = (-R^2+u^2+1)/(2 u)+(I Sqrt[-R^4+2 (u^2+1) R^2-(u^2-1)^2])/(2 u)

b = (-R^2+u^2+1)/(2 u)-(I Sqrt[-R^4+2 (u^2+1) R^2-(u^2-1)^2])/(2 u)

c = (I (R-u) Sqrt[-R^4+2 (u^2+1) R^2-(u^2-1)^2] (R+u))/(2 u)+(-R^4+2 u^2 R^2+R^2-u^4+3 u^2)/(2 u)

d = ((u^2-1)^2-R^2 (u^2+1))/(2 R^2 u)-(I (u-1) (u+1) Sqrt[-R^4+2 (u^2+1) R^2-(u^2-1)^2])/(2 R^2 u)

e = (I (R^2-u^2+u) Sqrt[-R^4+2 (u^2+1) R^2-(u^2-1)^2] (R^2-u (u+1)))/(2 R^2 u)+(-R^6+(3 u^2+1) R^4+(u^2-3 u^4) R^2+u^2 (u^2-1)^2)/(2 R^2 u)

f = -((I (-u^2+R u+1) Sqrt[-R^4+2 (u^2+1) R^2-(u^2-1)^2] (u^2+R u-1))/(2 R^2 u))-(u^2 R^4-(2 u^4+u^2-1) R^2+(u^2-1)^3)/(2 R^2 u)

m = (I Sqrt[-(R-u-1) (R-u+1) (R+u-1) (R+u+1)] (R^4-2 u^2 R^2+u^4-u^2))/(2 u (R^4-(2 u^2+1) R^2+(u^2-1)^2))+(-R^6+(3 u^2+1) R^4+(u^2-3 u^4) R^2+u^2 (u^2-1)^2)/(2 u (R^4-(2 u^2+1) R^2+(u^2-1)^2))

n = (I Sqrt[-(R-u-1) (R-u+1) (R+u-1) (R+u+1)] (u^4-(R^2+2) u^2+1))/(2 u (R^4-(2 u^2+1) R^2+(u^2-1)^2))+(u^2 R^4-(2 u^4+3 u^2+1) R^2+(u^2-1)^2 (u^2+1))/(2 u (R^4-(2 u^2+1) R^2+(u^2-1)^2))

q = (-R^2+u^2+1)/(2 u)+(I Sqrt[-(R-u-1) (R-u+1) (R+u-1) (R+u+1)] (R^6-2 u^2 R^4+u^2 (u^2-2) R^2+(u^2-1)^2))/(2 (R^2+1) u (R^4-(2 u^2+1) R^2+(u^2-1)^2))

DB = Sqrt[-((R^4-2 (u^2+1) R^2+(u^2-1)^2)/(R^2 u^2))]

BC = Sqrt[-((R^2 (R^4-2 (u^2+1) R^2+(u^2-1)^2))/u^2)]

MQ = Sqrt[-((R^2 (2 R^6-(5 u^2+2) R^4+(4 u^4-6 u^2-2) R^2-(u^2-2) (u^2-1)^2))/((R^2+1)^2 (R^4-(2 u^2+1) R^2+(u^2-1)^2)^2))]

NQ = Sqrt[-((R^6 (2 R^6-(5 u^2+2) R^4+(4 u^4-6 u^2-2) R^2-(u^2-2) (u^2-1)^2))/((R^2+1)^2 (R^4-(2 u^2+1) R^2+(u^2-1)^2)^2))]

DB/BC = 1/R^2

MQ/NQ = 1/R^2

由于二者之比都等于 1/R^2，所以DB/BC = MQ/NQ

creasson 发表于 2021-10-6 23:55:01

基于有理参数表示的做法

Clear["Global`*"];
(*设点*)
points = {A->0, B->1,P->(1+I p)/(1-I u), T->(1+I q)/(1-I v)};
(*在A处的切向量*)
vectors = Factor[{v1 -> Limit*u^2,u->\],v2 -> Limit*v^2,v->\]}];
(*求C,D*)
CDEQ = (Factor]]//Numerator)&/@({(T-A)/v1, (P-A)/v2}/.points/.vectors);
CDsol = Solve//Flatten;
points = Union//Factor;
(*求E,F*)
EFEQ = (Factor]]//Numerator)&/@({(P-B)/(C-B), (T-B)/(D-B)}/.points);
EFsol = Solve[[-1]];
points = Union//Factor;
(*求M,N*)
points = Union//Factor;
points = Union*D+(1-\)A, N->\*C+(1-\)A}/.points]//Factor;
MNEQ = (Factor]]//Numerator)&/@({(M-O1)/(E-O1), (N-O2)/(F-O2)}/.points);
MNsol = Solve, \}]//Flatten;
points = Factor;
(*求点Q*)
points = Union}]//Factor;
QEQ = (Factor]]//Numerator)&/@({(M-Q)/(N-Q)}/.points);
Qsol = Solve}]//Factor//Flatten;
points = Factor;
(*结论*)
squarelens = Factor^2]]&/@({B-D,B-C,Q-M,Q-N}/.points);
target = Factor[(squarelens[]/squarelens[])-(squarelens[]/squarelens[])];
(*显示*)
Print["points = ", points];
Print["target = ", target];

TSC999 发表于 2021-10-7 10:52:10

本帖最后由 TSC999 于 2021-10-7 13:07 编辑

creasson 发表于 2021-10-6 23:55
基于有理参数表示的做法

如果各点的算式表达的是点的复数坐标值，为什么与图形的实测坐标值不符合？程序中的 u代表什么？设定了 A 在坐标原点、B 的坐标是 (1, 0) 时，是否还应该再设两个圆半径为已知（或一个圆半径及两圆心的距离），才能确定其它点的坐标？
例如将a = 0; b = 1; p = 1.145;q = 0.393;代入 c = (p - q)/(p + I)中，算出 c=0.372579 -0.325397 I，不等于实际值c=1.167+1.165 I。

creasson 发表于 2021-10-7 11:45:27

TSC999 发表于 2021-10-7 10:52
如果各点的算式表达的是点的复数坐标值，为什么与图形的实测坐标值不符合？程序中的 u代表什么？...

我用的是#11的图，$p, q$为任意实数，点 $P, T$分别表示圆$O_1,O_2$上的任意点，替换为其他字母如$X,Y$ 就好。
半径$r_1= \frac{1}{2}\sqrt {1 + p^2} $, $r_2 = \frac{1}{2}\sqrt {1 + q^2} $。

本图的话，若指定A=0,B=1,C=1.167+1.165I, 则由$ (p - q)/(p + I) = 1.167+1.165I$ 解出
$ p =- 1.00172,q = 1.33229 $

TSC999 发表于 2021-10-7 13:13:29

本帖最后由 TSC999 于 2021-10-7 13:15 编辑

creasson 发表于 2021-10-7 11:45
我用的是#11的图，$p, q$为任意实数，点 $P, T$分别表示圆$O_1,O_2$上的任意点，替换为其他字母如$X,Y ...

噢，我明白了。这个设点的方法很妙啊，设了点 A、B 的坐标外，为了确定两个圆的位置以及避免运算中有根式出现，不设两个圆半径的大小，而是设 O1 的纵坐标为 p/2,O2 的纵坐标为q/2, 也就是设 p、q为已知实数。其余各点的坐标都是 p、q 的函数。

经验算，用您的各点公式求出的复数坐标值全都符合 14# 页中的图。

Clear["Global`*"];
a = 0; b = 1; p = -2*0.518; q = 2*0.649;
c = C -> (p - q)/(p + I)
D -> -((p - q)/(q + I))
E -> ((p - I) (p - q))/((p + I) (q - I))
F -> -(((p - q) (q - I))/((p - I) (q + I)))
M -> ((p - I) (p + I) (p - q) (q - I))/(
q^2 p^2 - 3 p^2 + 8 q p - 3 q^2 + 1)
N -> -(((p - I) (p - q) (q - I) (q + I))/(
q^2 p^2 - 3 p^2 + 8 q p - 3 q^2 + 1))
Q -> -(((p^2 + 1) (p - q)^2 (q^2 + 1))/((p^2 + q^2 + 2) (q^2 p^2 -
3 p^2 + 8 q p - 3 q^2 + 1)))

C->1.16627 +1.12574 I
D->1.1284 -0.869337 I
E->0.828902 -1.15843 I
F->0.791031 +1.41483 I
M->0.387154 -0.298269 I
N->0.400147 +0.386242 I
Q->0.392816

dlsh 发表于 2021-10-7 23:04:41

本帖最后由 dlsh 于 2021-10-7 23:20 编辑

主贴还是线性构造命题，用代数证明并不难，下面一段选自李涛的博士毕业论文，也是线性构造，按部就班就行了。

这些结论如果用纯几何方法是很难的。
一些非线性命题，看起来构造不难，反而很难证明。例如：
1如果三角形内角平分线相等，则它是等腰三角形。
2正方形与心脏线
正△ABC中，D、E分别是AC、BC上的一点，有AD=CE，BD与AE相交于F。∠AEC和∠CBD的平分线交点G恰好位于AC上。求证：∠ABG=∠BGF。

TSC999 发表于 2021-10-8 21:12:56

前面 creasson 先生程序是很正宗的机器证明程序。一时也学不会这个程序的编写方法，但是可以用直角坐标法来写程序，好处是编写容易，按相同套路一直走下去即可。

Clear["Global`*"];(*令O1圆圆心的纵坐标为 p/2，O2圆圆心的纵坐标为 q/2*)
(*与以往的程序不同，点的复数坐标都采用大写字母表示。这样有其好处，比如图中有 P 这个点，所以如果 P 点的复坐标用小写字母 p \
表示，那 O1 的纵坐标就不能用 p/2 表示了。当然点的复坐标都用大写字母表示也有坏处，那就是变量不得使用大写的 \
C、D、N，这几个大写字母是 mathematica 禁用的，因此这些点的复坐标可写成 CC、DD、NN，但用字符显示时仍可写 C、D、N \
*)
XA = 0; YA = 0; XB = 1; YB = 0; XO1 = 1/2; YO1 = p/2; XO2 = 1/2; YO2 =
q/2;
A = XA + I YA; B = XB + I YB;O1 = XO1 + I YO1; O2 = XO2 + I YO2;
CC = Solve[{(x - 1/2)^2 + (y - q/2)^2 == (1/2)^2 + (q/2)^2(*O2圆方程*),
y == -1/p x(*AC方程*)}, {x, y}];
XC = Part, 1], 2];
YC = Part, 2], 2];
CC = Factor@Simplify;
DD = Solve[{(x - 1/2)^2 + (y - p/2)^2 == (1/2)^2 + (p/2)^2(*O1圆方程*),
y == -1/q x(*AD方程*)}, {x, y}];
XD = Part, 1], 2];
YD = Part, 2], 2];
DD = Factor@Simplify;
Print["C = ", CC];
Print["D = ", DD];
EE = Solve[{(x - 1/2)^2 + (y - p/2)^2 == (1/2)^2 + (p/2)^2(*O1圆方程*), (
y - YC)/(x - XC) == (y - YB)/(x - XB)(*CB方程*)}, {x, y}];
XE = Part, 1], 2];
YE = Part, 2], 2];
EE = Factor@Simplify;
Print["E = ", EE];
F = Solve[{(x - 1/2)^2 + (y - q/2)^2 == (1/2)^2 + (q/2)^2(*O2圆方程*), (
y - YD)/(x - XD) == (y - YB)/(x - XB)(*DB方程*)}, {x, y}];
XF = Part, 1], 2];
YF = Part, 2], 2];
F = Factor@Simplify;
Print["F = ", F];
M = Solve[{(y - YA)/(x - XA) == (y - YD)/(x - XD)(*AD方程*), (y - YE)/(
x - XE) == (y - YO1)/(x - XO1)(*EO1方程*)}, {x, y}];
XM = Part, 1], 2];
YM = Part, 2], 2];
M = Factor@Simplify;
Print["M = ", M];
NN = Solve[{(y - YA)/(x - XA) == (y - YC)/(x - XC)(*AC方程*), (y - YF)/(
x - XF) == (y - YO2)/(x - XO2)(*FO2方程*)}, {x, y}];
XN = Part, 1], 2];
YN = Part, 2], 2];
NN = Factor@Simplify;
Print["N = ", NN];
Q = Solve[{(y - YA)/(x - XA) == (y - YB)/(x - XB)(*AB方程*), (y - YM)/(
x - XM) == (y - YN)/(x - XN)(*MN方程*)}, {x, y}];
XQ = Part, 1], 2];
YQ = Part, 2], 2];
Q = Factor@Simplify;
Print["Q = ", Q];
R1 = Simplify];
R2 = Simplify];
Print["R1 = ", R1];
Print["R2 = ", R2];
k = Simplify;
k1 = ExpandDenominator@
Together@ComplexExpand@Simplify];
k2 = ExpandDenominator@
Together@ComplexExpand@Simplify];
Print["DB/BC = ", k1];
Print["MQ/NQ = ", k2];
Print["(R1/R2\!$\*SuperscriptBox[\()$, $2$]\) = ", k];
If[k1 == k2 == k,
Print["由于 DB/BC = MQ/NQ = (R1/R2\!$\*SuperscriptBox[\()$, \
$2$]\)，所以 DB/BC = MQ/NQ"]]

程序运行结果：

C = (p-q)/(p+I)
D = (q-p)/(q+I)
E = ((p-I) (p-q))/((p+I) (q-I))
F = -(((p-q) (q-I))/((p-I) (q+I)))
M = ((p-I) (p+I) (p-q) (q-I))/(q^2 p^2-3 ^2+8 q p-3 q^2+1)
N = -(((p-I) (p-q) (q-I) (q+I))/(q^2 p^2-3 p^2+8 q p-3 q^2+1))
Q = -(((p^2+1) (p-q)^2 (q^2+1))/((p^2+q^2+2) (q^2 p^2-3 p^2+8 q p-3 q^2+1)))
R1 = Sqrt/2
R2 = Sqrt/2
DB/BC = (p^2+1)/(q^2+1)
MQ/NQ = (p^2+1)/(q^2+1)
(R1/R2)^2 = (p^2+1)/(q^2+1)
由于 DB/BC = MQ/NQ = (R1/R2)^2，所以 DB/BC = MQ/NQ

页: 1 [2]

数学研发论坛's Archiver