Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.mul_meas_ge_le_integral_of_nonneg

Modification history

2022-07-12 08:44
src/measure_theory/integral/bochner.lean
feat(probability/moments): Chernoff bound on the upper/lower tail of a real random variable (#15129) …
Added measure_theory.mul_meas_ge_le_integral_of_nonnegView on Github →