Commit 2023-10-12 07:34 780c5bab
View on Github →feat(Integral/Bochner): golf Markov's inequality, drop an assumption (#7619)
- Golf the proof of
MeasureTheory.mul_meas_ge_le_integral_of_nonneg
. - Drop the assumption
[IsFiniteMeasure μ]
. - Assume
0 ≤ᵐ[μ] f
instead of0 ≤ f
.