-
Notifications
You must be signed in to change notification settings - Fork 273
/
Support.lean
49 lines (34 loc) · 1.31 KB
/
Support.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
/-
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
-/
import Mathlib.Analysis.Calculus.Deriv.Basic
#align_import analysis.calculus.deriv.support from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
/-!
# 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
protected theorem HasCompactSupport.deriv (hf : HasCompactSupport f) :
HasCompactSupport (deriv f) :=
hf.mono' support_deriv_subset
#align has_compact_support.deriv HasCompactSupport.deriv
end Support