Physlib.SpaceAndTime.Space.Derivatives.Iterated

Imports

/-
Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Juan Jose Fernandez Morales
-/
module

public import Physlib.SpaceAndTime.Space.Derivatives.Basic
public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex

Iterated derivatives on `Space d`

i. Overview

This module defines iterated coordinate derivatives on Space d indexed by multi-indices.

The implementation is intentionally modest. A multi-index is first expanded into a canonical list of coordinate directions, and the iterated derivative is then defined by repeated application of Space.deriv along that list.

ii. Key results

Space.iteratedDeriv : iterated coordinate derivatives on Space d.

∂^[I] f : notation for the iterated derivative indexed by the multi-index I.

Space.iteratedDeriv_add, Space.iteratedDeriv_const_smul : algebraic compatibility for smooth scalar-valued functions.

Space.iteratedDeriv_contDiff : smooth scalar-valued functions remain smooth after iterated coordinate differentiation.

Space.tsupport_iteratedDeriv_subset : the support of an iterated spatial derivative is contained in that of the original function.

iii. Table of contents

A. Iterated derivatives on Space d

B. Algebraic and regularity lemmas

C. Support lemmas

iv. References

@[expose] public section

A. Iterated derivatives on `Space d`

              @[inherit_doc iteratedDeriv]
