The barycenter of the standard simplex

noncomputable def Convexity.StdSimplex.subBarycenter {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] (S : Finset M) (hS : S.Nonempty) : StdSimplex K M

In the standard simplex with vertices M, this is the barycenter of a nonempty finite subset S of M.

Equations

• Convexity.StdSimplex.subBarycenter S hS = { weights := ∑ m ∈ S, Finsupp.single m (↑S.card)⁻¹, nonneg := ⋯, total := ⋯ }

theorem Convexity.StdSimplex.weights_subBarycenter {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] (S : Finset M) (hS : S.Nonempty) : (subBarycenter S hS).weights = ∑ m ∈ S, Finsupp.single m (↑S.card)⁻¹

theorem Convexity.StdSimplex.subBarycenter_weights_apply_eq_zero {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] (S : Finset M) (hS : S.Nonempty) (m : M) (hm : m ∉ S) : (subBarycenter S hS).weights m = 0

@[simp]

theorem Convexity.StdSimplex.subBarycenter_singleton {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] (m : M) : subBarycenter {m} ⋯ = single m

@[reducible, inline]

noncomputable abbrev Convexity.StdSimplex.barycenter {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] [Nonempty M] [Fintype M] : StdSimplex K M

The barycenter of the standard simplex.

Equations

• Convexity.StdSimplex.barycenter = Convexity.StdSimplex.subBarycenter Finset.univ ⋯

theorem Convexity.StdSimplex.weights_barycenter_apply {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] [Nonempty M] [Fintype M] (m : M) : barycenter.weights m = (↑(Fintype.card M))⁻¹

theorem Convexity.StdSimplex.barycenter_of_unique {K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] [Unique M] : barycenter = single default

@[simp]

theorem Convexity.StdSimplex.barycenter_fin_one {K : Type u_1} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] : barycenter = single 0