Commit 2023-05-25 08:25 036470e8

View on Github →

feat: port Analysis.Calculus.Fderiv.Bilinear (#4221) Also golf/extend theorems about bounded bilinear maps and rewrite the proof using the fact that the derivative of a bilinear map is a continuous bilinear map.

Estimated changes

Modified Mathlib.lean

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

added theorem ContinuousLinearMap.fderivWithin_of_bilinear

added theorem ContinuousLinearMap.fderiv_of_bilinear

added theorem ContinuousLinearMap.hasFDerivAt_of_bilinear

added theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear

added theorem IsBoundedBilinearMap.differentiable

added theorem IsBoundedBilinearMap.differentiableAt

added theorem IsBoundedBilinearMap.differentiableOn

added theorem IsBoundedBilinearMap.differentiableWithinAt

added theorem IsBoundedBilinearMap.fderiv

added theorem IsBoundedBilinearMap.fderivWithin

added theorem IsBoundedBilinearMap.hasFDerivAt

added theorem IsBoundedBilinearMap.hasFDerivWithinAt

added theorem IsBoundedBilinearMap.hasStrictFDerivAt