Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Matrices for ODEs


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC