由一点到抛物线两条切线长 不等式

hbghlyj

hbghlyj

设切点为$(x_1,x_1^2)$

In[1]:=
      CoefficientList[Resultant[y0 + x1^2 - 2 x0 x1, (x0 - x1)^2 + (y0 - x1^2)^2 - t, x1], t]
Out[1]:=
      $\left\{x_0^4+16 x_0^6-2 x_0^2 y_0-40 x_0^4 y_0+y_0^2+32 x_0^2
   y_0^2+16 x_0^4 y_0^2-8 y_0^3-32 x_0^2 y_0^3+16 y_0^4,-2
   x_0^2-16 x_0^4+2 y_0+24 x_0^2 y_0-8 y_0^2,1\right\}$
In[2]:=
      Refine[Resolve[Exists[{x0, y0},
                                     y0 <= x0^2 && p == -%[[2]] && q == %[[1]]
                                     ],
                                       {p, q}, Reals], Assumptions -> p > 0]
Out[2]:=
      $\displaystyle\frac{\sqrt{262144 p^3+110592 p^2+15552 p+729}}{2048}-\frac{9 (32 p+3)}{2048}\leq q\leq \frac{p^2}{4}$

hbghlyj

证明:$$\frac{(64 p+9)^{3/2}-9 (32 p+3)}{2048}\leq q$$
$$⇔(9 (32 p + 3) + 2048 q)^2 - (9 + 64 p)^3≥0$$
\begin{aligned}⇔262144 \left(8 y_0-1\right){}^2 \left(x_0^2-y_0\right){}^3 \left(64 x_0^2 y_0^2-176 x_0^2 y_0+128 x_0^4+13 x_0^2-64 y_0^3+48 y_0^2-12 y_0+1\right)≥0\end{aligned}
而$x_0^2-y_0≥0$,只需证$$64 x_0^2 y_0^2-176 x_0^2 y_0+128 x_0^4+13 x_0^2-64 y_0^3+48 y_0^2-12 y_0+1≥0$$令$r=x_0^2-y_0$,展开得$$128 r^2+64 r y_0^2+80 r y_0+13 r+y_0+1≥0$$
显然成立.

hbghlyj

有了式子以后,证明不难.关键是怎么得到那个式子.
Mathematica应该是使用Cylindrical Decomposition得到的那个式子.