MathGroup Archive 2007

[Date Index] [Thread Index] [Author Index]

Search the Archive

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:
  • Prev by Date: Re: Re: Cantor Function problem
  • Next by Date: Re: Integrate (a curious result)
  • Previous by thread: verification
  • Next by thread: Re: verification