Physlib.SpaceAndTime.Space.Derivatives.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Joseph Tooby-Smith, Lode Vermeulen
-/
module

public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
public import Physlib.Mathematics.Distribution.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
public import Physlib.SpaceAndTime.Space.Module
public import Mathlib.Analysis.InnerProductSpace.Calculus

Derivatives on Space

i. Overview

In this module we define derivatives of functions and distributions on space Space d, in the standard directions.

ii. Key results

deriv : The derivative of a function on space in a given direction.

distDeriv : The derivative of a distribution on space in a given direction.

iii. Table of contents

A. Derivatives of functions on Space d

A.1. Basic equalities

A.2. Derivative of the constant function

A.3. Derivative distributes over addition

A.4. Derivative distributes over scalar multiplication

A.5. Two spatial derivatives commute

A.6. Derivative of a component

A.7. Derivative of a component squared

A.8. Derivivatives of components

A.9. Derivative of a norm squared

A.9.1. Differentiability of the norm squared function

A.9.2. Derivative of the norm squared function

A.10. Derivative of the inner product

A.10.1. Differentiability of the inner product function

A.10.2. Derivative of the inner product function

A.10.3. Derivative of the inner product on one side

A.11. Differentiability of derivatives

B. Derivatives of distributions on Space d

B.1. The definition

B.2. Basic equality

B.3. Commutation of derivatives

iv. References

@[expose] public section

A. Derivatives of functions on `Space d`

