Commit 2025-11-27 16:17 633ee94e

View on Github →

feat(Analysis/Distribution/ContDiffMapSupportedIn): add withSeminorms statement (#30236) Add withSeminorms instance to ContDiffMapSupportedIn, where the seminorm familiy is given by the sup-norm on the i-th derivative. Co-authored by: @ADedecker

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

added theorem ContDiffMapSupportedIn.norm_apply_le_seminorm

added theorem ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm

added theorem ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder

added theorem ContDiffMapSupportedIn.norm_toBoundedContinuousFunction

added theorem ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply

added theorem ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_apply