Sammanfattning Statistiska mängder, såsom förväntan (medel) och varians, spelar en viktig roll i den nuvarande tidsåldern probabilistisk analys. I denna uppsats presenterar vi en formalisering av förväntanteorin som kan användas för att verifiera förväntningarna och variansegenskaperna hos diskreta slumpmässiga variabler inom HOL-teorin. Motiveringen bakom detta är förmågan att utföra felfri probabilistisk analys, som i sin tur kan vara mycket användbar för prestanda- och tillförlitlighetsanalys av system som används inom säkerhetskritiska områden, såsom rymdresor, medicin och militär. Vi presenterar först en formell definition av förväntan på en funktion av en diskret slumpmässig variabel. Utifrån denna definition formaliserar vi det matematiska begreppet varians och verifierar några klassiska egenskaper hos förväntan och varians i HOL. Vi använder sedan dessa formella definitioner för att verifiera förväntningarna och variansegenskaperna hos den geometriska slumpvariabeln. För att visa den praktiska effektiviteten i den formalisering som presenteras i detta dokument presenterar vi också den probabilistiska analysen av Coupon Collectors problem i HOL.
På samma sätt använde vi våra teorier relaterade till den formella verifieringen av statistiska egenskaper för prestandaanalys av Coupon Collector problem REF.
Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Mathematics', 'Computer Science']}