English
Let a, b be real numbers and t a complex exponent with t ≠ -1. Then the integral from a to b of x times (1 + x^2)^t (viewed as a complex-valued function) equals the boundary term difference: (1 + b^2)^{t+1}/(2(t+1)) − (1 + a^2)^{t+1}/(2(t+1)).
Русский
Пусть a, b ∈ ℝ и t ∈ ℂ с t ≠ −1. Тогда интеграл по x от a до b от x(1 + x^2)^t (комплекснозначная функция) равен разности: (1 + b^2)^{t+1}/(2(t+1)) − (1 + a^2)^{t+1}/(2(t+1)).
LaTeX
$$$$\\displaystyle \\int_{a}^{b} x\\left(1+x^{2}\\right)^{t}\\,dx = \\frac{(1+b^{2})^{t+1}}{2(t+1)} - \\frac{(1+a^{2})^{t+1}}{2(t+1)}.$$$$
Lean4
theorem integral_mul_cpow_one_add_sq {t : ℂ} (ht : 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)) :=
by
have : t + 1 ≠ 0 := by contrapose! ht; rwa [add_eq_zero_iff_eq_neg] at ht
apply integral_eq_sub_of_hasDerivAt
· intro x _
have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x :=
by
convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1
simp
have g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z :=
by
intro z hz
convert (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const (2 * (t + 1)) using 1
simp [field]
convert (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1
· field_simp
· exact mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)
· apply Continuous.intervalIntegrable
refine continuous_ofReal.mul ?_
apply Continuous.cpow
· exact continuous_const.add (continuous_ofReal.pow 2)
· exact continuous_const
· intro a
norm_cast
exact ofReal_mem_slitPlane.2 <| add_pos_of_pos_of_nonneg one_pos <| sq_nonneg a