macro "∂^[" I:term "]" : term => `(iteratedDeriv $I)private lemma iteratedDerivList_contDiff (L : List (Fin d)) {f : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) :
    ContDiff ℝ ∞ (L.foldr (fun i g => deriv i g) f) := byd:ℕL:List (Fin d)f:Space d → ℝhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ (List.foldr (fun i g => deriv i g) f L)
  induction L generalizing f with
  | nil =>nild:ℕf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ (List.foldr (fun i g => deriv i g) f []) simpa using hfAll goals completed! 🐙
  | cons i L ih =>consd:ℕi:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ}, ContDiff ℝ ∞ f → ContDiff ℝ ∞ (List.foldr (fun i g => deriv i g) f L)f:Space d → ℝhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ (List.foldr (fun i g => deriv i g) f (i :: L)) exact (contDiff_apply ℝ ℝ i).comp (Space.deriv_contDiff (n := ∞) (ih hf))All goals completed! 🐙private lemma iteratedDerivList_add (L : List (Fin d)) {f g : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g) :
    L.foldr (fun i h => deriv i h) (f + g) =
      L.foldr (fun i h => deriv i h) f + L.foldr (fun i h => deriv i h) g := byd:ℕL:List (Fin d)f:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ List.foldr (fun i h => deriv i h) (f + g) L =
  List.foldr (fun i h => deriv i h) f L + List.foldr (fun i h => deriv i h) g L
  induction L generalizing f g with
  | nil =>nild:ℕf:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ List.foldr (fun i h => deriv i h) (f + g) [] =
  List.foldr (fun i h => deriv i h) f [] + List.foldr (fun i h => deriv i h) g [] rflAll goals completed! 🐙
  | cons i L ih =>consd:ℕi:Fin dL:List (Fin d)ih:∀ {f g : Space d → ℝ},
  ContDiff ℝ ∞ f →
    ContDiff ℝ ∞ g →
      List.foldr (fun i h => deriv i h) (f + g) L =
        List.foldr (fun i h => deriv i h) f L + List.foldr (fun i h => deriv i h) g Lf:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ List.foldr (fun i h => deriv i h) (f + g) (i :: L) =
  List.foldr (fun i h => deriv i h) f (i :: L) + List.foldr (fun i h => deriv i h) g (i :: L)
      simp only [List.foldr, ih hf hg]consd:ℕi:Fin dL:List (Fin d)ih:∀ {f g : Space d → ℝ},
  ContDiff ℝ ∞ f →
    ContDiff ℝ ∞ g →
      List.foldr (fun i h => deriv i h) (f + g) L =
        List.foldr (fun i h => deriv i h) f L + List.foldr (fun i h => deriv i h) g Lf:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ deriv i (List.foldr (fun i h => deriv i h) f L + List.foldr (fun i h => deriv i h) g L) =
  deriv i (List.foldr (fun i h => deriv i h) f L) + deriv i (List.foldr (fun i h => deriv i h) g L)
      exact Space.deriv_add _ _ ((iteratedDerivList_contDiff L hf).differentiable (byd:ℕi:Fin dL:List (Fin d)ih:∀ {f g : Space d → ℝ},
  ContDiff ℝ ∞ f →
    ContDiff ℝ ∞ g →
      List.foldr (fun i h => deriv i h) (f + g) L =
        List.foldr (fun i h => deriv i h) f L + List.foldr (fun i h => deriv i h) g Lf:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ ∞ ≠ 0 simpAll goals completed! 🐙))
        ((iteratedDerivList_contDiff L hg).differentiable (byd:ℕi:Fin dL:List (Fin d)ih:∀ {f g : Space d → ℝ},
  ContDiff ℝ ∞ f →
    ContDiff ℝ ∞ g →
      List.foldr (fun i h => deriv i h) (f + g) L =
        List.foldr (fun i h => deriv i h) f L + List.foldr (fun i h => deriv i h) g Lf:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ ∞ ≠ 0 simpAll goals completed! 🐙))private lemma iteratedDerivList_const_smul (L : List (Fin d)) (c : ℝ) {f : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) :
    L.foldr (fun i h => deriv i h) (c • f) =
      c • L.foldr (fun i h => deriv i h) f := byd:ℕL:List (Fin d)c:ℝf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ List.foldr (fun i h => deriv i h) (c • f) L = c • List.foldr (fun i h => deriv i h) f L
  induction L generalizing f with
  | nil =>nild:ℕc:ℝf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ List.foldr (fun i h => deriv i h) (c • f) [] = c • List.foldr (fun i h => deriv i h) f [] rflAll goals completed! 🐙
  | cons i L ih =>consd:ℕc:ℝi:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ},
  ContDiff ℝ ∞ f → List.foldr (fun i h => deriv i h) (c • f) L = c • List.foldr (fun i h => deriv i h) f Lf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ List.foldr (fun i h => deriv i h) (c • f) (i :: L) = c • List.foldr (fun i h => deriv i h) f (i :: L)
      simp only [List.foldr, ih hf]consd:ℕc:ℝi:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ},
  ContDiff ℝ ∞ f → List.foldr (fun i h => deriv i h) (c • f) L = c • List.foldr (fun i h => deriv i h) f Lf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ deriv i (c • List.foldr (fun i h => deriv i h) f L) = c • deriv i (List.foldr (fun i h => deriv i h) f L)
      exact Space.deriv_const_smul c ((iteratedDerivList_contDiff L hf).differentiable (byd:ℕc:ℝi:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ},
  ContDiff ℝ ∞ f → List.foldr (fun i h => deriv i h) (c • f) L = c • List.foldr (fun i h => deriv i h) f Lf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ ∞ ≠ 0 simpAll goals completed! 🐙))@[simp]
lemma iteratedDeriv_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (f : Space d → M) : ∂^[0] f = f := byM:Typed:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mf:Space d → M⊢ iteratedDeriv 0 f = f
  simp [iteratedDeriv, Physlib.MultiIndex.toList_zero]All goals completed! 🐙@[simp]
lemma iteratedDeriv_increment_zero [NeZero d] [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (I : MultiIndex d) (f : Space d → M) :
    ∂^[MultiIndex.increment I 0] f = ∂[0] (∂^[I] f) := byM:Typed:ℕinst✝³:NeZero dinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace MI:MultiIndex df:Space d → M⊢ iteratedDeriv (I.increment 0) f = deriv 0 (iteratedDeriv I f)
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne d)M:Typeinst✝³:AddCommGroup Minst✝²:Module ℝ Minst✝¹:TopologicalSpace Mn:ℕinst✝:NeZero n.succI:MultiIndex n.succf:Space n.succ → M⊢ iteratedDeriv (I.increment 0) f = deriv 0 (iteratedDeriv I f)
  simp [iteratedDeriv, Physlib.MultiIndex.toList_increment_zero]All goals completed! 🐙@[simp]
lemma iteratedDeriv_single [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (i : Fin d) (f : Space d → M) :
    ∂^[MultiIndex.increment 0 i] f = ∂[i] f := byM:Typed:ℕinst✝²:AddCommGroup Minst✝¹:Module ℝ Minst✝:TopologicalSpace Mi:Fin df:Space d → M⊢ iteratedDeriv (MultiIndex.increment 0 i) f = deriv i f
  simp [iteratedDeriv, Physlib.MultiIndex.toList_single]All goals completed! 🐙lemma iteratedDeriv_add (I : MultiIndex d) {f g : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g) :
    ∂^[I] (f + g) = ∂^[I] f + ∂^[I] g := byd:ℕI:MultiIndex df:Space d → ℝg:Space d → ℝhf:ContDiff ℝ ∞ fhg:ContDiff ℝ ∞ g⊢ iteratedDeriv I (f + g) = iteratedDeriv I f + iteratedDeriv I g
  simpa [iteratedDeriv] using iteratedDerivList_add I.toList hf hgAll goals completed! 🐙lemma iteratedDeriv_const_smul (I : MultiIndex d) (c : ℝ) {f : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) :
    ∂^[I] (c • f) = c • ∂^[I] f := byd:ℕI:MultiIndex dc:ℝf:Space d → ℝhf:ContDiff ℝ ∞ f⊢ iteratedDeriv I (c • f) = c • iteratedDeriv I f
  simpa [iteratedDeriv] using iteratedDerivList_const_smul I.toList c hfAll goals completed! 🐙

Iterated spatial derivatives preserve smoothness for scalar-valued functions.

lemma iteratedDeriv_contDiff (I : MultiIndex d) {f : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) :
    ContDiff ℝ ∞ (∂^[I] f) := byd:ℕI:MultiIndex df:Space d → ℝhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ (iteratedDeriv I f)
  simpa [iteratedDeriv] using iteratedDerivList_contDiff I.toList hfAll goals completed! 🐙

The topological support of a spatial derivative is contained in that of the original function.

lemma tsupport_deriv_subset (i : Fin d) {f : Space d → ℝ} :
    tsupport (deriv i f) ⊆ tsupport f := byd:ℕi:Fin df:Space d → ℝ⊢ tsupport (deriv i f) ⊆ tsupport f
  simpa [deriv_eq_fderiv_fun] using
    (tsupport_fderiv_apply_subset (𝕜 := ℝ) (f := fun x => f x) (v := basis i))All goals completed! 🐙

private lemma iteratedDerivList_commute_deriv (L : List (Fin d)) (i : Fin d)
    {f : Space d → ℝ} (hf : ContDiff ℝ ∞ f) :
    L.foldr (fun j g => deriv j g) (deriv i f) =
      deriv i (L.foldr (fun j g => deriv j g) f) := byd:ℕL:List (Fin d)i:Fin df:Space d → ℝhf:ContDiff ℝ ∞ f⊢ List.foldr (fun j g => deriv j g) (deriv i f) L = deriv i (List.foldr (fun j g => deriv j g) f L)
  induction L generalizing f with
  | nil =>nild:ℕi:Fin df:Space d → ℝhf:ContDiff ℝ ∞ f⊢ List.foldr (fun j g => deriv j g) (deriv i f) [] = deriv i (List.foldr (fun j g => deriv j g) f []) rflAll goals completed! 🐙
  | cons j L ih =>consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ},
  ContDiff ℝ ∞ f → List.foldr (fun j g => deriv j g) (deriv i f) L = deriv i (List.foldr (fun j g => deriv j g) f L)f:Space d → ℝhf:ContDiff ℝ ∞ f⊢ List.foldr (fun j g => deriv j g) (deriv i f) (j :: L) = deriv i (List.foldr (fun j g => deriv j g) f (j :: L))
      simp only [List.foldr, ih hf]consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ},
  ContDiff ℝ ∞ f → List.foldr (fun j g => deriv j g) (deriv i f) L = deriv i (List.foldr (fun j g => deriv j g) f L)f:Space d → ℝhf:ContDiff ℝ ∞ f⊢ deriv j (deriv i (List.foldr (fun j g => deriv j g) f L)) = deriv i (deriv j (List.foldr (fun j g => deriv j g) f L))
      exact Space.deriv_commute _
        ((iteratedDerivList_contDiff L hf).of_le (WithTop.coe_le_coe.mpr le_top))All goals completed! 🐙

An extra spatial derivative commutes with iterated spatial derivatives for smooth scalar-valued functions.

lemma deriv_iteratedDeriv_commute (i : Fin d) (I : MultiIndex d) {f : Space d → ℝ}
    (hf : ContDiff ℝ ∞ f) :
    deriv i (∂^[I] f) = ∂^[I] (deriv i f) := byd:ℕi:Fin dI:MultiIndex df:Space d → ℝhf:ContDiff ℝ ∞ f⊢ deriv i (iteratedDeriv I f) = iteratedDeriv I (deriv i f)
  simpa [iteratedDeriv] using (iteratedDerivList_commute_deriv I.toList i hf).symmAll goals completed! 🐙

private lemma tsupport_iteratedDerivList_subset (L : List (Fin d)) {f : Space d → ℝ} :
    tsupport (L.foldr (fun i g => deriv i g) f) ⊆ tsupport f := byd:ℕL:List (Fin d)f:Space d → ℝ⊢ tsupport (List.foldr (fun i g => deriv i g) f L) ⊆ tsupport f
  induction L generalizing f with
  | nil =>nild:ℕf:Space d → ℝ⊢ tsupport (List.foldr (fun i g => deriv i g) f []) ⊆ tsupport f simpAll goals completed! 🐙
  | cons i L ih =>consd:ℕi:Fin dL:List (Fin d)ih:∀ {f : Space d → ℝ}, tsupport (List.foldr (fun i g => deriv i g) f L) ⊆ tsupport ff:Space d → ℝ⊢ tsupport (List.foldr (fun i g => deriv i g) f (i :: L)) ⊆ tsupport f simpa [List.foldr] using (tsupport_deriv_subset i).trans ihAll goals completed! 🐙

The topological support of an iterated spatial derivative is contained in that of the original function.

lemma tsupport_iteratedDeriv_subset (I : MultiIndex d) {f : Space d → ℝ} :
    tsupport (∂^[I] f) ⊆ tsupport f := byd:ℕI:MultiIndex df:Space d → ℝ⊢ tsupport (iteratedDeriv I f) ⊆ tsupport f
  simpa [iteratedDeriv] using tsupport_iteratedDerivList_subset I.toList (f := f)All goals completed! 🐙

An iterated spatial derivative vanishes outside the topological support of the original function.

lemma iteratedDeriv_eq_zero_of_notMem_tsupport (I : MultiIndex d) {f : Space d → ℝ} {x : Space d}
    (hx : x ∉ tsupport f) :
    ∂^[I] f x = 0 :=
  image_eq_zero_of_notMem_tsupport fun h => hx (tsupport_iteratedDeriv_subset I h)

Iterated derivatives on Space d