Recenty in sci.math.symbolic there was a question if
b^2 >= (a - c)^2 AND a^2 >= b^2 implies
c^2 >= (a + b)^2 OR c^2 >= (a - b)^2
That can be solved using CAD, a shown in attachement.
--
Waldek Hebisch
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/fricas-devel/ZPI1xegGEArMaNaM%40mail.math.uni.wroc.pl.
-- We want to show that:
-- b^2 >= (a - c)^2 AND a^2 >= b^2
-- implies:
-- c^2 >= (a + b)^2 OR c^2 >= (a - b)^2
-- where ">=" denotes "greater or equal"?
rC := RealClosure(Fraction(Integer))
pR := POLY(rC)
-- Replace inequalies by differences of sides
lp := [b^2 - (a - c)^2, a^2 - b^2, c^2 - (a + b)^2, c^2 - (a - b)^2]
-- Do CAD
cd := cylindricalDecomposition(lp::List(pR)
)$CylindricalAlgebraicDecompositionPackage(rC)
-- If implication is false, then there is opposite strict ineqality
-- in the last two inequalities. Hence, there is counterexample where
-- all inequalities are strict. Consequently, it is enough to look
-- only at cells of full dimension.
cd3 := [ce for ce in cd | dimension(ce) = 3];
sp3 := [samplePoint(ce) for ce in cd3]::List(List(Fraction(Integer)))
vll := [map(p +-> eval(p, [a, b, c], pp), lp) for pp in sp3];
vlq := vll::List(List(Fraction(Integer)))
good := true
-- Loop to check validity of formula at each sample point
for vl in vlq repeat
if vl(1) > 0 and vl(2) > 0 and vl(3) < 0 and vl(4) < 0 then
good := false
print good
