English
If a function f: ℝ → E has derivative f' and both f and f' are integrable on ℝ, then the improper integral of the derivative is zero, provided f(x) → 0 as x → ±∞ (the function tends to 0 at both ends): ∫_{−∞}^{∞} f'(x) dx = 0.
Русский
Пусть f: ℝ → E имеет производную f' и обе функции интегрируемы на ℝ; если f(x) стремится к 0 на −∞ и на +∞, то ∫_{−∞}^{∞} f'(x) dx = 0.
LaTeX
$$$$ \int_{-\infty}^{\infty} f'(x) \, dx = 0, $$$$
Lean4
/-- If a function and its derivative are integrable on the real line, then the integral of the
derivative is zero. -/
theorem integral_eq_zero_of_hasDerivAt_of_integrable (hderiv : ∀ x, HasDerivAt f (f' x) x) (hf' : Integrable f')
(hf : Integrable f) : ∫ x, f' x = 0 := by
by_cases hE : CompleteSpace E; swap
· simp [integral, hE]
have A : Tendsto f atBot (𝓝 0) :=
tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0) (fun x _hx ↦ hderiv x) hf'.integrableOn hf.integrableOn
have B : Tendsto f atTop (𝓝 0) :=
tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0) (fun x _hx ↦ hderiv x) hf'.integrableOn hf.integrableOn
simpa using integral_of_hasDerivAt_of_tendsto hderiv hf' A B
