English
Deriv on Schwartz(E, F) is a continuous linear map; applying it to f yields the usual directional derivative f′.
Русский
Производная на Schwartz(Е, F) является непрерывно линейным отображением; применение к f даёт обычную направленную производную f′.
LaTeX
$$$derivCLM 𝕜\, f = \text{the map } x \mapsto \frac{d}{dx}f(x)$$$
Lean4
/-- The 1-dimensional derivative on Schwartz space as a continuous `𝕜`-linear map. -/
def derivCLM : 𝓢(ℝ, F) →L[𝕜] 𝓢(ℝ, F) :=
mkCLM (deriv ·) (fun f g _ => deriv_add f.differentiableAt g.differentiableAt)
(fun a f _ => deriv_const_smul a f.differentiableAt) (fun f => (contDiff_succ_iff_deriv.mp (f.smooth ⊤)).2.2)
fun ⟨k, n⟩ =>
⟨{⟨k, n + 1⟩}, 1, zero_le_one, fun f x => by
simpa only [Real.norm_eq_abs, Finset.sup_singleton, schwartzSeminormFamily_apply, one_mul,
norm_iteratedFDeriv_eq_norm_iteratedDeriv, ← iteratedDeriv_succ'] using f.le_seminorm' 𝕜 k (n + 1) x⟩
