Vi formaliserar några grundläggande egenskaper hos Fourier-serien i logiken hos ACL2(r), som är en variant av ACL2 som stöder resonemang om verkliga och komplexa tal genom icke-standardanalys. Mer specifikt utökar vi en ram för att formellt utvärdera bestämda integraler av realvärderade, kontinuerliga funktioner med hjälp av den andra grundläggande teorin av analys. Vårt utökade ramverk tillämpas också på funktioner som innehåller fria argument. Med hjälp av detta ramverk kan vi bevisa de ortogonala sambanden mellan trigonometriska funktioner, som är de väsentliga egenskaperna i Fourier serieanalys. Summan regel för bestämda integraler av indexerade belopp formaliseras också genom att tillämpa den utvidgade ramen tillsammans med den första grundläggande teorem av analys och summan regel för differentiering. De Fourier koefficientformlerna för periodiska funktioner formaliseras sedan från ortogonalitetsförhållandena och totalregeln för integration. Följaktligen är det unika i Fourier summor en enkel följd. Vi presenterar också vår formalisering av totalregeln för bestämda integraler av oändliga serier i ACL2(r). En del av denna uppgift är att bevisa Dini Uniform Convergency Theorem och kontinuiteten i en gränsfunktion under vissa förhållanden. En nyckelteknik i våra bevis på dessa teorem är att tillämpa överspillprincipen från icke-standardanalys.
På liknande sätt, Chau et al. REF formaliserade Fourier-koefficientformlerna och deras egenskaper i ACL2(r).
Fourier Series Formalization in ACL2(r)
{'venue': 'EPTCS 192, 2015, pp. 35-51', 'journal': None, 'mag_field_of_study': ['Computer Science']}