pi_gt_sqrtTwoAddSeries — Mathlib

English

For every natural n, 2^(n+1) · √(2 − sqrtTwoAddSeries(0,n)) < π.

Русский

Для каждого натурального n верно: 2^(n+1) · √(2 − sqrtTwoAddSeries(0,n)) < π.

LaTeX

$$$\forall n \in \mathbb{N}: 2^{n+1} \cdot \sqrt{2 - \sqrtTwoAddSeries(0,n)} < \pi$$$

Lean4

theorem pi_gt_sqrtTwoAddSeries (n : ℕ) : 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π :=
  by
  have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π :=
    by
    rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
    focus
      apply sin_lt
      apply div_pos pi_pos
    all_goals apply pow_pos; norm_num
  refine lt_of_le_of_lt (le_of_eq ?_) this
  rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]; simp

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