Moment determination for measures supported on the standard simplex

theorem ProbabilityTheory.integrable_of_continuous_of_restrict_stdSimplex {α : Type u_1} [Fintype α] {μ : MeasureTheory.Measure (α → ℝ)} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ.restrict (Convexity.StdSimplex.coordinateSet ℝ α) = μ) {g : (α → ℝ) → ℝ} (hg : Continuous g) : MeasureTheory.Integrable g μ

A continuous real function is integrable against a finite measure supported on the simplex.

theorem ProbabilityTheory.eq_of_forall_monomial_integral_eq_of_restrict_stdSimplex {α : Type u_1} [Fintype α] {μ ν : MeasureTheory.Measure (α → ℝ)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : μ.restrict (Convexity.StdSimplex.coordinateSet ℝ α) = μ) (hν : ν.restrict (Convexity.StdSimplex.coordinateSet ℝ α) = ν) (h : ∀ (m : α → ℕ), ∫ (x : α → ℝ), ∏ i : α, x i ^ m i ∂μ = ∫ (x : α → ℝ), ∏ i : α, x i ^ m i ∂ν) : μ = ν

Finite Borel measures supported on the standard simplex are determined by their monomial moments.