Commit 2025-01-23 07:42 a6e1dfdd

View on Github →

feat: more lemmas for enorm (#20966) These follow the existing norm and nnnorm. The large import comes from the fact that we need to import Topology.Instances.ENNReal to state continuous_enorm : Continuous (‖·‖ₑ).

Estimated changes

added theorem NNReal.enorm_eq
modified theorem NNReal.nnnorm_eq
modified theorem NormOneClass.nontrivial
added theorem enorm_inv
added theorem enorm_mul
added theorem enorm_one
added theorem enorm_pow
modified theorem nnnorm_mul
deleted theorem nnnorm_norm
modified theorem nnnorm_one
deleted theorem norm_norm
added theorem Continuous.enorm'
added theorem ContinuousAt.enorm'
added theorem ContinuousOn.enorm'
added theorem Filter.Tendsto.enorm'
added theorem Real.enorm_abs
added theorem Real.enorm_natCast
added theorem Real.enorm_of_nonneg
modified theorem Real.nnnorm_abs
added theorem coe_le_enorm
added theorem coe_lt_enorm
added theorem continuous_enorm'
added theorem enorm_div_le
modified theorem enorm_eq_nnnorm
added theorem enorm_eq_zero'
added theorem enorm_inv'
added theorem enorm_le_coe
added theorem enorm_lt_coe
added theorem enorm_lt_top
added theorem enorm_mul_le'
added theorem enorm_ne_top
added theorem enorm_ne_zero'
added theorem enorm_norm'
added theorem enorm_one'
added theorem enorm_pos'
added theorem nnnorm_norm'
added theorem norm_norm'
added theorem ofReal_norm'
added theorem toReal_enorm'
added theorem Pi.enorm_single
added theorem enorm_smul
added theorem enorm_smul_le
added theorem Int.enorm_natCast