From bf6c19b0e52cb67c3722096e4ca1aefd68569d54 Mon Sep 17 00:00:00 2001
From: juanjfndz <juanjfndz@gmail.com>
Date: Mon, 6 Apr 2026 16:35:35 +0200
Subject: [PATCH 1/3] Add iterated Space derivatives indexed by multi-indices

---
 Physlib.lean                                  |   1 +
 .../Space/Derivatives/Iterated.lean           | 149 ++++++++++++++++++
 2 files changed, 150 insertions(+)
 create mode 100644 Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean

diff --git a/Physlib.lean b/Physlib.lean
index 616caa334..e95ad9fea 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -349,6 +349,7 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Basic
 public import Physlib.SpaceAndTime.Space.Derivatives.Curl
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+public import Physlib.SpaceAndTime.Space.Derivatives.Iterated
 public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian
 public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
 public import Physlib.SpaceAndTime.Space.DistConst
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
new file mode 100644
index 000000000..a4e92dac9
--- /dev/null
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
@@ -0,0 +1,149 @@
+/-
+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
+
+- `Physlib.MultiIndex.toList` : the canonical ordered list of directions encoded by a multi-index.
+- `Space.iteratedDeriv` : iterated coordinate derivatives on `Space d`.
+
+## iii. Table of contents
+
+- A. The combinatorics of iterated directions
+- B. Iterated derivatives on `Space d`
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace Physlib
+
+namespace MultiIndex
+
+variable {d : ℕ}
+
+/-!
+## A. The combinatorics of iterated directions
+
+-/
+
+/-- The tail of a multi-index on `d + 1` coordinates, dropping the `0`-th coordinate. -/
+def tail (I : MultiIndex d.succ) : MultiIndex d := ⟨fun i => I i.succ⟩
+
+/-- The canonical ordered list of coordinate directions encoded by a multi-index. -/
+def toList : {d : ℕ} → MultiIndex d → List (Fin d)
+  | 0, _ => []
+  | _ + 1, I => List.replicate (I 0) 0 ++ (toList (tail I)).map Fin.succ
+
+@[simp]
+lemma tail_zero : tail (0 : MultiIndex d.succ) = 0 := by
+  ext i
+  rfl
+
+@[simp]
+lemma tail_increment_zero (I : MultiIndex d.succ) : tail (increment I 0) = tail I := by
+  ext i
+  simp [tail, increment]
+
+@[simp]
+lemma tail_increment_succ (I : MultiIndex d.succ) (i : Fin d) :
+    tail (increment I i.succ) = increment (tail I) i := by
+  ext j
+  by_cases h : j = i
+  · subst h
+    simp [tail, increment]
+  · simp [tail, increment, h]
+
+@[simp]
+lemma toList_zero : toList (0 : MultiIndex d) = [] := by
+  induction d with
+  | zero => rfl
+  | succ d ih =>
+      simp [toList, ih]
+
+lemma length_toList (I : MultiIndex d) : I.toList.length = I.order := by
+  induction d with
+  | zero =>
+      simp [toList, MultiIndex.order]
+  | succ d ih =>
+      simp [toList, tail, MultiIndex.order, Fin.sum_univ_succ, ih]
+
+@[simp]
+lemma toList_increment_zero (I : MultiIndex d.succ) :
+    toList (increment I 0) = 0 :: toList I := by
+  simp only [toList, increment_apply_same, tail_increment_zero]
+  rw [show I 0 + 1 = 1 + I 0 by omega, List.replicate_add]
+  simp
+
+@[simp]
+lemma toList_single (i : Fin d) : toList (increment 0 i : MultiIndex d) = [i] := by
+  induction d with
+  | zero =>
+      exact Fin.elim0 i
+  | succ d ih =>
+      refine Fin.cases ?_ ?_ i
+      · simp [toList_increment_zero]
+      · intro j
+        have htail :
+            tail (increment (0 : MultiIndex d.succ) j.succ) = increment (0 : MultiIndex d) j := by
+          rw [tail_increment_succ, tail_zero]
+        have hzero : increment (0 : MultiIndex d.succ) j.succ 0 = 0 := by
+          simp [increment]
+        simp [toList, hzero, htail, ih j]
+
+end MultiIndex
+
+end Physlib
+
+namespace Space
+
+open Physlib
+
+variable {M : Type} {d : ℕ}
+
+/-!
+## B. Iterated derivatives on `Space d`
+
+-/
+
+/-- The iterated coordinate derivative on `Space d` indexed by a multi-index. -/
+noncomputable def iteratedDeriv [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
+    (I : MultiIndex d) (f : Space d → M) : Space d → M :=
+  I.toList.foldr (fun i g => deriv i g) f
+
+@[simp]
+lemma iteratedDeriv_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
+    (f : Space d → M) : iteratedDeriv (0 : MultiIndex d) f = f := by
+  simp [iteratedDeriv, Physlib.MultiIndex.toList_zero]
+
+@[simp]
+lemma iteratedDeriv_increment_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
+    (I : MultiIndex d.succ) (f : Space d.succ → M) :
+    iteratedDeriv (MultiIndex.increment I 0) f = ∂[0] (iteratedDeriv I f) := by
+  simp [iteratedDeriv, Physlib.MultiIndex.toList_increment_zero]
+
+@[simp]
+lemma iteratedDeriv_single [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
+    (i : Fin d) (f : Space d → M) :
+    iteratedDeriv (MultiIndex.increment 0 i) f = ∂[i] f := by
+  simp [iteratedDeriv, Physlib.MultiIndex.toList_single]
+
+end Space

From 227ecca197319fe288527e38606a68ca36c955ec Mon Sep 17 00:00:00 2001
From: juanjfndz <juanjfndz@gmail.com>
Date: Tue, 7 Apr 2026 17:30:33 +0200
Subject: [PATCH 2/3] Move MultiIndex combinatorics and add iterated-derivative
 notation

---
 .../Space/Derivatives/Iterated.lean           | 93 ++-----------------
 .../Space/Derivatives/MultiIndex.lean         | 72 ++++++++++++++
 2 files changed, 80 insertions(+), 85 deletions(-)

diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
index a4e92dac9..d46abc2dc 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
@@ -20,13 +20,12 @@ of coordinate directions, and the iterated derivative is then defined by repeate
 
 ## ii. Key results
 
-- `Physlib.MultiIndex.toList` : the canonical ordered list of directions encoded by a multi-index.
 - `Space.iteratedDeriv` : iterated coordinate derivatives on `Space d`.
+- `∂^[I] f` : notation for the iterated derivative indexed by the multi-index `I`.
 
 ## iii. Table of contents
 
-- A. The combinatorics of iterated directions
-- B. Iterated derivatives on `Space d`
+- A. Iterated derivatives on `Space d`
 
 ## iv. References
 
@@ -34,85 +33,6 @@ of coordinate directions, and the iterated derivative is then defined by repeate
 
 @[expose] public section
 
-namespace Physlib
-
-namespace MultiIndex
-
-variable {d : ℕ}
-
-/-!
-## A. The combinatorics of iterated directions
-
--/
-
-/-- The tail of a multi-index on `d + 1` coordinates, dropping the `0`-th coordinate. -/
-def tail (I : MultiIndex d.succ) : MultiIndex d := ⟨fun i => I i.succ⟩
-
-/-- The canonical ordered list of coordinate directions encoded by a multi-index. -/
-def toList : {d : ℕ} → MultiIndex d → List (Fin d)
-  | 0, _ => []
-  | _ + 1, I => List.replicate (I 0) 0 ++ (toList (tail I)).map Fin.succ
-
-@[simp]
-lemma tail_zero : tail (0 : MultiIndex d.succ) = 0 := by
-  ext i
-  rfl
-
-@[simp]
-lemma tail_increment_zero (I : MultiIndex d.succ) : tail (increment I 0) = tail I := by
-  ext i
-  simp [tail, increment]
-
-@[simp]
-lemma tail_increment_succ (I : MultiIndex d.succ) (i : Fin d) :
-    tail (increment I i.succ) = increment (tail I) i := by
-  ext j
-  by_cases h : j = i
-  · subst h
-    simp [tail, increment]
-  · simp [tail, increment, h]
-
-@[simp]
-lemma toList_zero : toList (0 : MultiIndex d) = [] := by
-  induction d with
-  | zero => rfl
-  | succ d ih =>
-      simp [toList, ih]
-
-lemma length_toList (I : MultiIndex d) : I.toList.length = I.order := by
-  induction d with
-  | zero =>
-      simp [toList, MultiIndex.order]
-  | succ d ih =>
-      simp [toList, tail, MultiIndex.order, Fin.sum_univ_succ, ih]
-
-@[simp]
-lemma toList_increment_zero (I : MultiIndex d.succ) :
-    toList (increment I 0) = 0 :: toList I := by
-  simp only [toList, increment_apply_same, tail_increment_zero]
-  rw [show I 0 + 1 = 1 + I 0 by omega, List.replicate_add]
-  simp
-
-@[simp]
-lemma toList_single (i : Fin d) : toList (increment 0 i : MultiIndex d) = [i] := by
-  induction d with
-  | zero =>
-      exact Fin.elim0 i
-  | succ d ih =>
-      refine Fin.cases ?_ ?_ i
-      · simp [toList_increment_zero]
-      · intro j
-        have htail :
-            tail (increment (0 : MultiIndex d.succ) j.succ) = increment (0 : MultiIndex d) j := by
-          rw [tail_increment_succ, tail_zero]
-        have hzero : increment (0 : MultiIndex d.succ) j.succ 0 = 0 := by
-          simp [increment]
-        simp [toList, hzero, htail, ih j]
-
-end MultiIndex
-
-end Physlib
-
 namespace Space
 
 open Physlib
@@ -120,7 +40,7 @@ open Physlib
 variable {M : Type} {d : ℕ}
 
 /-!
-## B. Iterated derivatives on `Space d`
+## A. Iterated derivatives on `Space d`
 
 -/
 
@@ -129,6 +49,9 @@ noncomputable def iteratedDeriv [AddCommGroup M] [Module ℝ M] [TopologicalSpac
     (I : MultiIndex d) (f : Space d → M) : Space d → M :=
   I.toList.foldr (fun i g => deriv i g) f
 
+@[inherit_doc iteratedDeriv]
+macro "∂^[" I:term "]" : term => `(iteratedDeriv $I)
+
 @[simp]
 lemma iteratedDeriv_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
     (f : Space d → M) : iteratedDeriv (0 : MultiIndex d) f = f := by
@@ -137,13 +60,13 @@ lemma iteratedDeriv_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
 @[simp]
 lemma iteratedDeriv_increment_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
     (I : MultiIndex d.succ) (f : Space d.succ → M) :
-    iteratedDeriv (MultiIndex.increment I 0) f = ∂[0] (iteratedDeriv I f) := by
+    ∂^[MultiIndex.increment I 0] f = ∂[0] (∂^[I] f) := by
   simp [iteratedDeriv, Physlib.MultiIndex.toList_increment_zero]
 
 @[simp]
 lemma iteratedDeriv_single [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
     (i : Fin d) (f : Space d → M) :
-    iteratedDeriv (MultiIndex.increment 0 i) f = ∂[i] f := by
+    ∂^[MultiIndex.increment 0 i] f = ∂[i] f := by
   simp [iteratedDeriv, Physlib.MultiIndex.toList_single]
 
 end Space
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
index f76657402..c42570152 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
@@ -7,6 +7,7 @@ Authors: Juan Jose Fernandez Morales
 module
 
 public import Mathlib.Algebra.BigOperators.Pi
+public import Mathlib.Algebra.BigOperators.Fin
 
 /-!
 # Multi-indices
@@ -24,12 +25,14 @@ Theory development.
 - `Physlib.MultiIndex` : multi-indices on `d` coordinates.
 - `MultiIndex.order` : the order `|I|` of a multi-index.
 - `MultiIndex.increment` : increment a single coordinate of a multi-index.
+- `MultiIndex.toList` : the canonical ordered list of directions encoded by a multi-index.
 
 ## iii. Table of contents
 
 - A. The basic type of multi-indices
   - A.1. Basic operations
   - A.2. Basic lemmas
+  - A.3. Canonical ordered lists of directions
 
 ## iv. References
 
@@ -126,6 +129,75 @@ lemma order_increment (I : MultiIndex d) (i : Fin d) :
     order (increment I i) = order I + 1 := by
   simp [increment, order, Finset.sum_add_distrib]
 
+/-!
+### A.3. Canonical ordered lists of directions
+
+-/
+
+/-- The tail of a multi-index on `d + 1` coordinates, dropping the `0`-th coordinate. -/
+def tail (I : MultiIndex d.succ) : MultiIndex d := ⟨fun i => I i.succ⟩
+
+/-- The canonical ordered list of coordinate directions encoded by a multi-index. -/
+def toList : {d : ℕ} → MultiIndex d → List (Fin d)
+  | 0, _ => []
+  | _ + 1, I => List.replicate (I 0) 0 ++ (toList (tail I)).map Fin.succ
+
+@[simp]
+lemma tail_zero : tail (0 : MultiIndex d.succ) = 0 := by
+  ext i
+  rfl
+
+@[simp]
+lemma tail_increment_zero (I : MultiIndex d.succ) : tail (increment I 0) = tail I := by
+  ext i
+  simp [tail, increment]
+
+@[simp]
+lemma tail_increment_succ (I : MultiIndex d.succ) (i : Fin d) :
+    tail (increment I i.succ) = increment (tail I) i := by
+  ext j
+  by_cases h : j = i
+  · subst h
+    simp [tail, increment]
+  · simp [tail, increment, h]
+
+@[simp]
+lemma toList_zero : toList (0 : MultiIndex d) = [] := by
+  induction d with
+  | zero => rfl
+  | succ d ih =>
+      simp [toList, ih]
+
+lemma length_toList (I : MultiIndex d) : I.toList.length = I.order := by
+  induction d with
+  | zero =>
+      simp [toList, MultiIndex.order]
+  | succ d ih =>
+      simp [toList, tail, MultiIndex.order, Fin.sum_univ_succ, ih]
+
+@[simp]
+lemma toList_increment_zero (I : MultiIndex d.succ) :
+    toList (increment I 0) = 0 :: toList I := by
+  simp only [toList, increment_apply_same, tail_increment_zero]
+  rw [show I 0 + 1 = 1 + I 0 by omega, List.replicate_add]
+  simp
+
+@[simp]
+lemma toList_single (i : Fin d) : toList (increment 0 i : MultiIndex d) = [i] := by
+  induction d with
+  | zero =>
+      exact Fin.elim0 i
+  | succ d ih =>
+      refine Fin.cases ?_ ?_ i
+      · simp [toList_increment_zero]
+      · intro j
+        have htail :
+            tail (increment (0 : MultiIndex d.succ) j.succ) = increment (0 : MultiIndex d) j := by
+          rw [tail_increment_succ, tail_zero]
+        have hzero : increment (0 : MultiIndex d.succ) j.succ 0 = 0 := by
+          simp [increment]
+        simp [toList, hzero, htail, ih j]
+
 end MultiIndex
 
 end Physlib

From 0f5ab7f5015163996d87e34dba531224cb4620a7 Mon Sep 17 00:00:00 2001
From: juanjfndz <juanjfndz@gmail.com>
Date: Tue, 7 Apr 2026 20:01:48 +0200
Subject: [PATCH 3/3] Use iterated-derivative notation consistently in Iterated

---
 Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
index d46abc2dc..47be77d1a 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
@@ -54,7 +54,7 @@ macro "∂^[" I:term "]" : term => `(iteratedDeriv $I)
 
 @[simp]
 lemma iteratedDeriv_zero [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
-    (f : Space d → M) : iteratedDeriv (0 : MultiIndex d) f = f := by
+    (f : Space d → M) : ∂^[0] f = f := by
   simp [iteratedDeriv, Physlib.MultiIndex.toList_zero]
 
 @[simp]