Commit 2025-11-25 10:20 aa61c4e7

View on Github →

feat(Calculus): derivative of ContinuousAlternatingMap.compContinuousLinearMap (#30331)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/TVS.lean

added theorem LinearMap.isBigOTVS_rev_comp

Created Mathlib/Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean

added theorem ContinuousAlternatingMap.differentiable

added theorem ContinuousAlternatingMap.hasFDerivAt

added theorem ContinuousAlternatingMap.hasFDerivWithinAt

added theorem ContinuousAlternatingMap.hasStrictFDerivAt

added theorem ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap

added theorem ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff

added theorem Differentiable.continuousAlternatingMap_apply

added theorem DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap

added theorem DifferentiableAt.continuousAlternatingMap_apply

added theorem DifferentiableOn.continuousAlternatingMap_apply

added theorem DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap

added theorem DifferentiableWithinAt.continuousAlternatingMap_apply

added theorem HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap

added theorem HasFDerivAt.continuousAlternatingMap_apply

added theorem HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap

added theorem HasFDerivWithinAt.continuousAlternatingMap_apply

added theorem HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap

added theorem HasStrictFDerivAt.continuousAlternatingMap_apply

added theorem fderivWithin_continuousAlternatingMapCompContinuousLinearMap

added theorem fderivWithin_continuousAlternatingMap_apply

added theorem fderiv_continuousAlternatingMapCompContinuousLinearMap

added theorem fderiv_continuousAlternatingMap_apply

Modified Mathlib/Analysis/Convex/EGauge.lean

added theorem le_egauge_of_forall_ne_zero

Modified Mathlib/Analysis/Normed/Module/Alternating/Basic.lean

modified def ContinuousAlternatingMap.compContinuousLinearMapCLM

added def ContinuousAlternatingMap.fderivCompContinuousLinearMap

added theorem ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply

modified theorem ContinuousAlternatingMap.norm_compContinuousLinearMap_le

added theorem ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap

Modified Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

modified def ContinuousAlternatingMap.apply

modified theorem ContinuousAlternatingMap.apply_apply

modified theorem ContinuousAlternatingMap.hasSum_eval

added def ContinuousAlternatingMap.liftCLM

added theorem ContinuousAlternatingMap.liftCLM_apply

modified theorem ContinuousAlternatingMap.tsum_eval