Commit 2026-06-01 07:16 bde7627e
View on Github →chore: fix deprecations for PMF.bernoulli (#40031)
Some statements about PMF.bernoulli were not deprecated while PMF.bernoulli was deprecated, see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Deprecation.20policy/near/598588742.
The two lemmas about the support of PMF.bernoulli are deprecated in favor of ProbabilityTheory.bernoulliMeasure_apply_of_notMem_of_notMem.
PMF.binomial_one_eq_bernoulli should wait for #37736 which deprecates PMF.binomial.