Commit 2026-03-10 20:55 e821a3fc

View on Github →

feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n (#30240) Add a wrapper for fderiv as a continuous linear map from D_K^n to D_K^(n-1). Co-Authored by: @ADedecker

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

added theorem ContDiffMapSupportedIn.fderivCLM_apply

added theorem ContDiffMapSupportedIn.fderivCLM_apply_of_gt

added theorem ContDiffMapSupportedIn.fderivCLM_apply_of_le

added theorem ContDiffMapSupportedIn.fderivCLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.fderivLM_apply

added theorem ContDiffMapSupportedIn.fderivLM_apply_of_gt

added theorem ContDiffMapSupportedIn.fderivLM_apply_of_le

added theorem ContDiffMapSupportedIn.fderivLM_eq_of_scalars

modified theorem ContDiffMapSupportedIn.iteratedFDerivLM_apply_of_gt

added theorem ContDiffMapSupportedIn.seminorm_fderivLM_le

added theorem ContDiffMapSupportedIn.seminorm_fderivLM_top