Постоянная Каталана как определённый интеграл

[Pedja]

Привет!
Может кто-нибудь доказать следующую формулу:

$$G=-\int\limits_{0}^{\frac{\pi}{2}}\ln\left(2\sin \frac{x}{2}\right)\, dx$$

где $G$ - постоянная Каталана
Численное вычисление: SageMathCell

[Aritaborian]

Вы приводите численное вычисление в одной СКА, тогда я приведу вам символьное в другой (Mathematica):

In[1]:= -Integrate[Log[2 Sin[x/2]], {x, 0, \[Pi]/2}] == Catalan
Out[1]= True

Устроит такое доказательство?

[zykov]

Или wolframalpha.

[Pedja]

Aritaborian в сообщении #1540885 писал(а):

Устроит такое доказательство?

Я ищу строгое математическое доказательство.

[Someone]

Pedja в сообщении #1540900 писал(а):

Я ищу строгое математическое доказательство.

А как у Вас определяется постоянная Каталана?

[Pedja]

Someone в сообщении #1540924 писал(а):

А как у Вас определяется постоянная Каталана?

$$G=\displaystyle\sum_{n=0}^{\infty}\frac{(-1)^n}{(2n+1)^2}$$

[zykov]

В энциклопедии вольфрама (https://mathworld.wolfram.com/CatalansConstant.html) эта формула идёт под номером [38] и дана ссылка "Borwein et al. (2004, p. 106)".

[Someone]

Ага. Это, если не ошибаюсь, стандартное определение.
Этот ряд получается интегрированием функции $\frac{\arctg x}x$ от $0$ до $1$ разложением в степенной ряд. Можно попробовать преобразовать один интеграл в другой какой-нибудь заменой переменной…

[Pedja]

@Someone Спасибо.

[MetaMorphy]

Можно использовать равенство (при $|r|<1$)

$$\ln(1-2r\cos x+r^2)=\ln\big[(1-re^{ix})(1-re^{-ix})\big]=-2\sum_{n=1}^\infty\frac{r^n}{n}\cos nx,$$

интегрирование которого по $x\in(0,\pi/2)$ даёт

$$\int_0^{\pi/2}\ln(1-2r\cos x+r^2)\,dx=-2\sum_{n=1}^\infty\frac{r^n}{n^2}\sin\frac{n\pi}{2}=-2\sum_{n=0}^\infty\frac{(-1)^n r^{2n+1}}{(2n+1)^2},$$

и остаётся выполнить предельный переход $r\to1$ (теоремой об ограниченной сходимости, например).