sin_sq_pi_over_two_pow_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sin_sq_pi_over_two_pow_succ (n : ℕ) : sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4 :=
  by
  rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
  · congr
    · norm_num
    · norm_num
  · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)

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