Directional derivatives of test functions

Mathlib equips the test functions 𝓓(Ω, F) with the directional derivative ∂_{v}. This file evaluates it pointwise as the classical directional derivative, and shows that two directional derivatives of a test function commute, ∂_{v} (∂_{w} φ) = ∂_{w} (∂_{v} φ), because the second derivative of a smooth function is symmetric. Moving derivatives between the two sides of an integration-by-parts identity uses exactly this, for instance to show that weak derivatives commute. Summing over an orthonormal basis, the Laplacian of a test function commutes with every directional derivative. Finally, a test function on Ω times a function smooth on Ω is again a test function, with the classical product rule for its directional derivatives; this is what lets a weak derivative be tested against g φ when g is only smooth inside Ω.

Main declarations

• TestFunction.lineDerivOp_apply: ∂_{v} φ is the classical directional derivative of φ.
• TestFunction.lineDerivOp_apply_eq_fderiv: ∂_{v} φ x = Dφ(x) v.
• TestFunction.tsupport_lineDerivOp_subset: ∂_{v} φ is supported in the support of φ.
• TestFunction.lineDerivOp_one_apply_eq_deriv: on the real line, ∂_{1} φ is the derivative of φ.
• TestFunction.coe_iterate_lineDerivOp_one: repeated derivatives on the real line agree with the iterates of the ordinary derivative.
• TestFunction.lineDerivCLM_postcompCLM: directional derivatives commute with postcomposition by a continuous linear map.
• TestFunction.lineDerivOp_comm and TestFunction.lineDeriv_lineDerivOp_comm: directional derivatives of test functions commute.
• TestFunction.lineDerivOp_laplacianCLM: the Laplacian of test functions commutes with directional derivatives.
• TestFunction.exists_coe_eq_smul_of_contDiffOn: the product of a test function on Ω with a function smooth on Ω is a test function on Ω.
• TestFunction.lineDeriv_fun_smul_of_differentiableOn: its directional derivatives obey the product rule.
• TestFunction.laplacianCLM_apply: the test-function Laplacian agrees pointwise with the classical Laplacian.

@[simp]

theorem TestFunction.lineDerivOp_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v x : E) : (LineDeriv.lineDerivOp v φ) x = lineDeriv ℝ (⇑φ) x v

The directional derivative of a test function is its classical directional derivative.

theorem TestFunction.lineDerivOp_apply_eq_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v x : E) : (LineDeriv.lineDerivOp v φ) x = (fderiv ℝ (⇑φ) x) v

The directional derivative of a test function is its Fréchet derivative applied to the direction.

theorem TestFunction.tsupport_lineDerivOp_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v : E) : tsupport ⇑(LineDeriv.lineDerivOp v φ) ⊆ tsupport ⇑φ

A directional derivative of a test function is supported in the support of the function.

theorem TestFunction.lineDerivOp_one_apply_eq_deriv {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens ℝ} (φ : TestFunction Ω F ⊤) (x : ℝ) : (LineDeriv.lineDerivOp 1 φ) x = deriv (⇑φ) x

On the real line, the directional derivative of a test function in the direction 1 is its derivative.

@[simp]

theorem TestFunction.coe_iterate_lineDerivOp_one {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens ℝ} (φ : TestFunction Ω F ⊤) (n : ℕ) : ⇑((LineDeriv.lineDerivOp 1)^[n] φ) = deriv^[n] ⇑φ

Iterating the directional derivative in direction 1 on a real-line test function agrees with iterating its ordinary derivative.

@[simp]

theorem TestFunction.coe_lineDerivCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v : E) : ⇑((lineDerivCLM ℝ v) φ) = fun (x : E) => lineDeriv ℝ (⇑φ) x v

The underlying function of a directional derivative of a test function is its classical directional derivative.

theorem TestFunction.lineDerivCLM_postcompCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [Algebra ℝ 𝕜] [NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F] {n k : ℕ∞} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] [IsScalarTower ℝ 𝕜 F'] (L : F →L[𝕜] F') (v : E) (φ : TestFunction Ω F n) : (lineDerivCLM 𝕜 v) ((postcompCLM L) φ) = (postcompCLM L) ((lineDerivCLM 𝕜 v) φ)

Directional derivatives of test functions commute with postcomposition by a continuous linear map, at every pair of orders.

theorem TestFunction.lineDeriv_lineDeriv_eq_fderiv_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v w x : E) : lineDeriv ℝ (fun (y : E) => lineDeriv ℝ (⇑φ) y v) x w = (fderiv ℝ (fun (y : E) => (fderiv ℝ (⇑φ) y) v) x) w

Iterated directional derivatives of a test function agree with its iterated Fréchet derivatives evaluated in those directions.

theorem TestFunction.lineDerivOp_comm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v w : E) : LineDeriv.lineDerivOp v (LineDeriv.lineDerivOp w φ) = LineDeriv.lineDerivOp w (LineDeriv.lineDerivOp v φ)

Directional derivatives of test functions commute.

theorem TestFunction.lineDeriv_lineDerivOp_comm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v w x : E) : lineDeriv ℝ (⇑(LineDeriv.lineDerivOp v φ)) x w = lineDeriv ℝ (⇑(LineDeriv.lineDerivOp w φ)) x v

The classical directional derivative of ∂_{v} φ in the direction w is that of ∂_{w} φ in the direction v.

Multiplication by a function smooth on Ω

theorem TestFunction.exists_coe_eq_smul_of_contDiffOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {g : E → ℝ} (hg : ContDiffOn ℝ (↑⊤) g ↑Ω) (φ : TestFunction Ω F ⊤) : ∃ (ψ : TestFunction Ω F ⊤), ⇑ψ = fun (x : E) => g x • φ x

A test function times a function smooth on Ω is a test function. If g is smooth on Ω, with no condition off Ω, and φ ∈ 𝓓(Ω, F), then x ↦ g x • φ x is again a test function on Ω: it is smooth on Ω and vanishes on the open complement of tsupport φ, and these two open sets cover E.

theorem TestFunction.lineDeriv_fun_smul_of_differentiableOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {g : E → ℝ} (hg : DifferentiableOn ℝ g ↑Ω) (φ : TestFunction Ω F ⊤) (x v : E) : lineDeriv ℝ (fun (y : E) => g y • φ y) x v = g x • lineDeriv ℝ (⇑φ) x v + (fderiv ℝ g x) v • φ x

The product rule for a test function times a function differentiable on Ω: ∂_v (g φ) = g ∂_v φ + (∂_v g) φ at every point of E. Off tsupport φ both sides vanish, so nothing is needed of g outside Ω.

theorem TestFunction.lineDerivOp_laplacianCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (v : E) : LineDeriv.lineDerivOp v ((LineDeriv.laplacianCLM ℝ E (TestFunction Ω F ⊤)) φ) = (LineDeriv.laplacianCLM ℝ E (TestFunction Ω F ⊤)) (LineDeriv.lineDerivOp v φ)

The Laplacian of test functions commutes with directional derivatives: ∂_{v} (Δφ) = Δ (∂_{v} φ).

@[simp]

theorem TestFunction.laplacianCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (x : E) : ((LineDeriv.laplacianCLM ℝ E (TestFunction Ω F ⊤)) φ) x = Laplacian.laplacian (⇑φ) x

The test-function Laplacian agrees pointwise with the classical Laplacian.