@[inherit_doc deriv]
macro "∂[" i:term "]" : term => `(deriv $i)

A.1. Basic equalities

              lemma deriv_eq [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (μ : Fin d) (f : Space d → M) (x : Space d) :
    deriv μ f x = fderiv ℝ f x (basis μ) := byM:Type u_1d:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mμ:Fin df:Space d → Mx:Space d⊢ deriv μ f x = (fderiv ℝ f x) (basis μ) rflAll goals completed! 🐙lemma deriv_eq_fderiv_fun [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (μ : Fin d) (f : Space d → M) :
    deriv μ f = fun x => fderiv ℝ (fun x => f x) x (basis μ) := byM:Type u_1d:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mμ:Fin df:Space d → M⊢ deriv μ f = fun x => (fderiv ℝ (fun x => f x) x) (basis μ) rflAll goals completed! 🐙lemma deriv_eq_fderiv_basis [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (μ : Fin d) (f : Space d → M) (x : Space d) :
    deriv μ f x = fderiv ℝ f x (basis μ) := byM:Type u_1d:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mμ:Fin df:Space d → Mx:Space d⊢ deriv μ f x = (fderiv ℝ f x) (basis μ) rflAll goals completed! 🐙lemma fderiv_eq_sum_deriv {M d} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (f : Space d → M) (x y : Space d) :
    fderiv ℝ f x y = ∑ i : Fin d, y i • ∂[i] f x := byM:Type u_1d:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mf:Space d → Mx:Space dy:Space d⊢ (fderiv ℝ f x) y = ∑ i, y.val i • deriv i f x
  conv_lhs => rw [← basis.sum_repr y]M:Type u_1d:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mf:Space d → Mx:Space dy:Space d| (fderiv ℝ f x) (∑ i, (basis.repr y).ofLp i • basis i)
  simp [deriv_eq_fderiv_basis]All goals completed! 🐙TODO "Make the version of the derivative described through
  `deriv_eq_mfderiv_manifoldStructure` the definition of `deriv` and prove the
  equivalence with the current definition, under suitable conditions."

A.2. Derivative of the constant function

@[simp]
lemma deriv_const [NormedAddCommGroup M] [NormedSpace ℝ M] (m : M) (μ : Fin d) :
    deriv μ (fun _ => m) t = 0 := byM:Type u_1d:ℕt:Space dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mm:Mμ:Fin d⊢ deriv μ (fun x => m) t = 0
  simp [deriv]All goals completed! 🐙

A.3. Derivative distributes over addition and subtraction

Eta-expanded form of Space.deriv_add

Derivatives on space distribute over addition.

@[to_fun]
lemma deriv_add [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f1 f2 : Space d → M) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) :
    ∂[u] (f1 + f2) = ∂[u] f1 + ∂[u] f2 := byM:Type u_1d:ℕu:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf1:Space d → Mf2:Space d → Mhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ deriv u (f1 + f2) = deriv u f1 + deriv u f2
  ext xM:Type u_1d:ℕu:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf1:Space d → Mf2:Space d → Mhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ deriv u (f1 + f2) x = (deriv u f1 + deriv u f2) x
  simp [deriv_eq, fderiv_add (hf1 x) (hf2 x)]All goals completed! 🐙

Derivatives on space distribute coordinate-wise over addition.

lemma deriv_coord_add (f1 f2 : Space d → EuclideanSpace ℝ (Fin d))
    (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) :
    (∂[u] (fun x => f1 x i + f2 x i)) =
      (∂[u] (fun x => f1 x i)) + (∂[u] (fun x => f2 x i)) :=
  deriv_add (fun x => f1 x i) (fun x => f2 x i) (byd:ℕu:Fin di:Fin df1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ Differentiable ℝ fun x => (f1 x).ofLp i fun_propAll goals completed! 🐙) (byd:ℕu:Fin di:Fin df1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ Differentiable ℝ fun x => (f2 x).ofLp i fun_propAll goals completed! 🐙)

Eta-expanded form of Space.deriv_sub

Derivatives on space distribute over subtraction.

@[to_fun]
lemma deriv_sub [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f1 f2 : Space d → M) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) :
    ∂[u] (f1 - f2) = ∂[u] f1 - ∂[u] f2 := byM:Type u_1d:ℕu:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf1:Space d → Mf2:Space d → Mhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ deriv u (f1 - f2) = deriv u f1 - deriv u f2
  ext xM:Type u_1d:ℕu:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf1:Space d → Mf2:Space d → Mhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ deriv u (f1 - f2) x = (deriv u f1 - deriv u f2) x
  simp [deriv_eq, fderiv_sub (hf1 x) (hf2 x)]All goals completed! 🐙

A.4. Derivative distributes over scalar multiplication

Space derivatives on scalar product of functions.

lemma deriv_smul [NormedAddCommGroup M] [NormedSpace ℝ M] [NontriviallyNormedField 𝕜]
    [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 M] {c : Space d → 𝕜} {f : Space d → M}
    (hc : DifferentiableAt ℝ c x) (hf : DifferentiableAt ℝ f x) :
    ∂[u] (c • f) x = c x • ∂[u] f x + ∂[u] c x • f x := byM:Type u_1𝕜:Type u_2d:ℕx:Space du:Fin dinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:NontriviallyNormedField 𝕜inst✝¹:NormedAlgebra ℝ 𝕜inst✝:NormedSpace 𝕜 Mc:Space d → 𝕜f:Space d → Mhc:DifferentiableAt ℝ c xhf:DifferentiableAt ℝ f x⊢ deriv u (c • f) x = c x • deriv u f x + deriv u c x • f x
  simp [deriv_eq, fderiv_smul hc hf]All goals completed! 🐙

Space derivatives on scalar times function.

lemma deriv_const_smul [NormedAddCommGroup M] [NormedSpace ℝ M] [Semiring R]
    [Module R M] [SMulCommClass ℝ R M] [ContinuousConstSMul R M] {f : Space d → M} (c : R)
    (h : Differentiable ℝ f) : ∂[u] (c • f) = c • ∂[u] f := byM:Type u_1R:Type u_2d:ℕu:Fin dinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:Semiring Rinst✝²:Module R Minst✝¹:SMulCommClass ℝ R Minst✝:ContinuousConstSMul R Mf:Space d → Mc:Rh:Differentiable ℝ f⊢ deriv u (c • f) = c • deriv u f
  ext xM:Type u_1R:Type u_2d:ℕu:Fin dinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:Semiring Rinst✝²:Module R Minst✝¹:SMulCommClass ℝ R Minst✝:ContinuousConstSMul R Mf:Space d → Mc:Rh:Differentiable ℝ fx:Space d⊢ deriv u (c • f) x = (c • deriv u f) x
  simp [deriv_eq, fderiv_const_smul (h x) c]All goals completed! 🐙

Coordinate-wise scalar multiplication on space derivatives.

lemma deriv_coord_smul (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ)
    (hf : Differentiable ℝ f) :
    ∂[u] (fun x => k * f x i) x = k * ∂[u] (fun x => f x i) x :=
  congrFun (deriv_const_smul (f := fun x => f x i) k (byd:ℕu:Fin di:Fin dx:Space df:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ Differentiable ℝ fun x => (f x).ofLp i fun_propAll goals completed! 🐙)) x

A.5. Two spatial derivatives commute

Derivatives on space commute with one another.


lemma deriv_commute [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : Space d → M) (hf : ContDiff ℝ 2 f) : ∂[u] (∂[v] f) = ∂[v] (∂[u] f) := byM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 f⊢ deriv u (deriv v f) = deriv v (deriv u f)
  simp only [deriv_eq_fderiv_fun]M:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 f⊢ (fun x => (fderiv ℝ (fun x => (fderiv ℝ (fun x => f x) x) (basis v)) x) (basis u)) = fun x =>
  (fderiv ℝ (fun x => (fderiv ℝ (fun x => f x) x) (basis u)) x) (basis v)
  ext xM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ (fderiv ℝ (fun x => (fderiv ℝ (fun x => f x) x) (basis v)) x) (basis u) =
  (fderiv ℝ (fun x => (fderiv ℝ (fun x => f x) x) (basis u)) x) (basis v)
  rw [fderiv_clm_apply,M:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis v) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis v))
    (basis u) =
  (fderiv ℝ (fun x => (fderiv ℝ (fun x => f x) x) (basis u)) x) (basis v)hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) xM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis v) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis v))
    (basis u) =
  (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis u) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis u))
    (basis v)hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x fderiv_clm_applyM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis v) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis v))
    (basis u) =
  (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis u) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis u))
    (basis v)hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) xM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis v) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis v))
    (basis u) =
  (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis u) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis u))
    (basis v)hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x]M:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis v) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis v))
    (basis u) =
  (fderiv ℝ (fun x => f x) x ∘SL fderiv ℝ (fun x => basis u) x + (fderiv ℝ (fderiv ℝ fun x => f x) x).flip (basis u))
    (basis v)hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x
  simp only [fderiv_fun_const, Pi.ofNat_apply, ContinuousLinearMap.comp_zero, zero_add,
    ContinuousLinearMap.flip_apply]M:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ ((fderiv ℝ (fderiv ℝ fun x => f x) x) (basis u)) (basis v) = ((fderiv ℝ (fderiv ℝ fun x => f x) x) (basis v)) (basis u)hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x
  rw [(hf.contDiffAt.isSymmSndFDerivAt (byM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ minSmoothness ℝ 2 ≤ 2hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x simpAll goals completed! 🐙hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x)).eq]hcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis u) xhcM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fderiv ℝ fun x => f x) xhuM:Type u_1d:ℕu:Fin dv:Fin dinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Space d → Mhf:ContDiff ℝ 2 fx:Space d⊢ DifferentiableAt ℝ (fun x => basis v) x
  repeat fun_propAll goals completed! 🐙

A.6. Derivative of a component

              @[simp]
lemma deriv_component_same (μ : Fin d) (x : Space d) :
    ∂[μ] (fun x => x μ) x = 1 := byd:ℕμ:Fin dx:Space d⊢ deriv μ (fun x => x.val μ) x = 1
  simp only [← Space.coord_apply, ← Space.coordCLM_apply]d:ℕμ:Fin dx:Space d⊢ deriv μ (fun x => (coordCLM μ) x) x = 1
  simp only [deriv_eq, ContinuousLinearMap.fderiv]d:ℕμ:Fin dx:Space d⊢ (coordCLM μ) (basis μ) = 1
  simp [Space.coordCLM, Space.coord]All goals completed! 🐙lemma deriv_component_diff (μ ν : Fin d) (x : Space d) (h : μ ≠ ν) :
    (deriv μ (fun x => x ν) x) = 0 := byd:ℕμ:Fin dν:Fin dx:Space dh:μ ≠ ν⊢ deriv μ (fun x => x.val ν) x = 0
  simp only [← Space.coord_apply, ← Space.coordCLM_apply]d:ℕμ:Fin dν:Fin dx:Space dh:μ ≠ ν⊢ deriv μ (fun x => (coordCLM ν) x) x = 0
  simp only [deriv_eq, ContinuousLinearMap.fderiv]d:ℕμ:Fin dν:Fin dx:Space dh:μ ≠ ν⊢ (coordCLM ν) (basis μ) = 0
  simpa [Space.coordCLM, Space.coord, basis_apply] using hAll goals completed! 🐙lemma deriv_component (μ ν : Fin d) (x : Space d) :
    (deriv ν (fun x => x μ) x) = if ν = μ then 1 else 0 := byd:ℕμ:Fin dν:Fin dx:Space d⊢ deriv ν (fun x => x.val μ) x = if ν = μ then 1 else 0
  obtain rfl | h' := eq_or_ne ν μinld:ℕν:Fin dx:Space d⊢ deriv ν (fun x => x.val ν) x = if ν = ν then 1 else 0inrd:ℕμ:Fin dν:Fin dx:Space dh':ν ≠ μ⊢ deriv ν (fun x => x.val μ) x = if ν = μ then 1 else 0
  ·inld:ℕν:Fin dx:Space d⊢ deriv ν (fun x => x.val ν) x = if ν = ν then 1 else 0 simpAll goals completed! 🐙
  ·inrd:ℕμ:Fin dν:Fin dx:Space dh':ν ≠ μ⊢ deriv ν (fun x => x.val μ) x = if ν = μ then 1 else 0 simp [deriv_component_diff ν μ x h', h']All goals completed! 🐙

A.7. Derivative of a component squared



lemma deriv_component_sq {d : ℕ} {ν μ : Fin d} (x : Space d) :
    (deriv ν (fun x => (x μ) ^ 2) x) = if ν = μ then 2 * x μ else 0:= byd:ℕν:Fin dμ:Fin dx:Space d⊢ deriv ν (fun x => x.val μ ^ 2) x = if ν = μ then 2 * x.val μ else 0
  rw [deriv_eq,d:ℕν:Fin dμ:Fin dx:Space d⊢ (fderiv ℝ (fun x => x.val μ ^ 2) x) (basis ν) = if ν = μ then 2 * x.val μ else 0d:ℕν:Fin dμ:Fin dx:Space d⊢ ((2 • x.val μ ^ (2 - 1)) • fderiv ℝ (fun p => p.val μ) x) (basis ν) = if ν = μ then 2 * x.val μ else 0 fderiv_fun_pow 2 (eval_differentiable μ x)d:ℕν:Fin dμ:Fin dx:Space d⊢ ((2 • x.val μ ^ (2 - 1)) • fderiv ℝ (fun p => p.val μ) x) (basis ν) = if ν = μ then 2 * x.val μ else 0d:ℕν:Fin dμ:Fin dx:Space d⊢ ((2 • x.val μ ^ (2 - 1)) • fderiv ℝ (fun p => p.val μ) x) (basis ν) = if ν = μ then 2 * x.val μ else 0]d:ℕν:Fin dμ:Fin dx:Space d⊢ ((2 • x.val μ ^ (2 - 1)) • fderiv ℝ (fun p => p.val μ) x) (basis ν) = if ν = μ then 2 * x.val μ else 0
  simp [← deriv_eq, deriv_component, mul_ite]All goals completed! 🐙

A.8. Derivivatives of components



lemma deriv_euclid {d ν μ} {f : Space d → EuclideanSpace ℝ (Fin n)}
    (hf : Differentiable ℝ f) (x : Space d) :
    deriv ν (fun x => f x μ) x = deriv ν (fun x => f x) x μ := byn:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ deriv ν (fun x => (f x).ofLp μ) x = (deriv ν (fun x => f x) x).ofLp μ
  rw [deriv_eq_fderiv_basisn:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (fun x => (f x).ofLp μ) x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μn:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (fun x => (f x).ofLp μ) x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μ]n:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (fun x => (f x).ofLp μ) x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μ
  change fderiv ℝ (EuclideanSpace.proj μ ∘ fun x => f x) x (basis ν) = _n:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ) ∘ fun x => f x) x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μ
  rw [fderiv_comp x (EuclideanSpace.proj μ).differentiableAt (hf x)n:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f x) ∘SL fderiv ℝ f x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μn:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f x) ∘SL fderiv ℝ f x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μ]n:ℕd:ℕν:Fin dμ:Fin nf:Space d → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f x) ∘SL fderiv ℝ f x) (basis ν) = (deriv ν (fun x => f x) x).ofLp μ
  simp [-EuclideanSpace.coe_proj, ← deriv_eq_fderiv_basis]All goals completed! 🐙



lemma deriv_lorentz_vector {d ν μ} {f : Space d → Lorentz.Vector d}
    (hf : Differentiable ℝ f) (x : Space d) :
    deriv ν (fun x => f x μ) x = deriv ν (fun x => f x) x μ := byd:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ deriv ν (fun x => f x μ) x = deriv ν (fun x => f x) x μ
  rw [deriv_eq_fderiv_basisd:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (fun x => f x μ) x) (basis ν) = deriv ν (fun x => f x) x μd:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (fun x => f x μ) x) (basis ν) = deriv ν (fun x => f x) x μ]d:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (fun x => f x μ) x) (basis ν) = deriv ν (fun x => f x) x μ
  change fderiv ℝ (Lorentz.Vector.coordCLM μ ∘ fun x => f x) x (basis ν) = _d:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM μ) ∘ fun x => f x) x) (basis ν) = deriv ν (fun x => f x) x μ
  rw [fderiv_comp x (Lorentz.Vector.coordCLM μ).differentiableAt (hf x)d:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM μ)) (f x) ∘SL fderiv ℝ f x) (basis ν) = deriv ν (fun x => f x) x μd:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM μ)) (f x) ∘SL fderiv ℝ f x) (basis ν) = deriv ν (fun x => f x) x μ]d:ℕν:Fin dμ:Fin 1 ⊕ Fin df:Space d → Lorentz.Vector dhf:Differentiable ℝ fx:Space d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM μ)) (f x) ∘SL fderiv ℝ f x) (basis ν) = deriv ν (fun x => f x) x μ
  simp [← deriv_eq_fderiv_basis, Lorentz.Vector.coordCLM_apply]All goals completed! 🐙

A.9. Derivative of a norm squared

A.9.1. Differentiability of the norm squared function

@[fun_prop]
lemma norm_sq_differentiable : Differentiable ℝ (fun x : Space d => ‖x‖ ^ 2) :=
  (contDiff_norm_sq ℝ).differentiable one_ne_zero

A.9.2. Derivative of the norm squared function

lemma deriv_norm_sq (x : Space d) (i : Fin d) :
    deriv i (fun x => ‖x‖ ^ 2) x = 2 * x i := byd:ℕx:Space di:Fin d⊢ deriv i (fun x => ‖x‖ ^ 2) x = 2 * x.val i
  simp [deriv_eq, fderiv_norm_sq_apply]All goals completed! 🐙

A.10. Derivative of the inner product

A.10.1. Differentiability of the inner product function

The inner product is differentiable.

@[fun_prop]
lemma inner_differentiable {d : ℕ} :
    Differentiable ℝ (fun y : Space d => ⟪y, y⟫_ℝ) :=
  differentiable_id.inner ℝ differentiable_id

              @[fun_prop]
lemma inner_differentiableAt {d : ℕ} (x : Space d) :
    DifferentiableAt ℝ (fun y : Space d => ⟪y, y⟫_ℝ) x :=
  inner_differentiable x@[fun_prop]
lemma inner_apply_differentiableAt {d : ℕ} [NormedAddCommGroup M]
    [NormedSpace ℝ M]
    {f : M → Space d} {g : M → Space d} (x : M)
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    DifferentiableAt ℝ (fun y : M => ⟪f y, g y⟫_ℝ) x :=
  hf.inner ℝ hg@[fun_prop]
lemma inner_apply_differentiable {d : ℕ} [NormedAddCommGroup M]
    [NormedSpace ℝ M]
    {f : M → Space d} {g : M → Space d}
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
    Differentiable ℝ (fun y : M => ⟪f y, g y⟫_ℝ) :=
  hf.inner ℝ hg@[fun_prop]
lemma inner_contDiff {n : WithTop ℕ∞} {d : ℕ} :
    ContDiff ℝ n (fun y : Space d => ⟪y, y⟫_ℝ) :=
  contDiff_id.inner ℝ contDiff_id@[fun_prop]
lemma inner_apply_contDiff {n : WithTop ℕ∞} {d : ℕ} [NormedAddCommGroup M]
    [NormedSpace ℝ M]
    {f : M → Space d} {g : M → Space d}
    (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) :
    ContDiff ℝ n (fun y : M => ⟪f y, g y⟫_ℝ) :=
  hf.inner ℝ hg

A.10.2. Derivative of the inner product function

lemma deriv_eq_inner_self (x : Space d) (i : Fin d) :
    deriv i (fun x => ⟪x, x⟫_ℝ) x = 2 * x i := byd:ℕx:Space di:Fin d⊢ deriv i (fun x => ⟪x, x⟫_ℝ) x = 2 * x.val i
  simpa only [real_inner_self_eq_norm_sq] using deriv_norm_sq x iAll goals completed! 🐙

A.10.3. Derivative of the inner product on one side

@[simp]
lemma deriv_inner_left {d} (x1 x2 : Space d) (i : Fin d) :
    deriv i (fun x => ⟪x, x2⟫_ℝ) x1 = x2 i := byd:ℕx1:Space dx2:Space di:Fin d⊢ deriv i (fun x => ⟪x, x2⟫_ℝ) x1 = x2.val i
  simp [deriv_eq, fderiv_inner_apply ℝ differentiableAt_fun_id (differentiableAt_const x2)]All goals completed! 🐙

@[simp]
lemma deriv_inner_right {d} (x1 x2 : Space d) (i : Fin d) :
    deriv i (fun x => ⟪x1, x⟫_ℝ) x2 = x1 i := byd:ℕx1:Space dx2:Space di:Fin d⊢ deriv i (fun x => ⟪x1, x⟫_ℝ) x2 = x1.val i
  simp [deriv_eq, fderiv_inner_apply ℝ (differentiableAt_const x1) differentiableAt_fun_id]All goals completed! 🐙

A.11. Differentiability of derivatives

lemma deriv_differentiable {M} [NormedAddCommGroup M]
    [NormedSpace ℝ M] {d : ℕ} {f : Space d → M}
    (hf : ContDiff ℝ 2 f) (i : Fin d) :
    Differentiable ℝ (deriv i f) := byM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕf:Space d → Mhf:ContDiff ℝ 2 fi:Fin d⊢ Differentiable ℝ (deriv i f)
  unfold derivM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕf:Space d → Mhf:ContDiff ℝ 2 fi:Fin d⊢ Differentiable ℝ fun x => (fderiv ℝ f x) (basis i)
  fun_propAll goals completed! 🐙

lemma deriv_contDiff {d} {f : Space d → ℝ} (hf : ContDiff ℝ (n + 1) f) :
    ContDiff ℝ n fun x i => deriv i f x := byn:ℕ∞ωd:ℕf:Space d → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n fun x i => deriv i f x
  unfold derivn:ℕ∞ωd:ℕf:Space d → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n fun x i => (fderiv ℝ f x) (basis i)
  fun_propAll goals completed! 🐙

B. Derivatives of distributions on `Space d`

B.1. The definition

@[inherit_doc distDeriv]
macro "∂ᵈ[" i:term "]" : term => `(distDeriv $i)

