feat(analysis/schwartz_space): 1-dimensional derivative (#18745)

src/analysis/schwartz_space.lean

@@ -5,6 +5,7 @@ Authors: Moritz Doll
 -/
 
 import analysis.calculus.cont_diff
+import analysis.calculus.iterated_deriv
 import analysis.locally_convex.with_seminorms
 import topology.algebra.uniform_filter_basis
 import topology.continuous_function.bounded
@@ -33,6 +34,8 @@ decay faster than any power of `‖x‖`.
 * `schwartz_map.seminorm`: The family of seminorms as described above
 * `schwartz_map.fderiv_clm`: The differential as a continuous linear map
 `𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F)`
+* `schwartz_map.deriv_clm`: The one-dimensional derivative as a continuous linear map
+`𝓢(ℝ, F) →L[𝕜] 𝓢(ℝ, F)`
 
 ## Main statements
 
@@ -101,6 +104,10 @@ lemma smooth (f : 𝓢(E, F)) (n : ℕ∞) : cont_diff ℝ n f := f.smooth'.of_l
 @[protected] lemma differentiable (f : 𝓢(E, F)) : differentiable ℝ f :=
 (f.smooth 1).differentiable rfl.le
 
+/-- Every Schwartz function is differentiable at any point. -/
+@[protected] lemma differentiable_at (f : 𝓢(E, F)) {x : E} : differentiable_at ℝ f x :=
+f.differentiable.differentiable_at
+
 @[ext] lemma ext {f g : 𝓢(E, F)} (h : ∀ x, (f : E → F) x = g x) : f = g := fun_like.ext f g h
 
 section is_O
@@ -377,11 +384,31 @@ lemma seminorm_le_bound (k n : ℕ) (f : 𝓢(E, F)) {M : ℝ} (hMp: 0 ≤ M)
   (hM : ∀ x, ‖x‖^k * ‖iterated_fderiv ℝ n f x‖ ≤ M) : seminorm 𝕜 k n f ≤ M :=
 f.seminorm_aux_le_bound k n hMp hM
 
+/-- If one controls the seminorm for every `x`, then one controls the seminorm.
+
+Variant for functions `𝓢(ℝ, F)`. -/
+lemma seminorm_le_bound' (k n : ℕ) (f : 𝓢(ℝ, F)) {M : ℝ} (hMp: 0 ≤ M)
+  (hM : ∀ x, |x|^k * ‖iterated_deriv n f x‖ ≤ M) : seminorm 𝕜 k n f ≤ M :=
+begin
+  refine seminorm_le_bound 𝕜 k n f hMp _,
+  simpa only [real.norm_eq_abs, norm_iterated_fderiv_eq_norm_iterated_deriv],
+end
+
 /-- The seminorm controls the Schwartz estimate for any fixed `x`. -/
 lemma le_seminorm (k n : ℕ) (f : 𝓢(E, F)) (x : E) :
   ‖x‖ ^ k * ‖iterated_fderiv ℝ n f x‖ ≤ seminorm 𝕜 k n f :=
 f.le_seminorm_aux k n x
 
+/-- The seminorm controls the Schwartz estimate for any fixed `x`.
+
+Variant for functions `𝓢(ℝ, F)`. -/
+lemma le_seminorm' (k n : ℕ) (f : 𝓢(ℝ, F)) (x : ℝ) :
+  |x| ^ k * ‖iterated_deriv n f x‖ ≤ seminorm 𝕜 k n f :=
+begin
+  have := le_seminorm 𝕜 k n f x,
+  rwa [← real.norm_eq_abs, ← norm_iterated_fderiv_eq_norm_iterated_deriv],
+end
+
 lemma norm_iterated_fderiv_le_seminorm (f : 𝓢(E, F)) (n : ℕ) (x₀ : E) :
   ‖iterated_fderiv ℝ n f x₀‖ ≤ (schwartz_map.seminorm 𝕜 0 n) f :=
 begin
@@ -515,18 +542,18 @@ def mk_clm [ring_hom_isometric σ] (A : (D → E) → (F → G))
 
 end clm
 
-section fderiv
+section derivatives
 
 /-! ### Derivatives of Schwartz functions -/
 
 variables (𝕜)
 variables [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class ℝ 𝕜 F]
 
-/-- The real derivative on Schwartz space as a continuous `𝕜`-linear map. -/
+/-- The Fréchet derivative on Schwartz space as a continuous `𝕜`-linear map. -/
 def fderiv_clm : 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F) :=
 mk_clm (fderiv ℝ)
-  (λ f g _, fderiv_add f.differentiable.differentiable_at g.differentiable.differentiable_at)
-  (λ a f _, fderiv_const_smul f.differentiable.differentiable_at a)
+  (λ f g _, fderiv_add f.differentiable_at g.differentiable_at)
+  (λ a f _, fderiv_const_smul f.differentiable_at a)
   (λ f, (cont_diff_top_iff_fderiv.mp f.smooth').2)
   (λ ⟨k, n⟩, ⟨{⟨k, n+1⟩}, 1, zero_le_one, λ f x, by simpa only [schwartz_seminorm_family_apply,
     seminorm.comp_apply, finset.sup_singleton, one_smul, norm_iterated_fderiv_fderiv, one_mul]
@@ -535,7 +562,20 @@ mk_clm (fderiv ℝ)
 @[simp] lemma fderiv_clm_apply (f : 𝓢(E, F)) (x : E) : fderiv_clm 𝕜 f x = fderiv ℝ f x :=
 rfl
 
-end fderiv
+/-- The 1-dimensional derivative on Schwartz space as a continuous `𝕜`-linear map. -/
+def deriv_clm : 𝓢(ℝ, F) →L[𝕜] 𝓢(ℝ, F) :=
+mk_clm (λ f, deriv f)
+  (λ f g _, deriv_add f.differentiable_at g.differentiable_at)
+  (λ a f _, deriv_const_smul a f.differentiable_at)
+  (λ f, (cont_diff_top_iff_deriv.mp f.smooth').2)
+  (λ ⟨k, n⟩, ⟨{⟨k, n+1⟩}, 1, zero_le_one, λ f x, by simpa only [real.norm_eq_abs,
+    finset.sup_singleton, schwartz_seminorm_family_apply, one_mul,
+    norm_iterated_fderiv_eq_norm_iterated_deriv, ← iterated_deriv_succ']
+    using f.le_seminorm' 𝕜 k (n + 1) x⟩)
+
+@[simp] lemma deriv_clm_apply (f : 𝓢(ℝ, F)) (x : ℝ) : deriv_clm 𝕜 f x = deriv f x := rfl
+
+end derivatives
 
 section bounded_continuous_function