Email Gateway (Aug 23 2022 at 09:06): Email Gateway (Aug 23 2022 at 09:06):From: Manuel Eberl <eberlm@in.tum.de>
Matrices for ODEs
by Jonathan Julian Huerta y Munive
Our theories formalise various matrix properties that serve to establish
existence, uniqueness and characterisation of the solution to affine
systems of ordinary differential equations (ODEs). In particular, we
formalise the operator and maximum norm of matrices. Then we use them to
prove that square matrices form a Banach space, and in this setting, we
show an instance of Picard-Lindelöf’s theorem for affine systems of
ODEs. Finally, we use this formalisation to verify three simple hybrid
programs.
https://www.isa-afp.org/entries/Matrices_for_ODEs.html
Enjoy,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC