Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-22 16:26 83bd2e68

View on Github →

feat(analysis/normed_space/multilinear): add a few inequalities (#8018) Also add a few lemmas about tsum and nnnorm.

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem nnnorm_tsum_le

added theorem tsum_of_nnnorm_bounded

Modified src/analysis/normed_space/multilinear.lean

added theorem continuous_multilinear_map.le_of_op_nnnorm_le

added theorem continuous_multilinear_map.le_op_nnnorm

added theorem continuous_multilinear_map.le_op_norm_mul_pow_card_of_le

added theorem continuous_multilinear_map.le_op_norm_mul_pow_of_le

added theorem continuous_multilinear_map.le_op_norm_mul_prod_of_le

added theorem continuous_multilinear_map.tsum_eval