[isabelle] New in the AFP: Matrices for ODEs

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.