English
For natural n and real a, b, the integral over the interval from a to b of |x − a|^n equals |b − a|^(n+1) / (n+1).
Русский
Для натурального n и вещественных a, b интеграл по интервалу [a, b] от |x − a|^n равен |b − a|^(n+1) / (n+1).
LaTeX
$$$\forall a,b \in \mathbb{R},\ (n \in \mathbb{N}) \Rightarrow \displaystyle \int_{\mathrm{I}a b} |x - a|^n \, d\mu = \frac{|b - a|^{n+1}}{n+1}$$$
Lean4
/-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the
Picard-Lindelöf/Cauchy-Lipschitz theorem. -/
theorem integral_pow_abs_sub_uIoc : ∫ x in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (n + 1) :=
by
rcases le_or_gt a b with hab | hab
·
calc
∫ x in Ι a b, |x - a| ^ n = ∫ x in a..b, |x - a| ^ n := by rw [uIoc_of_le hab, ← integral_of_le hab]
_ = ∫ x in 0..(b - a), x ^ n :=
by
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl
rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
exact hx.1
_ = |b - a| ^ (n + 1) / (n + 1) := by simp [abs_of_nonneg (sub_nonneg.2 hab)]
·
calc
∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n := by rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]
_ = ∫ x in b - a..0, (-x) ^ n :=
by
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl
rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
exact hx.2
_ = |b - a| ^ (n + 1) / (n + 1) := by simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]
