cos_pi_over_two_pow — Mathlib

English

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

Русский

Для каждого n ∈ ℕ косинус π / 2^(n+1) равен sqrtTwoAddSeries 0 n делить на 2.

LaTeX

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

Lean4

@[simp]
theorem cos_pi_over_two_pow : ∀ n : ℕ, cos (π / 2 ^ (n + 1)) = sqrtTwoAddSeries 0 n / 2
  | 0 => by simp
  | n + 1 => by
    have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero
    have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A
    have C : 0 < π / 2 ^ (n + 1) := by positivity
    rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries, add_div_eq_mul_add_div,
        one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self] <;>
      linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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