B.2. Basic equality

lemma distDeriv_apply {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (μ : Fin d) (f : (Space d) →d[ℝ] M) (ε : 𝓢(Space d, ℝ)) :
    (∂ᵈ[μ] f) ε = fderivD ℝ f ε (basis μ) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin df:(Space d)→d[ℝ] Mε:𝓢(Space d, ℝ)⊢ ((distDeriv μ) f) ε = (((fderivD ℝ) f) ε) (basis μ)
  simp [distDeriv, Distribution.fderivD]All goals completed! 🐙

B.3. Commutation of derivatives

lemma schwartMap_fderiv_comm {d}
    (μ ν : Fin d) (x : Space d) (η : 𝓢(Space d, ℝ)) :
    ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ))
      ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν))
      ((fderivCLM ℝ (Space d) ℝ) η)))) x =
    ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν))
      ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ))
      ((fderivCLM ℝ (Space d) ℝ) η)))) x := byd:ℕμ:Fin dν:Fin dx:Space dη:𝓢(Space d, ℝ)⊢ ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ))
      ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν)) ((fderivCLM ℝ (Space d) ℝ) η))))
    x =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν))
      ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ)) ((fderivCLM ℝ (Space d) ℝ) η))))
    x
  change ∂[μ] (∂[ν] ⇑η) x = ∂[ν] (∂[μ] ⇑η) xd:ℕμ:Fin dν:Fin dx:Space dη:𝓢(Space d, ℝ)⊢ deriv μ (deriv ν ⇑η) x = deriv ν (deriv μ ⇑η) x
  exact congrFun (deriv_commute _ (η.smooth 2)) xAll goals completed! 🐙

