Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-19 21:59 b1214293

View on Github →

feat(measure_theory/lp_space): extend the definition of Lp seminorm to p ennreal (#5808) Rename the seminorm with real exponent to snorm', introduce snorm_ess_sup for L\infty, equal to the essential supremum of the norm.

Estimated changes

modified theorem ennreal.ae_le_ess_sup
modified theorem ennreal.ess_sup_add_le
modified theorem ennreal.ess_sup_const_mul
deleted theorem ess_sup_eq_zero_iff
modified theorem ℒp_space.mem_ℒp.add
modified theorem ℒp_space.mem_ℒp.ae_eq
modified theorem ℒp_space.mem_ℒp.neg
modified theorem ℒp_space.mem_ℒp.sub
modified def ℒp_space.mem_ℒp
modified theorem ℒp_space.mem_ℒp_const
added theorem ℒp_space.snorm'_neg
added theorem ℒp_space.snorm'_zero
modified def ℒp_space.snorm
modified theorem ℒp_space.snorm_add_le
modified theorem ℒp_space.snorm_congr_ae
modified theorem ℒp_space.snorm_const'
modified theorem ℒp_space.snorm_const
modified theorem ℒp_space.snorm_const_smul
modified theorem ℒp_space.snorm_neg
deleted theorem ℒp_space.snorm_zero'
modified theorem ℒp_space.snorm_zero