sin_sq_pi_over_two_pow

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.sin_sq_pi_over_two_pow

English

For all n ∈ ℕ, sin(π / 2^(n+1))^2 = 1 - ( sqrtTwoAddSeries 0 n / 2 )^2.

Русский

Для каждого n ∈ ℕ выполнено: sin(π / 2^(n+1))^2 = 1 - ( sqrtTwoAddSeries 0 n / 2 )^2.

LaTeX

$$$\\sin\\left(\\frac{\\pi}{2^{n+1}}\\right)^2 = 1 - \$\\frac{\\sqrtTwoAddSeries(0,n)}{2}\$^{2}$$$

Lean4

theorem sin_sq_pi_over_two_pow (n : ℕ) : sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2 := by
  rw [sin_sq, cos_pi_over_two_pow]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru