[Merged by Bors] - feat: port Analysis.Calculus.Deriv.Support

Mathlib.lean

@@ -423,6 +423,7 @@ import Mathlib.Analysis.Calculus.Deriv.Linear
 import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Prod
 import Mathlib.Analysis.Calculus.Deriv.Slope
+import Mathlib.Analysis.Calculus.Deriv.Support
 import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Bilinear

Mathlib/Analysis/Calculus/Deriv/Support.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2022 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+! This file was ported from Lean 3 source module analysis.calculus.deriv.support
+! leanprover-community/mathlib commit 3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Calculus.Deriv.Basic
+
+/-!
+# 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
+-/
+
+
+universe u v
+
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
+
+variable {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+variable {f : 𝕜 → E}
+
+/-! ### Support of derivatives -/
+
+
+section Support
+
+open Function
+
+theorem support_deriv_subset : support (deriv f) ⊆ tsupport f := by
+  intro x
+  rw [← not_imp_not]
+  intro h2x
+  rw [not_mem_tsupport_iff_eventuallyEq] at h2x
+  exact nmem_support.mpr (h2x.deriv_eq.trans (deriv_const x 0))
+#align support_deriv_subset support_deriv_subset
+
+theorem HasCompactSupport.deriv (hf : HasCompactSupport f) : HasCompactSupport (deriv f) :=
+  hf.mono' support_deriv_subset
+#align has_compact_support.deriv HasCompactSupport.deriv
+
+end Support
+