Thoughts on Fundamental Matrix

Stream: mathlib4

[finegeometer]

Mathlib doesn't have much theory about differential equations. One thing to add might be the fundamental matrix.

Consider the differential equation y' = Ay, where y is a vector and A is a matrix, both depending continuously on x. Let S be the space of solutions to this differential equation. This turns out to be a vector space, and each x yields an obvious linear map φ_x given by φ_x(f) = f(x). Existence-uniqueness shows these φ_x are isomorphisms; the fundamental matrix Φ(x,x_0) is the composition φ_x ∘ φ_{x_0}^{-1}.

This should be reasonably easy to implement, since we already have the existence-uniqueness theorems. But the question is what level of generality to use. As far as I can tell, linearity is mostly a red herring; the concept should work equally well for any differential equation that satisfies existence-uniqueness. The problem is it isn't exactly clear how to express the concept of "differential equation satisfying existence-uniqueness" in Mathlib, in a form suitable for use as a hypothesis.

Alternatively, we could define the fundamental matrix for all differential equations; returning junk values if the solution doesn't exist for long enough. One way to do this might be to construct maximally-extended solutions by constructing the set of all solutions on all intervals, establishing an order by defining f ≤ g if f is a restriction of g to a smaller interval, and applying Zorn's lemma.

So, to those who know Mathlib better than I do, what do you think would be the right design? I figure that's the hard part; the implementation should be comparatively easy.

[Winston Yin (尹維晨)]

What if you just used the minimal assumptions of existence-uniqueness? There’s docs#IsPicardLindelof for example.

[Winston Yin (尹維晨)]

Maximal solution is not yet in mathlib. I’m in the process of generalising the existence theorem to flows (#20704), so maximal solutions are a natural next step. Would welcome any contribution there!