Skip to content

jvlmdr/forml

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

98 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

ForML

This project aims to prove useful theorems for machine learning in Lean.

Definitions

  • Smooth, compact bump functions (with topology)

Theorems

  • Schwartz functions
    • Schwartz functions are in Lp
    • Integral of a Schwartz function as a ContinuousLinearMap
    • Integral against HasTemperateGrowth function is a tempered distribution
    • HasTemperateGrowth for trigonometric functions
    • Application of a CLM commutes with (iterated) Fréchet derivative
    • Iterated partial derivative is equal to iterated Fréchet derivative
  • Gaussian tends to Dirac delta
  • Second mean value theorem for (improper) integrals
  • Hölder's inequality for functions in L1 and L∞

Todo

  • Fourier transform of Schwartz function
  • Fourier transform of tempered distribution
  • Schwartz function: Integral up to a point as a CLM

Roadmap (depth first)

  • Sum of two independent r.v.s is convolution of pdfs (where pdf is a distribution)
    • Define Fourier transform for distributions
      • Define distribution as continuous linear map on test functions
    • Fourier transform of convolution of distributions
      • Fourier transform of Dirac delta, constant, sin/cos, derivative, integral, ...

Other todos

  • Generate docs (and add links to readme)
  • Add CI

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages