Directional derivatives of tempered distributions

Mathlib defines the directional derivative of a tempered distribution by duality, (∂_m f) u = f (-∂_m u). Since directional derivatives of Schwartz functions commute (SchwartzMap.lineDerivOp_comm), so do those of tempered distributions. On the plane ℂ the Laplacian of a tempered distribution is then ∂₁² f + ∂₂² f, with ∂₁ and ∂₂ the derivatives along 1 and I, as for Schwartz functions (SchwartzMap.laplacian_eq_lineDerivOp_one_I). These are the identities needed to compute compositions of constant-coefficient first-order operators on tempered distributions. Directional differentiation of the tempered distribution given by a Schwartz function also commutes with a continuous real-linear map applied to its values.

Main results

• TemperedDistribution.lineDerivOp_comm: ∂_v ∂_w f = ∂_w ∂_v f.
• TemperedDistribution.laplacian_eq_lineDerivOp_one_I: Δ f = ∂₁² f + ∂₂² f on ℂ.
• TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_postcompCLM: ∂_v (L ∘ f) = L ∘ ∂_v f for a Schwartz function f viewed as a tempered distribution.

theorem TemperedDistribution.lineDerivOp_comm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : TemperedDistribution E F) (v w : E) : LineDeriv.lineDerivOp v (LineDeriv.lineDerivOp w f) = LineDeriv.lineDerivOp w (LineDeriv.lineDerivOp v f)

Directional derivatives of tempered distributions commute.

theorem TemperedDistribution.laplacian_eq_lineDerivOp_one_I {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : TemperedDistribution ℂ F) : Laplacian.laplacian f = LineDeriv.lineDerivOp 1 (LineDeriv.lineDerivOp 1 f) + LineDeriv.lineDerivOp Complex.I (LineDeriv.lineDerivOp Complex.I f)

The Laplacian on the plane in coordinates: Δ f = ∂₁² f + ∂₂² f for a tempered distribution f on ℂ, where ∂₁ and ∂₂ differentiate along 1 and I.

theorem TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_postcompCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (L : G →L[ℝ] F) (f : SchwartzMap E G) (m : E) : LineDeriv.lineDerivOp m ((SchwartzMap.toTemperedDistributionCLM E F μ) ((SchwartzMap.postcompCLM L) f)) = (SchwartzMap.toTemperedDistributionCLM E F μ) ((SchwartzMap.postcompCLM L) (LineDeriv.lineDerivOp m f))

Directional differentiation of the tempered distribution given by a Schwartz function commutes with a continuous real-linear map applied to the values of the function.