integral_cos_pow_pos — Mathlib

English

For any natural n, the integral of cos^n on [0, π/2] is strictly positive: 0 < ∫_0^{π/2} cos^n x dx.

Русский

Для любого натурального n интеграл cos^n на отрезке [0, π/2] strictly положителен.

LaTeX

$$$0 < \int_{0}^{\frac{\pi}{2}} \cos^{n} x \, dx$$$

Lean4

theorem integral_cos_pow_pos (n : ℕ) : 0 < ∫ x in (0 : ℝ)..π / 2, cos x ^ n :=
  (integral_cos_pow_eq n).symm ▸ mul_pos one_half_pos (integral_sin_pow_pos _)

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