sin_pi_over_two_pow_succ — Mathlib

English

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

Русский

Для всех n ∈ ℕ: sin(π / 2^(n+2)) = sqrt(2 - sqrtTwoAddSeries 0 n) / 2.

LaTeX

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

Lean4

@[simp]
theorem sin_pi_over_two_pow_succ (n : ℕ) : sin (π / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2 :=
  by
  rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow, sin_sq_pi_over_two_pow_succ, sub_mul]
  · congr <;> norm_num
  · rw [sub_nonneg]
    exact (sqrtTwoAddSeries_lt_two _).le
  refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two
  · positivity
  · exact div_le_self pi_pos.le <| one_le_pow₀ one_le_two

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