Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-31 01:35 f4d72050

View on Github →

chore(measure_theory/*): rename probability_measure and finite_measure (#8831) Renamed to is_probability_measure and is_finite_measure, respectively. Also, locally_finite_measure becomes is_locally_finite_measure. See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238337.20Weak.20convergence

Estimated changes

modified theorem convex.integral_mem
modified theorem convex_on.map_integral_le
modified theorem real.measure_ext_Ioo_rat
modified theorem measure_theory.Lp.antimono
deleted theorem is_compact.finite_measure
modified theorem measure_theory.prob_le_one