Commit 2026-03-18 15:04 3611c4ea

View on Github →

feat: differentiation of test function as a CLM (#31809)

Estimated changes

Modified Mathlib/Analysis/Distribution/TestFunction.lean

added theorem TestFunction.fderivCLM_apply

added theorem TestFunction.fderivCLM_apply_of_gt

added theorem TestFunction.fderivCLM_apply_of_le

added theorem TestFunction.fderivCLM_eq_of_scalars

added theorem TestFunction.fderivCLM_ofSupportedIn