Add iterated Space derivatives indexed by multi-indices

[juanjfndz]

Summary

This PR is the second step in a planned local Classical Field Theory development for PhysLib, aimed at a formalization of the local Euler--Lagrange criterion appearing as Theorem 5.2 in Cortés--Haupt, Chapter 5.

The overall local stack is intended to proceed through:

• multi-indices and iterated derivatives,
• admissible compactly supported variations,
• local jets,
• total derivatives,
• local lagrangians and the action functional,
• the local Euler--Lagrange operator,
• and finally the first-variation criterion.

The Zulip discussion for this development is here:

• https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib/topic/ClassicalFieldTheory/

The previous PR, #1021, introduced the reusable MultiIndex API. This PR extends that API with the canonical ordered list of directions associated to a multi-index, and then uses it to define iterated coordinate derivatives on Space d.

What This PR Adds

This PR adds Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean, updates Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean, and adds the corresponding import in Physlib.lean.

Concretely, it provides:

• MultiIndex.tail,
• MultiIndex.toList,
• MultiIndex.length_toList,
• the definition Space.iteratedDeriv,
• the notation ∂^[I] f,
• and the first basic lemmas identifying the order-zero and one-step cases.

In particular, the API already gives the expected specializations

∂^[0] f = f

and

∂^[increment I 0] f = ∂[0] (∂^[I] f)

as well as the single-direction case

∂^[increment 0 i] f = ∂[i] f.

Why This Is Needed

The previous PR, #1021, provided the combinatorial indexing layer. This PR supplies both the canonical ordered realization of a multi-index and the corresponding analytic notion of iterated coordinate derivative.

Later PRs will use iterated derivatives to define the local jet evaluation

j^k_x f

by collecting the derivative coordinates of a field up to order k.

These derivatives are also the local analytic input for the jet coordinates

u^a_I

and hence for local lagrangians depending on derivatives up to order k.

So this PR is the first analytic bridge between the reusable indexing object from MultiIndex and the later local field-theory constructions.

Scope Of This PR

This PR is intentionally limited to the core definition and its first basic recursion/specialization lemmas.

It does not yet add:

• linearity lemmas,
• smoothness preservation lemmas,
• or support lemmas for iterated derivatives.

Those will appear in the follow-up PR, so that the basic notion of iterated derivative can be reviewed separately before adding the later technical API needed for local jets and first variation.

Build

Locally checked with:

• python3 scripts/lint-style.py Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
• lake build Physlib.SpaceAndTime.Space.Derivatives.MultiIndex Physlib.SpaceAndTime.Space.Derivatives.Iterated
• lake build Physlib
• lake exe check_file_imports

[jstoobysmith]

These results about MultiIndex are probably best placed in that file not this one.

[jstoobysmith]

I think it would be nice to define some notation for this, so we don't have to use iteratedDeriv everywhere.

[juanjfndz]

That makes sense. Before changing the API, two notation candidates that seem most natural to me here are:

• ∂^[I] f, to stay close to the standard mathematical notation ∂^I f while still making the multi-index argument visually explicit in Lean;
• ∂[I] f, as the lighter-weight option, in continuity with the existing first-order notation ∂[i] f.

My preference would currently be the first one, but I would be happy to go with either if you think one fits PhysLib style better.

[jstoobysmith]

I think the first one is good, keeping the brackets might make it easier to define.

[juanjfndz]

Thanks — I have now updated this accordingly.

Concretely:

• the purely combinatorial MultiIndex material (tail, toList, and the associated lemmas) has been moved into Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean,
• and the iterated-derivative notation has been added in the form ∂^[I].

[jstoobysmith]

could use the notation here aswell.

[juanjfndz]

Sorry — this should have been consistent already.

I have now made the notation consistent in Iterated.lean as well, and updated the PR description so that it matches the current diff.

[jstoobysmith]

Great - approved. Many thanks, will merge shortly