Commit 2026-03-18 18:00 e7f2949f

View on Github →

feat: monotonicity of D^n(U) in n and in U as CLMs (#32401)

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

added theorem ContDiffMapSupportedIn.monoCLM_apply

added theorem ContDiffMapSupportedIn.monoCLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.monoCLM_eq_zero

added theorem ContDiffMapSupportedIn.monoLM_apply

added theorem ContDiffMapSupportedIn.monoLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.monoLM_eq_zero

added theorem ContDiffMapSupportedIn.seminorm_monoLM_eq

added theorem ContDiffMapSupportedIn.seminorm_monoLM_le

Modified Mathlib/Analysis/Distribution/TestFunction.lean

added theorem TestFunction.monoCLM_apply

added theorem TestFunction.monoCLM_eq_of_scalars

added theorem TestFunction.monoCLM_eq_zero