%0 DATA
%A Omar Ahmad, Jasim
%A Sandor, Veres
%D 2020
%T Formal proof of the small-gain theorem by interactive theorem proving
%U https://figshare.shef.ac.uk/articles/software/Formal_proof_of_the_small-gain_theorem_by_interactive_theorem_proving/11791449
%R 10.15131/shef.data.11791449
%2 https://figshare.shef.ac.uk/ndownloader/files/21520572
%2 https://figshare.shef.ac.uk/ndownloader/files/21520575
%2 https://figshare.shef.ac.uk/ndownloader/files/21520581
%K Isabelle/HOL
%K formal verification
%K control theory
%X 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".