Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-09 15:06 5faf34cc

View on Github →

feat(measure_theory/lp_space): add more lemmas about snorm (#5644)

Estimated changes

Modified src/measure_theory/lp_space.lean

modified theorem ℒp_space.ae_eq_zero_of_snorm_eq_zero

added theorem ℒp_space.mem_ℒp.ae_eq

added theorem ℒp_space.mem_ℒp.sub

added theorem ℒp_space.mem_ℒp_congr_ae

added theorem ℒp_space.mem_ℒp_const

added theorem ℒp_space.mem_ℒp_const_of_ne_zero

added theorem ℒp_space.mem_ℒp_const_of_nonneg

added theorem ℒp_space.snorm_congr_ae

added theorem ℒp_space.snorm_const'

added theorem ℒp_space.snorm_const

added theorem ℒp_space.snorm_const_of_probability_measure

added theorem ℒp_space.snorm_const_smul

modified theorem ℒp_space.snorm_eq_zero_iff

modified theorem ℒp_space.snorm_eq_zero_of_ae_zero'

modified theorem ℒp_space.snorm_eq_zero_of_ae_zero

added theorem ℒp_space.snorm_exponent_zero

added theorem ℒp_space.snorm_zero'

deleted theorem ℒp_space.zero_mem_ℒp

added theorem ℒp_space.zero_mem_ℒp_of_nonneg

added theorem ℒp_space.zero_mem_ℒp_of_pos