Commit 2021-09-14 06:36 ef78b322

View on Github →

feat(measure_theory/function/lp_space): add lemmas about snorm and mem_Lp (#9146) Also move lemma snorm_add_le (and related others) out of the borel space section, since opens_measurable_space is a sufficient hypothesis.

Estimated changes

Modified src/measure_theory/function/ess_sup.lean

added theorem ess_sup_smul_measure

Modified src/measure_theory/function/lp_space.lean

added theorem measure_theory.mem_ℒp.congr_norm

added theorem measure_theory.mem_ℒp.mono'

added theorem measure_theory.mem_ℒp_congr_norm

added theorem measure_theory.mem_ℒp_const_iff

added theorem measure_theory.mem_ℒp_finset_sum

added theorem measure_theory.mem_ℒp_neg_iff

added theorem measure_theory.mem_ℒp_norm_iff

added theorem measure_theory.snorm'_smul_measure

added theorem measure_theory.snorm_const_lt_top_iff

added theorem measure_theory.snorm_ess_sup_smul_measure

added theorem measure_theory.snorm_mono

added theorem measure_theory.snorm_mono_ae_real

added theorem measure_theory.snorm_mono_real

added theorem measure_theory.snorm_one_smul_measure

added theorem measure_theory.snorm_smul_measure_of_ne_top

added theorem measure_theory.snorm_smul_measure_of_ne_zero

added theorem measure_theory.snorm_sub_le

added theorem measure_theory.snorm_zero'

added theorem measure_theory.zero_mem_ℒp'