integral_sin_pow_succ_le — Mathlib

English

For all n, ∫_0^π sin^{n+1} x dx ≤ ∫_0^π sin^n x dx.

Русский

Для всех n: ∫_0^π sin^{n+1} x dx ≤ ∫_0^π sin^n x dx.

LaTeX

$$$$\\int_{0}^{\\pi} \\sin^{n+1}x \\,dx \\le \\int_{0}^{\\pi} \\sin^{n}x \\,dx.$$$

Lean4

theorem integral_sin_pow_succ_le : (∫ x in 0..π, sin x ^ (n + 1)) ≤ ∫ x in 0..π, sin x ^ n :=
  by
  let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)
  refine integral_mono_on pi_pos.le ?_ ?_ H <;> exact (continuous_sin.pow _).intervalIntegrable 0 π

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