Formal proof of the small-gain theorem by interactive theorem proving

2020-02-04T12:01:51Z (GMT) by Omar Ahmad Jasim Sandor Veres
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

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".