Commit 2021-06-15 14:54 2f1f34a9

View on Github →

feat(measure_theory/lp_space): add mem_Lp.mono_measure (#7927) also add monotonicity lemmas wrt the measure for snorm', snorm_ess_sup and snorm.

Estimated changes

Modified src/measure_theory/lp_space.lean

added theorem measure_theory.mem_ℒp.mono_measure

added theorem measure_theory.mem_ℒp.restrict

added theorem measure_theory.snorm'_mono_measure

added theorem measure_theory.snorm_ess_sup_mono_measure

added theorem measure_theory.snorm_mono_measure