English
Let f: R → E be continuously differentiable with compact support (i.e., C^1 with compact support). Then for every b ∈ R, the improper integral of the derivative up to b equals the value of f at b:
Русский
Пусть f: ℝ → E является непрерывно дифференцируемой с компактной опорой (C^1 с компактной опорой). Тогда для каждого b ∈ ℝ верно: ∫_{-∞}^{b} f'(x) dx = f(b).
LaTeX
$$$$ \int_{x \in Iic b} \ deriv f x\; dx = f(b) \quad\text{for all } b \in \mathbb{R}, \; f \in C^1_c(\mathbb{R},E). $$$$
Lean4
/-- A special case of `integral_Iic_of_hasDerivAt_of_tendsto` where we assume that `f` is C^1 with
compact support. -/
theorem _root_.HasCompactSupport.integral_Iic_deriv_eq (hf : ContDiff ℝ 1 f) (h2f : HasCompactSupport f) (b : ℝ) :
∫ x in Iic b, deriv f x = f b :=
by
have := fun x (_ : x ∈ Iio b) ↦ hf.differentiable le_rfl x |>.hasDerivAt
rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero]
· refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn
rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f
exact h2f.filter_mono _root_.atBot_le_cocompact |>.tendsto
