Re: verification
- To: mathgroup at smc.vnet.net
- Subject: [mg74718] Re: [mg74701] verification
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Mon, 2 Apr 2007 06:53:55 -0400 (EDT)
- References: <200704010815.EAA07245@smc.vnet.net>
On 1 Apr 2007, at 09:15, dimitris wrote:
> Hello.
>
>
> foo = {ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 -
> 4*I])] + ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])], ArcTan[3] + ArcTan[5] +
> ArcTan[41/3] + ArcTan[21], 2*Pi - ArcTan[1/4] - ArcTan[5/12]};
>
> The elements of foo list are equal
>
> Chop[N[foo, 30]]
> {5.64341552435296080601310475496,5.64341552435296080601310475496,5.\
> 64341552435296080601310475496}
>
> Block[{Message}, FullSimplify[foo[[2]] == foo[[3]]]]
> Block[{Message}, FullSimplify[foo[[1]] == foo[[3]]]]
> Block[{Message}, FullSimplify[foo[[1]] == foo[[2]]]]
>
> True
> ArcCot[4] + ArcTan[5/12] + ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/
> (1 + Sqrt[-15 - 4*I])] + ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])] == 2*Pi
> ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 - 4*I])] +
> ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])] == ArcTan[3] + ArcTan[5] +
> ArcTan[41/3] + ArcTan[21]
>
> In one of my attempts to show that foo[[1]]=foo[[3]] and
> foo[[1]]=foo[[2]] I try
>
> Block[{Message}, (FullSimplify[#1, ComplexityFunction -> LeafCount]
> & )
> [foo[[1]] == foo[[3]]]]
> Block[{Message}, (FullSimplify[#1, ComplexityFunction -> LeafCount]
> & )
> [foo[[1]] == foo[[2]]]]
>
> 2*Pi + ArcTan[8/(-1 + Sqrt[-15 - 4*I])] + ArcTan[8/(-1 + Sqrt[-15 +
> 4*I])] ==
> ArcCot[4] + ArcTan[5/12] + ArcTan[8/(1 + Sqrt[-15 - 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])]
> ArcTan[8/(1 + Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 + 4*I])] ==
> ArcTan[3] + ArcTan[5] + ArcTan[41/3] + ArcTan[21] + ArcTan[8/(-1 +
> Sqrt[-15 - 4*I])] + ArcTan[8/(-1 + Sqrt[-15 + 4*I])]
>
> but I failed.
>
> Introducing the following ComplexityFunction
>
> lst = Alternatives @@ Replace[ToExpression[Names["Arc*"]], x_ -> _x,
> -1]
> _ArcCos | _ArcCosh | _ArcCot | _ArcCoth | _ArcCsc | _ArcCsch | _ArcSec
> | _ArcSech | _ArcSin | _ArcSinh | _ArcTan | _ArcTanh
>
> I got
>
> TimeConstrained[Block[{Message}, (FullSimplify[#1,
> ComplexityFunction -
>> (Count[{#1}, lst, Infinity] & )] & )[
> foo[[1]] == foo[[3]]]], 300]
> $Aborted
>
> TimeConstrained[Block[{Message}, (FullSimplify[#1,
> ComplexityFunction -
>> (Count[{#1}, lst, Infinity] & )] & )[
> foo[[1]] == foo[[2]]]], 300]
> 0 == 4*Pi + 2*Log[(825/2873 - (2752*I)/2873)^(-(I/2))] + I*Log[-(((-1
> - 8*I) + Sqrt[-15 - 4*I])/(1 - Sqrt[-15 - 4*I]))] -
> I*Log[-(((-1 + 8*I) + Sqrt[-15 - 4*I])/(1 - Sqrt[-15 - 4*I]))] -
> I*Log[((1 - 8*I) + Sqrt[-15 - 4*I])/(1 + Sqrt[-15 - 4*I])] +
> I*Log[((1 + 8*I) + Sqrt[-15 - 4*I])/(1 + Sqrt[-15 - 4*I])] +
> I*Log[-
> (((-1 - 8*I) + Sqrt[-15 + 4*I])/(1 - Sqrt[-15 + 4*I]))] -
> I*Log[-(((-1 + 8*I) + Sqrt[-15 + 4*I])/(1 - Sqrt[-15 + 4*I]))] -
> I*Log[((1 - 8*I) + Sqrt[-15 + 4*I])/(1 + Sqrt[-15 + 4*I])] + I*Log[((1
> + 8*I) + Sqrt[-15 + 4*I])/(1 + Sqrt[-15 + 4*I])]
>
>
> Having failed also in similar attempts I would really appreciate any
> ideas!
>
> Dimitris
>
>
In fact it is quite easy to prove using Mathematica that all the
elements of foo must be equal although it needs a little human
intervention.
foo = {ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 -
4*I])] + ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
ArcTan[8/(1 + Sqrt[-15 + 4*I])], ArcTan[3] + ArcTan[5] +
ArcTan[41/3] + ArcTan[21], 2*Pi - ArcTan[1/4] - ArcTan[5/12]};
FullSimplify[Tan[foo[[2]]]-Tan[foo[[3]]]]
0
Since both foo[[2]] and foo[[3]] are real, in order to have equal
values of Tan they must differ by a multiple of Pi but:
Abs[foo[[2]]-foo[[3]]]<Pi
True
Essentially in the same way we can prove that foo[[1]] == foo[[2]].
Mathematica does not seem to be able to verify symbolically that foo
[[1]] is real, however, from defintion of Tan we know that it is
impossible for a non-real and real numbers to have equal values of
Tan, but
FullSimplify[Tan[foo[[1]]]-Tan[foo[[2]]]]
0
so foo[[1]] is also real. Exactly as above, we only need to check that
Abs[foo[[1]]-foo[[2]]]<Pi
True
That shows that they are the elements of the list foo are equal real
numbers.
Andrzej Kozlowski
- References:
- verification
- From: "dimitris" <dimmechan@yahoo.com>
- verification