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 of 0 ≤ f.

Estimated changes