English
For complex exponent r and appropriate conditions, the integral of z^r over [a,b] equals ((b)^(r+1) - (a)^(r+1)) / (r+1).
Русский
Для комплексного показателя r и соответствующих условий интеграл z^r по отрезку [a,b] равен ((b)^(r+1) - (a)^(r+1))/(r+1).
LaTeX
$$$\int_{a}^{b} z^{r} \, dz = \dfrac{b^{r+1} - a^{r+1}}{r+1}$$$
Lean4
theorem integral_cpow {r : ℂ} (h : -1 < r.re ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
(∫ x : ℝ in a..b, (x : ℂ) ^ r) = ((b : ℂ) ^ (r + 1) - (a : ℂ) ^ (r + 1)) / (r + 1) :=
by
rw [sub_div]
have hr : r + 1 ≠ 0 := by
rcases h with h | h
· apply_fun Complex.re
rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne, add_eq_zero_iff_eq_neg]
exact h.ne'
· rw [Ne, ← add_eq_zero_iff_eq_neg] at h; exact h.1
by_cases hab : (0 : ℝ) ∉ [[a, b]]
· apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_) (intervalIntegrable_cpow (r := r) <| Or.inr hab)
refine hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_
contrapose! hr; rwa [add_eq_zero_iff_eq_neg]
replace h : -1 < r.re := by tauto
suffices ∀ c : ℝ, (∫ x : ℝ in 0..c, (x : ℂ) ^ r) = (c : ℂ) ^ (r + 1) / (r + 1) - (0 : ℂ) ^ (r + 1) / (r + 1)
by
rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h) (@intervalIntegrable_cpow' 0 b r h),
integral_symm, this a, this b, Complex.zero_cpow hr]
ring
intro c
apply integral_eq_sub_of_hasDeriv_right
· refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn
rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]
· refine fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt
· rcases le_total c 0 with (hc | hc)
· rw [max_eq_left hc] at hx; exact hx.2.ne
· rw [min_eq_left hc] at hx; exact hx.1.ne'
· contrapose! hr; rw [hr]; ring
· exact intervalIntegrable_cpow' h
