Commit 2025-09-23 11:51 62b471f5

feat(ProbabilityTheory): Add moment_def and moment_one (#29902) Add moment_def to make it easier to go from μ[X ^ p] to moment X p μ. Also added moment_one as a special case. This is useful for stating a lemma for the mean and variance of a random variable as a corollary of the moments if all of the moments can be proved at once (but one could use moment_def instead if this lemma is deemed unnecessary).