Commit 2023-09-25 05:21 6f7f5f38

View on Github →

feat(OperatorNorm,Multilinear): add lemmas, golf (#7302)

Analysis/NormedSpace/OperatorNorm

  • Add ContinuousLinearMap.isLeast_op_norm, ContinuousLinearMap.op_nnnorm_le_iff, and ContinuousLinearMap.isLeast_op_nnnorm.
  • Golf some proofs.
  • Drop RingHomIsometric assumption here and there.

Analysis/NormedSpace/Multilinear

  • Add ContinuousMultilinearMap.isLeast_op_norm, ContinuousMultilinearMap.isLeast_op_nnnorm, ContinuousMultilinearMap.le_mul_prod_of_le_op_norm_of_le, ContinuousMultilinearMap.op_norm_le_iff, ContinuousMultilinearMap.op_nnnorm_le_iff, ContinuousMultilinearMap.op_nnnorm_prod, ContinuousMultilinearMap.op_nnnorm_pi.
  • Golf/move some proofs.
  • Change implicit/explicit arguments in some lemmas.

Estimated changes