Formal proof of the small-gain theorem by interactive theorem proving
JasimOmar Ahmad
VeresSandor
2020
<div>This is source code of the formal proof of the Small-gain theorem in Isabelle/HOL theorem prover. This code is part of the paper "Towards Formal Proofs of Feedback Control Theory" presented in System Theory, Control and Computing (ICSTCC) conference published in IEEE - DOI: 10.1109/ICSTCC.2017.8107009 <br></div><div><br></div><div>Note: Put both files "L2Norm_Integral.thy" and
"Minkowski_Integral_Inequality.thy" in the main Isabelle's directory
before loading the main theorem file "Small_Gain_Theorem.thy".</div>