Commit 2023-05-25 03:53 745fa52a

View on Github →

chore: golf proofs about IsBoundedBilinearMap (#4239) Add IsBoundedBilinearMap.toContinuousLinearMap and use it to golf proofs by reusing facts about bundled bilinear maps E →L[𝕜] F →L[𝕜] G.

All changes

  • Add IsBoundedBilinearMap.toContinuousLinearMap.
  • Rename IsBoundedBilinearMap.is_O' to IsBoundedBilinearMap.isBigO'.
  • Rename isBoundedBilinearMap_deriv_coe to IsBoundedBilinearMap.deriv_apply.
  • Add LinearMap.mkContinuousOfExistsBound₂, a bilinear map version of LinearMap.mkContinuousOfExistsBound and use it to redefine LinearMap.mkContinuous₂. The new definition is definitionally equal to the old one.
  • Import Mathlib.Analysis.NormedSpace.OperatorNorm instead of Mathlib.Analysis.NormedSpace.BoundedLinearMaps in Mathlib.Analysis.Calculus.FDeriv.Basic.
  • Golf many proofs

Estimated changes