English
Let f: ℝ → E with derivative f'(x) existing for all x, and assume f' is integrable on ℝ. If f tends to m as x → -∞ and to n as x → +∞, then the integral of f' over the whole real line equals n − m:
Русский
Пусть f: ℝ → E имеет производную f'(x) во всех точках и производная интегрируема на ℝ; если f(x) стремится к m при x→−∞ и к n при x→+∞, то ∫_{−∞}^{∞} f'(x) dx = n − m.
LaTeX
$$$$ \int_{-\infty}^{\infty} f'(x) \, dx = n - m, \quad \text{where } \lim_{x\to -\infty} f(x) = m, \; \lim_{x\to +\infty} f(x) = n. $$$$
Lean4
/-- **Fundamental theorem of calculus-2**, on the whole real line
When a function has a limit `m` at `-∞` and `n` at `+∞`, and its derivative is integrable, then the
integral of the derivative is `n - m`.
Note that such a function always has a limit at `-∞` and `+∞`,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic` and
`tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`. -/
theorem integral_of_hasDerivAt_of_tendsto [CompleteSpace E] (hderiv : ∀ x, HasDerivAt f (f' x) x) (hf' : Integrable f')
(hbot : Tendsto f atBot (𝓝 m)) (htop : Tendsto f atTop (𝓝 n)) : ∫ x, f' x = n - m :=
by
rw [← setIntegral_univ, ← Set.Iic_union_Ioi (a := 0),
setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi hf'.integrableOn hf'.integrableOn,
integral_Iic_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn hbot,
integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn htop]
abel
