integral_sin_pow_pos — Mathlib

English

The map n ↦ ∫_0^π sin^n x dx is antitone; i.e., increasing n does not increase the integral.

Русский

Функция n ↦ ∫_0^π sin^n x dx убывающая по возрастанию n.

LaTeX

$$$$\\text{Antitone} \\quad f(n)=\\int_{0}^{\\pi} \\sin^{n}x\\,dx, \\quad n\\in\\mathbb{N}.$$$$

Lean4

theorem integral_sin_pow_pos : 0 < ∫ x in 0..π, sin x ^ n := by
  rcases even_or_odd' n with ⟨k, rfl | rfl⟩ <;> simp only [integral_sin_pow_even, integral_sin_pow_odd] <;>
        refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_) <;>
      norm_cast <;>
    omega

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