Commit 2024-04-05 06:15 44c063e1

View on Github →

feat: deriv versions of composition lemmas with bilinear maps (#11868) We already have the fderiv versions.

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Mul.lean

added theorem ContinuousLinearMap.derivWithin_of_bilinear

added theorem ContinuousLinearMap.deriv_of_bilinear

added theorem ContinuousLinearMap.hasDerivAt_of_bilinear

added theorem ContinuousLinearMap.hasDerivWithinAt_of_bilinear

added theorem ContinuousLinearMap.hasStrictDerivAt_of_bilinear

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

added theorem ContinuousLinearMap.hasStrictFDerivAt_of_bilinear

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem innerSL_real_flip

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

added theorem ContinuousLinearMap.precompL_apply