lemma distDeriv_commute {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (μ ν : Fin d) (f : (Space d) →d[ℝ] M) :
    (∂ᵈ[ν] (∂ᵈ[μ] f)) = (∂ᵈ[μ] (∂ᵈ[ν] f)) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin dν:Fin df:(Space d)→d[ℝ] M⊢ (distDeriv ν) ((distDeriv μ) f) = (distDeriv μ) ((distDeriv ν) f)
  ext ηM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin dν:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space d, ℝ)⊢ ((distDeriv ν) ((distDeriv μ) f)) η = ((distDeriv μ) ((distDeriv ν) f)) η
  simp [distDeriv, Distribution.fderivD]M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin dν:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space d, ℝ)⊢ f
    ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ))
      ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν)) ((fderivCLM ℝ (Space d) ℝ) η)))) =
  f
    ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν))
      ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ)) ((fderivCLM ℝ (Space d) ℝ) η))))
  congr 1e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin dν:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space d, ℝ)⊢ (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ))
    ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν)) ((fderivCLM ℝ (Space d) ℝ) η))) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν))
    ((fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ)) ((fderivCLM ℝ (Space d) ℝ) η)))
  exact SchwartzMap.ext fun x => schwartMap_fderiv_comm μ ν x ηAll goals completed! 🐙

Derivatives on Space

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Derivatives of functions on Space d

A.1. Basic equalities

A.2. Derivative of the constant function

A.3. Derivative distributes over addition and subtraction

A.4. Derivative distributes over scalar multiplication

A.5. Two spatial derivatives commute

A.6. Derivative of a component

A.7. Derivative of a component squared

A.8. Derivivatives of components

A.9. Derivative of a norm squared

A.9.1. Differentiability of the norm squared function

A.9.2. Derivative of the norm squared function

A.10. Derivative of the inner product

A.10.1. Differentiability of the inner product function

A.10.2. Derivative of the inner product function

A.10.3. Derivative of the inner product on one side

A.11. Differentiability of derivatives

B. Derivatives of distributions on Space d

B.1. The definition

B.2. Basic equality

B.3. Commutation of derivatives

A. Derivatives of functions on `Space d`

B. Derivatives of distributions on `Space d`