Zulip Chat Archive
Stream: general
Topic: Control theory for LTI systems
Joh-Tob Schäg (Mar 22 2023 at 14:39):
How much work would it be to implement
- Laplace transform and inverse laplace transform for linear systems
- closing feedback loops and connecting up such systems with linear or at worst affine functions
- sensitivity functions, frequency response curves, their approximation by piece wise linear functions
- characteristic polynomials
- solutions to the linear system:
- exponential stability, BIBO stability
- Hurwitz criteria
- step response, bode and nyquist diagrams
- limits and lapace transform
- simple measure of robustness
- proving certain statements about feedback controllers
- delay differential equations (atleast in laplace space)
Is see the 1D case (A has one algebraic eigen value whose geometric EV is the dimension of the matrix, u(t) and y(t) are scalar functions) as a bit simpler. It would require of solutions of complex solutions to real polynomials.
In the multidimensional case Jordan decompositions, the matrix exponential would be needed and theorems about observability, contrability, reachability, stabilisability become interesting, so so state-estimaters, maybe even kalman filters.
What of those is already being worked on?
Kevin Buzzard (Mar 22 2023 at 14:47):
Several person-years at least? And several more if you actually wanted to run the functions and get answers as opposed to just being able to prove theorems about them.
Joh-Tob Schäg (Mar 22 2023 at 14:52):
I guess that dampens my ambition a bit. :flushed:
Eric Wieser (Mar 22 2023 at 14:56):
This is something I'd be interested in, although probably won't have time to look at before my PhD concludes.
Joh-Tob Schäg (Mar 22 2023 at 14:57):
Is there an easy way for me to comprehend why that would be so hard?
Eric Wieser (Mar 22 2023 at 14:58):
In the multidimensional case Jordan decompositions
This is definitely within reach. Assuming I've not muddled unrelated things, there are two threas about it here: #maths > jordan normal form and #maths > jordan-chevalley decomposition . The first was blocked by something that's now in mathlib.
the matrix exponential would be needed
docs#matrix.exp_add_of_commute exists!
Johan Commelin (Mar 22 2023 at 14:59):
@Joh-Tob Schäg This is quite far from my mathematical area of expertise. But how long would it take you to explain all of this to a student who only knows the most basic calculus and analysis?
Now imagine that this student makes you pause and explain in more detail whenever a step is not super-explicitly-obvious from previous lemmas...
Eric Wieser (Mar 22 2023 at 15:03):
characteristic polynomials
docs#matrix.aeval_self_charpoly is likely one of the statements you're looking for
Eric Wieser (Mar 22 2023 at 15:06):
(I talked very briefly about how mathlib had some of the prerequisites for control theory in these slides)
Kevin Buzzard (Mar 22 2023 at 15:08):
Joh-Tob Schäg said:
Is there an easy way for me to comprehend why that would be so hard?
One issue is finding the right person for the job. Another issue is that contour integration is still very much a work in progress.
Joh-Tob Schäg (Mar 22 2023 at 16:12):
Multidimensional route:
We define a thing called the matrix exponential. We show that it is absolutetly convergent. We introduce exp(tA) we show it's properties with regard to derivative using absolute convergence. We introduce the Jordan normal form and connect that to eigenvalues. We show that for matrixes in jordan form the jordan blocks and matrix exponential give us the solution (relies on Cayley-Hamilton). We show that the solution to the jordan block system can be mapped to the originial solution (using exp(inv(T) X T) = inv(T)exp(J)T We can now solve linear homogenous time-invariant ODEs. https://en.wikipedia.org/wiki/Cauchy%E2%80%93Euler_equation is relevant here. We give linearity results. We introduce intial conditions. Using "Variation of parameters" (or something else) we proof the formula for affine differential equations we might need https://de.wikipedia.org/wiki/Picard-Iteration for that.
We define a with inputs and outputs as a system.
We define the act of connecting systems using linear/affine transforms of $y$s into $u$s. We define the reduction rules which allow to do a (surjective?) mapping of networks of systems into one system while preserving the same dynamics. It might be good to do that without feedback first. Then we do that with feedback. We define exponential stability, BIBO stability, Hurwitz criteria. We can introduce observability, controlability, reachability, stabelisability and their subspace and we would need rank based arguements here.
That's how far we get without laplace transforms of $$\mathbb{R}^n \mapsto \mathbb{R}^m} functions.
Laplace route (1D):
We take a theory of rational functions in one variable. We define abstract integral transformations, Laplace transformation, inverve lapalace transformation.
We do a 1 D solution theory for Cauchy-Euler equations. We define and proof the laplace transforms we need. We define and proof the rules we need which don't follow from integral transform.
We define exponential stability, stability. We define define tying transfer functions together, properness, transfer functions with multi inputs which all share a common s, show some obvious properties, define a particular type of transfer functionnetwork called a standard control loop. Define exponential stability, BIBO stability, (limits of lapace transform) show Hurrwitz criteria. Show many simple algebraic properties in Laplace space.
Show some properties of a thing called step response. Define some computeable properties of transfer functions. We proof that some common rule of thumbs for particular forms of transfer functions aren't horrible. We define constraints on implementability. Define some non standard control loops.
Cauchy's integral formula (no idea how to proof that). Define Nyquist-criteria. Define some define some properties of the nyquist plot. Define bode plot, proof limit on the badness of the piece wise linear approximation. Define some more common controller designs strategies and show that they work.
Honestly the laplace route sounds like a lot more of a pain and note that those are a bit pedestrian paths. There might be some category theory level stuff to cut that down a lot.
There is another approachable area for control theory of difference equations. You basically need the same linear algebra as in Multidimensional route but have less problems with difference equations. The Z transform sould be easier to deal with than the s transform if we have a good coverage of sequences and series. No matrix exponential to worry about.
Which reminds me. All those are covered under systems theory. They have a nice abstraction called a state transition function that might cut off some properties for all of those.
Eric Wieser (Mar 22 2023 at 17:09):
using exp(inv(T) X T) = inv(T)exp(J)T
docs#matrix.exp_conj' is this result
Adam Nemecek (Mar 27 2023 at 00:12):
are you folks aware of the work done by steven gray on the connection between hopf algebras and LTI? for example https://arxiv.org/pdf/1805.02954.pdf
Last updated: Dec 20 2023 at 11:08 UTC