Directional differentiation bundled with Schwartz regularity. The underlying functions are explicit Fréchet derivatives, so their public formulas do not depend on integration by parts or the analytic estimates used to prove rapid decay.

noncomputable def EulerSobolev.schwartzDerivative {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (m : E) (f : SchwartzMap E F) : SchwartzMap E F

The directional Fréchet derivative with its Schwartz smoothness and decay proofs.

Equations

• EulerSobolev.schwartzDerivative m f = { toFun := fun (x : E) => (fderiv ℝ (⇑f) x) m, smooth' := ⋯, decay' := ⋯ }

@[reducible, inline]

noncomputable abbrev EulerSobolev.schwartzIteratedDerivative {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} : (Fin n → E) → SchwartzMap E F → SchwartzMap E F

Iterated Schwartz differentiation in a finite ordered family of directions.

Equations

• EulerSobolev.schwartzIteratedDerivative = LineDeriv.iteratedLineDerivOp

theorem EulerSobolev.schwartzIteratedDerivative_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (m : Fin n → E) (f : SchwartzMap E F) (x : E) : (schwartzIteratedDerivative m f) x = (iteratedFDeriv ℝ n (⇑f) x) m

Iterated directional differentiation evaluates the actual Fréchet derivative tensor.