Commit 2025-03-07 09:37 47faa130

View on Github →

feat: add classes ContinuousENorm and ENormed(Add)(Comm)Monoid (#21670) and prove that these contain (commutative) (Add)NormedGroups. This allows generalising results from normed spaces/normed groups to ENNReal also. A future PR will generalise lemmas in mathlib to use these new classes. This PR only changes a few lemmas, to prove that these definitions are set up right. From the Carleson project.

Estimated changes

added theorem Continuous.enorm
added theorem ContinuousAt.enorm
added theorem ContinuousOn.enorm
added theorem continuous_enorm
modified theorem enorm_eq_zero'
modified theorem enorm_mul_le'
modified theorem enorm_ne_zero'
modified theorem enorm_pos'
deleted theorem Continuous.enorm'
deleted theorem ContinuousAt.enorm'
deleted theorem ContinuousOn.enorm'
deleted theorem ContinuousWithinAt.enorm'
deleted theorem continuous_enorm'