Euler's formula for product of cosines

According to "Squaring the Circle" by Ernest Hobson, this formula $$\theta =\frac{\sin\theta}{\cos\frac\theta2\cdot \cos\frac\theta4\cdot \cos\frac\theta8\dots}$$ for $\theta<\pi$ is due to Euler. He gives no reference.

Does anyone knows the reference to the original Euler's work?

1. Likely the formula was obtained by applying $$\sin(2{\cdot}x)=2\cdot\sin x\cdot \cos x$$ recursively. (It seems to be the easiest way.) If you plug in $\theta=\tfrac\pi2$ then you get the Vieta's identity $$\frac\pi2= \frac2{\sqrt{2}}\cdot \frac2{\sqrt{2+\sqrt2}}\cdot \frac2{\sqrt{2+\sqrt{2+\sqrt2}}} \ldots$$ This formula seems to be the first known "explicit" expression for $\pi$.

2. So far it seems that Hobson (and others after Hobson, including Cajori) made a mistake by attributing this formula to Euler.

Here's a link to Jordan Bell's English translation of Euler's original paper, "Various observations on angles proceeding in geometric progression". Euler begins exactly as the OP outlines, starting from the double-angle formula for sine. By the second page he has given the following version of the OP's formula:

Therefore the arc $$s$$ itself can be very prettily defined by its sine and the cosines of arcs continually diminished in double ratio, as $$s = \frac{\sin. s}{\cos. \frac{1}{2}s \cos. \frac{1}{4}s \cos. \frac{1}{8}s \cos. \frac{1}{16}s \cos. \frac{1}{32}s \cdot \operatorname{etc.}}$$

However, Alexandre Eremenko's answer makes a lot of sense, especially since from a modern perspective, we know the infinite product formulas

\begin{align*} \cos \frac{x}{2} = &\prod_{n=0}^\infty \left( 1 - \frac{x^2}{\pi^2 (2n+1)^2} \right), \\ \frac{\sin x}{x} = &\prod_{k=0}^\infty \left( 1 - \frac{x^2}{\pi^2 k^2} \right). \ \end{align*}

Clearly in the second product, every integer $$k \geq 1$$ can be expressed as a product $$k = (2n+1) 2^m$$ for unique nonnegative integers $$n, m \geq 0,$$ so we find

\begin{align*} \frac{\sin x}{x} = &\prod_{k=0}^\infty \left( 1 - \frac{x^2}{\pi^2 k^2} \right) \\ = &\prod_{m=0}^\infty \prod_{n=0}^\infty \left( 1 - \frac{x^2}{\pi^2 (2^m (2n+1))^2} \right) \\ = &\prod_{m=0}^\infty \cos \left( \frac{x}{2^{m+1}}\right) \\ =& \cos \frac{x}{2} \cos \frac{x}{4} \cos \frac{x}{8} \cos \frac{x}{16}... \ \end{align*}

It's not clear to me why "one should be mad" to discover or prove the identity this way.

In fact, Euler did know the infinite product formula $$\frac{\sin x}{x} = \prod_{k=0}^\infty \left( 1 - \frac{x^2}{\pi^2 k^2} \right),$$ although per heropup's answer linking to an old Ed Sandifer article, Euler never actually proved this formula rigorously.
In his paper "On the sums of series of reciprocals" (again translated by Jordan Bell), Euler used it to calculate various specific series of the form $$\sum_{n=1}^\infty \frac{1}{n^{2p}}$$, including the first solution to the Basel problem.
In Euler's notation below (from p. 6 of Bell's translation), $$p$$ means $$\pi$$, $$s$$ is an angle (or "arc"), and $$y$$ represents $$\sin s$$:

And on the next page, Euler states that $$\sum_{n=1}^\infty \frac{1}{n^2} = \frac{\pi^2}{6}$$:

This formula is an immediate consequence of the product expansion of the sine: $$\frac{\sin x}{x}=\prod_{n=1}^\infty\left(1-\frac{x^2}{\pi^2n^2}\right),$$ and of the well-known fact that every integer is a product of a power of $2$ and an odd integer.

The infinite product formula for the sine was proved by Euler in De summis serierum reciprocarum, Comment. Acad. Sci. Petrop. 7 (1740), 123– 134. (Read Dec. 5, 1735). (Opera Omnia, Series 1, Vol. 14, pp. 73–86.) The formula can be seen in paragraph 5 of Euler's work.

A good source for Euler's work on this subject is the survey of Lagarias Euler's constant: Euler's work and modern development, in the Bulletin AMS. 50, 4 2013, 527-628.

• I doubt that this is correct reference. The formula I am asking about is an immediate consequence of $$\sin (2{\cdot} x)=2\cdot\sin x\cdot\cos x.$$ One should be mad to get the formula the way you suggest. Nov 30 '15 at 10:42
• @Anton Petrunin: Your argument is very close to the original Vieta's proof, which is reproduced on p. 92 of Beckman, Hostory of pi. So perhaps the result should be credited to Vieta rather than Euler. Nov 30 '15 at 14:32

The formula Hobson is reporting on is unrelated to Euler's famous infinite product formula for sine. The constants in Hobson's formula vary geometrically whereas in Euler's famous product formula they vary quadratically. The latter result is considerably deeper than the former (though perhaps the former is also due to Euler). A discussion of the famous formula can be found in our Notices article here: http://www.ams.org/notices/201307/rnoti-p886.pdf