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 HasStrictDerivAt.of_notMem_tsupport {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : x ∉ tsupport f) : HasStrictDerivAt f 0 x

theorem HasDerivAt.of_notMem_tsupport {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : x ∉ tsupport f) : HasDerivAt f 0 x

theorem HasDerivWithinAt.of_notMem_tsupport {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {s : Set 𝕜} (h : x ∉ tsupport f) : HasDerivWithinAt f 0 s x

theorem deriv_of_notMem_tsupport {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : x ∉ tsupport f) : deriv f x = 0

theorem support_deriv_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : Function.support (deriv f) ⊆ tsupport f

theorem tsupport_deriv_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : tsupport (deriv f) ⊆ tsupport f

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