Solving Unsolved Trig Identity: sum[0 to x](sin(x))=180 * sin(x/2)^2 + sin(x)/2

[crash_matrix]

Hey guys,
I stumbled on an interesting and unexpected identity when looking for a simpler summation technique for inverse kinementics. Basically, I was trying to find a simpler way of summing IK vectors for some particular armature (like a tentacle or multi-branch armature on a robot). This question doesn't have to do with IK, but I accidentally calculated an identity rule I've not been able to attach to any other identity rule in trigonometry. This is the XPlore code that graphs the identity:
[The trig set is in degrees, not radians]

f(x)=sum(sin(t),t=0 to x step 1)
(Period,C)=(180,f(180))
g(x)=C*sin(x/2)^2+sin(x)/2
graph((f(x),g(x)),x=0 to Period)

When running those lines in XPlore (or any graphing calculator), you'll find that as the "step" value in the first line approaches zero, the two curves become equal. I've tested this rule across hundreds of different data sets and it always diverges perfectly, regarless of the precision of the calculator.
My question is: Is there an existing trig identity or rule (or set of iedntities or rules) that explains why the above functional set works?
Basically the "law" that it asserts is:

sum[0 to x](sin(x))=180 * sin(x/2)*sin(x/2) + sin(x)/2
where x is in degrees

I've looked up every trig and calculus identity and "rule" that I can find and I can't match it to anything.
It's not an important question, just something that's been bugging me for a while.

Thanks for looking,
--CM

 

[dodo]

sum[0 to x](sin(x))=180 * sin(x/2)*sin(x/2) + sin(x)/2
where x is in degrees

Didn't you mean f(180), instead of 180, above? f(180) being the sum[t=0 to 180](sin(t)).

Also, to avoid confusing the two meanings of 'x', you may want to express the left-hand side as sum[t=0 to x](sin(t)) ; 'x' is the limit of the sum, not really the argument to sin().

The x's in the right-hand side are correct, as they mean the same value of 'x' as the limit of the sum in the left-hand side.

So, if I get you right, the conjecture is$$\sum_{t=0}^x \sin t = \left( \sum_{t=0}^{180} \sin t \right) \sin^2(x/2) + (\sin x)/2$$with the arguments in degrees, not radians.

The two overlapping curves (left-hand side, right-hand side) looking like this, for x=0 to 180:
http://205.196.120.39/598b993ef2cba10162b685226796555be3a77674f71a36dcbc42144e3185d7bd5g.jpg

 

[sachav]

Hi,

sum[0 to x](sin(x))=180 * sin(x/2)*sin(x/2) + sin(x)/2

I'm guessing you meant :

sum[k=0 to x](sin(k))=f(180)*sin(x/2)*sin(x/2) + sin(x)/2

If you're interested in a proof, here you go.

