integral_cos_pow_three — Mathlib

English

The integral of cos^3 can be expressed as above; it equals sin a − sin b − (sin^3 a − sin^3 b)/3.

Русский

Интеграл cos^3 может быть записан как выше; равен sin a − sin b − (sin^3 a − sin^3 b)/3.

LaTeX

$$$$\\displaystyle \\int_{a}^{b} \\cos^{3}x \\,dx = \\sin a - \\sin b - \\frac{\\sin^{3}a - \\sin^{3}b}{3}. $$$$

Lean4

@[simp]
theorem integral_cos_pow_three : ∫ x in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3 :=
  by
  have := @integral_sin_pow_mul_cos_pow_odd a b 0 1
  norm_num at this; exact this

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