BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Heather Macbeth (Fordham University)
DTSTART:20220324T160000Z
DTEND:20220324T170000Z
DTSTAMP:20260415T010738Z
UID:LondonLearningLean/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/7/">Fourier series</a>\nby Heather Macbeth (Fordham University) as 
 part of London Learning Lean\n\n\nAbstract\nFourier series are not new to 
 formalization\; various results were proved by Harrison in HOL Light ten y
 ears ago\, and there are developments in Isabelle and Metamath too.  But t
 he Hilbert space theory and measure theory in Lean's library mathlib allow
 s for a very efficient presentation.  I will give a tour of some of this t
 heory\, touching on topological groups\, the Stone-Weierstrass theorem\, t
 he denseness of continuous functions in Lp\, and a TFAE for Hilbert bases.
 \n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/7/
END:VEVENT
END:VCALENDAR