Let $x \in \mathbb R, n \in \mathbb N$.
I'll be using radians instead of degrees, so I'll show that we have :
$$\sum_{k=0}^n \sin k = f(\pi) \sin^2\left(\dfrac{x}{2}\right)+\dfrac{\sin x}{2}$$
Where : $f(n) = \displaystyle\sum_{k=0}^n \sin k$ (NB: that expression isn't yet defined on all real numbers and more particularly on $n=\pi$, but it will be as soon as we get another expression of it).


We have :
$$f(n) = \sum_{k=0}^n \text{Im}(e^{ik}) = \text{Im}\left(\sum_{k=0}^n e^{ik}\right) = \text{Im}\left(\sum_{k=0}^n (e^{i})^k\right)$$
And since $e^i \neq 1$, applying the formula for the sum of a geometric sequence gives :

$$f(n) = \text{Im}\left(\dfrac{(e^i)^{n+1}-1}{e^i-1}\right) = \text{Im}\left(\dfrac{e^{i(n+1)}-1}{e^i-1}\right)$$
By applying half angle formulas :

$$f(n) = \text{Im}\left(\dfrac{e^{i(n+1)/2}\cdot 2i\sin\left(\dfrac{n+1}{2}\right)}{e^{i/2}\cdot 2i\sin(1/2)}\right)$$

After simplifying we finally get :

$$f(n) = \dfrac{\sin\left(\dfrac{n+1}{2}\right) \sin\left(\dfrac{n}{2}\right)}{\sin\left(\dfrac{1}{2}\right)}$$

That's a quite "simple" expression that only uses products, that naturally extends $f(n)$ to real numbers. I'll now show that the quantity $f(x)$ is exactly equal to $f(\pi) \sin^2\left(\dfrac{x}{2}\right) + \dfrac{\sin x}{2}$ for all $x \in \mathbb R$.

According to the expression of $f(x)$ obtained above, we have :
$$f(\pi) = \dfrac{\sin\left(\dfrac{\pi+1}{2}\right) }{\sin\left(\dfrac{1}{2}\right)} = \dfrac{\cos\left(\dfrac{1}{2}\right)}{\sin\left( \dfrac{1}{2}\right)}$$

Thus :
$$f(\pi) \sin^2\left(\dfrac{x}{2}\right) + \dfrac{\sin x}{2} = \dfrac{\cos\left(\dfrac{1}{2}\right)\sin^2\left( \dfrac{x}{2}\right) }{\sin\left( \dfrac{1}{2}\right)}+\dfrac{\sin x}{2} = \\ \dfrac{2\cos\left( \dfrac{1}{2}\right)\sin^2\left( \dfrac{x}{2}\right) + \sin\left( \dfrac{1}{2}\right)\left[2\sin\left(\dfrac{x}{2}\right)\cos\left( \dfrac{x}{2}\right)\right]}{2\sin\left( \dfrac{1}{2}\right)} = \\\dfrac{\sin\left(\dfrac{x}{2}\right)\left[\cos\left(\dfrac{1}{2}\right) \sin\left(\dfrac{x}{2}\right) + \sin\left(\dfrac{1}{2}\right)\cos\left(\dfrac{x}{2}\right)\right]}{\sin\left(\dfrac{1}{2}\right)} = \\\dfrac{\sin\left(\dfrac{x}{2}\right) \sin\left(\dfrac{x+1}{2}\right)}{\sin\left(\dfrac{1}{2}\right)} = f(x)$$

You just need to change from radians to degrees and it's done.

 

[dodo]

We have :
$$f(n) = \sum_{k=0}^n \text{Im}(e^{ik}) = \text{Im}\left(\sum_{k=0}^n e^{ik}\right) = \text{Im}\left(\sum_{k=0}^n (e^{i})^k\right)$$
And since $e^i \neq 1$, applying the formula for the sum of a geometric sequence gives :

$$f(n) = \text{Im}\left(\dfrac{(e^i)^{n+1}-1}{e^i-1}\right) = \text{Im}\left(\dfrac{e^{i(n+1)}-1}{e^i-1}\right)$$

This is a good one, congrats... I was scratching my head on how to treat these sums.

Edit:
On second thought, the technique is beautiful but there has to be an error here. $\sum_{k=0}^n \text{Im}(e^{ik})$ is not the same as $\sum_{k=0}^n \text{Im}(e^{ik \pi/180})$, which was what the OP had in mind, regardless of whether you later extend the definition for a real n: "mind the step" !

Edit2:
Ah, you already said that. "You just need to change from radians to degrees and it's done." - i.e. Repeat the proof, this time with a pi/180 multiplier. When will I learn to read posts to the end.

 

[dodo]

So, if I followed right, you end up with$$f(n) = \frac{\sin\left(\frac{\pi n}{360}\right) \sin\left(\frac{\pi(n+1)}{360}\right)} {\sin\left(\frac{\pi}{360}\right)}$$which, after expanding the sum of sines, and using a half-angle formula again, ends up in$$f(n) = \frac{\sin^2\left(\frac{\pi n}{360}\right)}{\tan\left(\frac{\pi}{360}\right)} + \frac{\sin\left(\frac{\pi n}{180}\right)}2$$so that$$f(180) = \frac 1 {\tan\left(\frac{\pi}{360}\right)}$$from which the conjecture$$f(n) = f(180) \sin^2(\pi n/360) + (\sin \pi n/180)/2$$follows.