Commit 2026-06-01 19:58 3d6f7ccc

View on Github →

feat: more basic lemmas on norms and sums (#40100)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

added theorem Summable.of_enorm

added theorem tsum_enorm_ne_top_iff_summable_nnnorm

added theorem tsum_enorm_ne_top_iff_summable_norm

Modified Mathlib/Analysis/Normed/Operator/Basic.lean

added theorem ContinuousLinearMap.opENorm_le_bound

Modified Mathlib/Analysis/Normed/Operator/Mul.lean

added theorem ContinuousLinearMap.opNNNorm_lsmul

added theorem ContinuousLinearMap.opNNNorm_lsmul_apply

added theorem ContinuousLinearMap.opNNNorm_lsmul_apply_le

added theorem ContinuousLinearMap.opNNNorm_lsmul_le

added theorem ContinuousLinearMap.opNorm_lsmul_apply

modified theorem ContinuousLinearMap.opNorm_lsmul_le