Commit 2026-06-30 09:15 b53180c4

View on Github →

feat: more API around enorms of operators (#41155)

Estimated changes

Modified Mathlib/Analysis/Analytic/Constructions.lean

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

added theorem tendsto_iff_enorm_div_tendsto_zero

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

deleted theorem ContinuousLinearMap.le_opNorm_enorm

deleted theorem ContinuousLinearMap.opENorm_le_bound

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

added theorem ContinuousLinearMap.le_opENorm₂

added theorem ContinuousLinearMap.opENorm_flip

added theorem ContinuousLinearMap.opENorm_le_bound₂

added theorem ContinuousLinearMap.opNNNorm_flip

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

added theorem ContinuousLinearMap.opENorm_lsmul

added theorem ContinuousLinearMap.opENorm_lsmul_apply

added theorem ContinuousLinearMap.opENorm_lsmul_le

added theorem ContinuousLinearMap.opENorm_mul

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

added theorem ContinuousLinearMap.le_of_opENorm_le

added theorem ContinuousLinearMap.le_of_opENorm_le_of_le

added theorem ContinuousLinearMap.le_opENorm_of_le

added theorem ContinuousLinearMap.opENorm_le_bound

added theorem ContinuousLinearMap.opENorm_le_iff

Modified Mathlib/Geometry/Manifold/Riemannian/Basic.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Variation/Semivariation.lean

Modified Mathlib/Probability/Moments/CovarianceBilinDual.lean