Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersCslib.Probability.PMF.posterior_hasSum
Plain-language statement
Posterior probabilities joint(a, b) / marginal(b) sum to 1 when b is in the support of the marginal.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Probability.PMF.posteriorDist_eq_prior_of_outputIndist
Plain-language statement
If the output distribution of a channel does not depend on the input, then conditioning on any output with positive probability leaves the prior unchanged.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Probability.PMF.uniformOfFintype_map_equiv
Plain-language statement
A uniform distribution on a finite type is invariant under any equivalence.
Source project: Lean Computer Science Library
Person-level attribution pending.
PMF.integrable_of_support_finite
Plain-language statement
Everything is integrable over PMFs with finite support
Source project: debate
Person-level attribution pending.
Prob.bind_toPmf
Plain-language statement
Prob.toPmf commutes with bind
Source project: debate
Person-level attribution pending.