feat(analysis/calculus): support and cont_diff (#11976)

* Add some lemmas about the support of the (f)derivative of a function
* Add some equivalences for `cont_diff`

src/analysis/calculus/cont_diff.lean

@@ -1244,8 +1244,8 @@ by simpa [hn, differentiable_within_at_univ] using h.differentiable_within_at
 /-- A function is `C^(n + 1)` at a point iff locally, it has a derivative which is `C^n`. -/
 theorem cont_diff_at_succ_iff_has_fderiv_at {n : ℕ} :
   cont_diff_at 𝕜 ((n + 1) : ℕ) f x
-  ↔ (∃ f' : E → (E →L[𝕜] F), (∃ u ∈ 𝓝 x, (∀ x ∈ u, has_fderiv_at f (f' x) x))
-      ∧ (cont_diff_at 𝕜 n f' x)) :=
+  ↔ (∃ f' : E → E →L[𝕜] F, (∃ u ∈ 𝓝 x, ∀ x ∈ u, has_fderiv_at f (f' x) x)
+      ∧ cont_diff_at 𝕜 n f' x) :=
 begin
   rw [← cont_diff_within_at_univ, cont_diff_within_at_succ_iff_has_fderiv_within_at],
   simp only [nhds_within_univ, exists_prop, mem_univ, insert_eq_of_mem],
@@ -1327,6 +1327,12 @@ lemma cont_diff_at_zero :
   cont_diff_at 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, continuous_on f u :=
 by { rw ← cont_diff_within_at_univ, simp [cont_diff_within_at_zero, nhds_within_univ] }
 
