Commit 2026-03-31 15:26 69cbc416

View on Github →

feat(Analysis/Distribution): define Dirac delta distribution (#36491) Defines Dirac delta distribution (classical) Closes #36464

  • Note: Used continuous_eval_const in defining Delta in Distribution.lean, rather than the way it's done in TemperedDistribution.lean (which could also work)
  • Defined for all $x \in E$, with delta_eq_zero_of_notMem which proves it's zero if $x \not\in \Omega$

Estimated changes