English
For a real p ≠ 0 and a function g: ℝ → F, the substitution y = x^p on the half-line Ioi 0 preserves the integral up to the Jacobian factor, yielding an equality between the two integrals with a factor depending on p.
Русский
При p ≠ 0 подстановка y = x^p на половой луч Ioi 0 сохраняет интеграл до множителя Якоби, зависящего от p.
LaTeX
$$$$ \int_{x in Ioi 0} (|p| \; x^{p-1}) \; g(x^p) \, dx = \int_{y in Ioi 0} g(y) \, dy, \quad p \neq 0. $$$$
Lean4
/-- **Integration by parts on (-∞, ∞).**
With respect to a general bilinear form, assuming moreover that the total function is integrable.
-/
theorem integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable (hu : ∀ x, HasDerivAt u (u' x) x)
(hv : ∀ x, HasDerivAt v (v' x) x) (huv' : Integrable (fun x ↦ L (u x) (v' x)))
(hu'v : Integrable (fun x ↦ L (u' x) (v x))) (huv : Integrable (fun x ↦ L (u x) (v x))) :
∫ (x : ℝ), L (u x) (v' x) = -∫ (x : ℝ), L (u' x) (v x) :=
by
by_cases hG : CompleteSpace G; swap
· simp [integral, hG]
have I : Tendsto (fun x ↦ L (u x) (v x)) atBot (𝓝 0) :=
tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0) (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
(huv'.add hu'v).integrableOn huv.integrableOn
have J : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 0) :=
tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0) (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
(huv'.add hu'v).integrableOn huv.integrableOn
simp [integral_bilinear_hasDerivAt_right_eq_sub hu hv huv' hu'v I J]
