Commit 2025-04-10 08:39 f87b8235

View on Github →

feat: definition and properties of characteristic functions (#19783) define characteristic functions. Show that characteristic functions separate finite measures.

Estimated changes

added theorem Circle.exp_pi_ne_one
added theorem Circle.star_addChar
added def Real.fourierChar
added theorem Real.fourierChar_apply
added def Real.probChar
added theorem Real.probChar_apply'
added theorem Real.probChar_apply
added theorem Real.probChar_ne_one
deleted def Real.fourierChar
deleted theorem Real.fourierChar_apply