Fourier series formalization in ACL2(r)

DOI10.4204/EPTCS.192.4MaRDI QIDQ6591104zbMATH OpenFDO

Authors Cuong K. Chau, Matt Kaufmann, Warren A. jun. Hunt

Publication date 21 August 2024

Full work available at URL https://doi.org/10.4204/EPTCS.192.4

Mathematics Subject Classification ID

Nonstandard analysis (26E35) Fourier coefficients, Fourier series of functions with special properties, special Fourier series (42A16) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A formalization of properties of continuous functions on closed intervals
• scientific article; zbMATH DE number 2003153
• The formalization of discrete Fourier transform in HOL
• On the formalization of Fourier transform in higher-order logic
• A Coq formalization of Lebesgue integration of nonnegative functions

This page was built for publication: Fourier series formalization in ACL2(r)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6591104)