Documentation

Mathlib.Analysis.Calculus.Deriv.Support

Support of the derivative of a function #

In this file we prove that the (topological) support of a function includes the support of its derivative. As a corollary, we show that the derivative of a function with compact support has compact support.

Keywords #

derivative, support

Support of derivatives #

theorem support_deriv_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} :
theorem HasCompactSupport.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} (hf : HasCompactSupport f) :