+theorem cont_diff_at_one_iff : cont_diff_at 𝕜 1 f x ↔
+  ∃ f' : E → (E →L[𝕜] F), ∃ u ∈ 𝓝 x, continuous_on f' u ∧ ∀ x ∈ u, has_fderiv_at f (f' x) x :=
+by simp_rw [show (1 : with_top ℕ) = (0 + 1 : ℕ), from (zero_add 1).symm,
+  cont_diff_at_succ_iff_has_fderiv_at, show ((0 : ℕ) : with_top ℕ) = 0, from rfl,
+  cont_diff_at_zero, exists_mem_and_iff antitone_bforall antitone_continuous_on, and_comm]
+
 lemma cont_diff.of_le {m n : with_top ℕ}
   (h : cont_diff 𝕜 n f) (hmn : m ≤ n) :
   cont_diff 𝕜 m f :=
@@ -1441,17 +1447,21 @@ lemma cont_diff_of_differentiable_iterated_fderiv {n : with_top ℕ}
 cont_diff_iff_continuous_differentiable.2
 ⟨λ m hm, (h m hm).continuous, λ m hm, (h m (le_of_lt hm))⟩
 
-/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if
-it is differentiable there, and its derivative is `C^n`. -/
+/-- A function is `C^(n + 1)` if and only if it is differentiable,
+and its derivative (formulated in terms of `fderiv`) is `C^n`. -/
 theorem cont_diff_succ_iff_fderiv {n : ℕ} :
   cont_diff 𝕜 ((n + 1) : ℕ) f ↔
   differentiable 𝕜 f ∧ cont_diff 𝕜 n (λ y, fderiv 𝕜 f y) :=
 by simp [cont_diff_on_univ.symm, differentiable_on_univ.symm, fderiv_within_univ.symm,
          - fderiv_within_univ, cont_diff_on_succ_iff_fderiv_within unique_diff_on_univ,
          -with_zero.coe_add, -add_comm]
 
-/-- A function is `C^∞` on a domain with unique derivatives if and only if it is differentiable
-there, and its derivative is `C^∞`. -/
+theorem cont_diff_one_iff_fderiv :
+  cont_diff 𝕜 1 f ↔ differentiable 𝕜 f ∧ continuous (fderiv 𝕜 f) :=
+cont_diff_succ_iff_fderiv.trans $ iff.rfl.and cont_diff_zero
+
+/-- A function is `C^∞` if and only if it is differentiable,
+and its derivative (formulated in terms of `fderiv`) is `C^∞`. -/
 theorem cont_diff_top_iff_fderiv :
   cont_diff 𝕜 ∞ f ↔
   differentiable 𝕜 f ∧ cont_diff 𝕜 ∞ (λ y, fderiv 𝕜 f y) :=
@@ -1552,7 +1562,7 @@ begin
   suffices h : cont_diff 𝕜 ∞ f, by exact h.of_le le_top,
   rw cont_diff_top_iff_fderiv,
   refine ⟨hf.differentiable, _⟩,
-  simp [hf.fderiv],
+  simp_rw [hf.fderiv],
   exact cont_diff_const
 end
 
@@ -2906,14 +2916,33 @@ lemma cont_diff_on.continuous_on_deriv_of_open {n : with_top ℕ}
   continuous_on (deriv f₂) s₂ :=
 ((cont_diff_on_succ_iff_deriv_of_open hs).1 (h.of_le hn)).2.continuous_on
 
-/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if it is
-differentiable there, and its derivative is `C^n`. -/
+/-- A function is `C^(n + 1)` if and only if it is differentiable,
+  and its derivative (formulated in terms of `deriv`) is `C^n`. -/
 theorem cont_diff_succ_iff_deriv {n : ℕ} :
   cont_diff 𝕜 ((n + 1) : ℕ) f₂ ↔
     differentiable 𝕜 f₂ ∧ cont_diff 𝕜 n (deriv f₂) :=
 by simp only [← cont_diff_on_univ, cont_diff_on_succ_iff_deriv_of_open, is_open_univ,
   differentiable_on_univ]
 
+theorem cont_diff_one_iff_deriv :
+  cont_diff 𝕜 1 f₂ ↔ differentiable 𝕜 f₂ ∧ continuous (deriv f₂) :=
+cont_diff_succ_iff_deriv.trans $ iff.rfl.and cont_diff_zero
+
+/-- A function is `C^∞` if and only if it is differentiable,
+and its derivative (formulated in terms of `deriv`) is `C^∞`. -/
+theorem cont_diff_top_iff_deriv :
+  cont_diff 𝕜 ∞ f₂ ↔
+  differentiable 𝕜 f₂ ∧ cont_diff 𝕜 ∞ (deriv f₂) :=
+begin
+  simp [cont_diff_on_univ.symm, differentiable_on_univ.symm, deriv_within_univ.symm,
+        - deriv_within_univ],
+  rw cont_diff_on_top_iff_deriv_within unique_diff_on_univ,
+end
+
+lemma cont_diff.continuous_deriv {n : with_top ℕ} (h : cont_diff 𝕜 n f₂) (hn : 1 ≤ n) :
+  continuous (deriv f₂) :=
+(cont_diff_succ_iff_deriv.mp (h.of_le hn)).2.continuous
+
 end deriv
 
 section restrict_scalars

src/analysis/calculus/deriv.lean

@@ -388,6 +388,9 @@ lemma differentiable_on.has_deriv_at (h : differentiable_on 𝕜 f s) (hs : s 
 lemma has_deriv_at.deriv (h : has_deriv_at f f' x) : deriv f x = f' :=
 h.differentiable_at.has_deriv_at.unique h
 
+lemma deriv_eq {f' : 𝕜 → F} (h : ∀ x, has_deriv_at f (f' x) x) : deriv f = f' :=
+funext $ λ x, (h x).deriv
+
 lemma has_deriv_within_at.deriv_within
   (h : has_deriv_within_at f f' s x) (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within f s x = f' :=
@@ -2019,6 +2022,27 @@ funext (iter_deriv_inv k)
 
 end zpow
 
+/-! ### Support of derivatives -/
+
+section support
+
+open function
+variables {F : Type*} [normed_group F] [normed_space 𝕜 F] {f : 𝕜 → F}
+
+lemma support_deriv_subset : support (deriv f) ⊆ tsupport f :=
+begin
+  intros x,
+  rw [← not_imp_not],
+  intro h2x,
+  rw [not_mem_closure_support_iff_eventually_eq] at h2x,
+  exact nmem_support.mpr (h2x.deriv_eq.trans (deriv_const x 0))
+end
+
+lemma has_compact_support.deriv (hf : has_compact_support f) : has_compact_support (deriv f) :=
+hf.mono' support_deriv_subset
+
+end support
+
 /-! ### Upper estimates on liminf and limsup -/
 
 section real

src/analysis/calculus/fderiv.lean

@@ -461,6 +461,9 @@ lemma differentiable_on.eventually_differentiable_at (h : differentiable_on 𝕜
 lemma has_fderiv_at.fderiv (h : has_fderiv_at f f' x) : fderiv 𝕜 f x = f' :=
 by { ext, rw h.unique h.differentiable_at.has_fderiv_at }
 
+lemma fderiv_eq {f' : E → E →L[𝕜] F} (h : ∀ x, has_fderiv_at f (f' x) x) : fderiv 𝕜 f = f' :=
+funext $ λ x, (h x).fderiv
+
 /-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
 on a neighborhood of `x₀` then it its derivative at `x₀` has norm bounded by `C`.
 Version using `fderiv`. -/
@@ -2997,3 +3000,25 @@ begin
 end
 
 end restrict_scalars
+
+/-! ### Support of derivatives -/
+
+section support
+
+open function
+variables (𝕜 : Type*) {E F : Type*} [nondiscrete_normed_field 𝕜]
+variables [normed_group E] [normed_space 𝕜 E] [normed_group F] [normed_space 𝕜 F] {f : E → F}
+
+lemma support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f :=
+begin
+  intros x,
+  rw [← not_imp_not],
+  intro h2x,
+  rw [not_mem_closure_support_iff_eventually_eq] at h2x,
+  exact nmem_support.mpr (h2x.fderiv_eq.trans $ fderiv_const_apply 0),
+end
+
+lemma has_compact_support.fderiv (hf : has_compact_support f) : has_compact_support (fderiv 𝕜 f) :=
+hf.mono' $ support_fderiv_subset 𝕜
+
+end support

src/data/set/lattice.lean

@@ -153,6 +153,10 @@ theorem antitone_set_of [preorder α] {p : α → β → Prop}
   (hp : ∀ b, antitone (λ a, p a b)) : antitone (λ a, {b | p a b}) :=
 λ a a' h b, hp b h
 
+/-- Quantifying over a set is antitone in the set -/
+lemma antitone_bforall {P : α → Prop} : antitone (λ s : set α, ∀ x ∈ s, P x) :=
+λ s t hst h x hx, h x $ hst hx
+
 section galois_connection
 variables {f : α → β}