Theorems · Theorem · real analysis

integral_mul_rpow_one_add_sq

∀ {a b t : ℝ},
  t ≠ -1 →
    ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t =
      (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))

Defined in

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Cited by

0 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound