Formalizing information theory in Lean 4: divergences, hypothesis testing and the data processing inequality

Questa tesi presenta la formalizzazione di risultati chiave del progetto “Lower bounds for hypothesis testing based on information theory” utilizzando l'interactive theorem prover Lean 4. Il lavoro si concentra sulla formalizzazione di strumenti di teoria dell'informazione, con particolare enfasi sulle divergenze e le loro applicazioni all'hypothesis testing. Il contributo principale è la formalizzazione di una versione generale della disuguaglianza di data processing (DPI) per le f-divergenze, un risultato fondamentale in teoria dell'informazione. Vengono confrontate tre diverse dimostrazioni della DPI, ciascuna con diversi gradi di generalità e ipotesi; la terza dimostrazione è la più generale e mette in evidenza la connessione tra la DPI e il problema di hypothesis testing. Oltre ai contributi teorici, la tesi riflette sulle scelte d'implementazione, sulle sfide affrontate e sulle intuizioni emerse durante il processo di formalizzazione. Questo lavoro sottolinea l'utilità degli interactive theorem prover nell'affrontare problemi matematici complessi, offrendo nuove prospettive nei campi della probabilità e della teoria dell'informazione.