Commit 2025-11-14 11:51 97e3e0d8

View on Github →

feat: add differentiation for ContDiffMapSupportedIn (#30201) Add a wrapper for iteratedFDeriv on ContDiffMapSupportedIn and related API.

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

added theorem ContDiffMapSupportedIn.coe_toBoundedContinuousFunction

added theorem ContDiffMapSupportedIn.iteratedFDerivLM_apply

added theorem ContDiffMapSupportedIn.iteratedFDerivLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.iteratedFDerivLM_eq_withOrder

added theorem ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply

added theorem ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_gt

added theorem ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_le

added theorem ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.structureMapLM_apply

added theorem ContDiffMapSupportedIn.structureMapLM_apply_withOrder

added theorem ContDiffMapSupportedIn.structureMapLM_eq

added theorem ContDiffMapSupportedIn.structureMapLM_eq_of_scalars

added theorem ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_eq_of_scalars

deleted theorem ContDiffMapSupportedIn.toBoundedContinuousFunction_apply

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

added theorem BoundedContinuousFunction.coe_mk