Documentation

Mathlib.Analysis.Convex.StdSimplex

The standard simplex #

In this file, given an ordered semiring π•œ and a finite type ΞΉ, we define stdSimplex : Set (ΞΉ β†’ π•œ) as the set of vectors with non-negative coordinates with total sum 1.

When f : X β†’ Y is a map between finite types, we define the map stdSimplex.map f : stdSimplex π•œ X β†’ stdSimplex π•œ Y.

source
@[deprecated Convexity.StdSimplex (since := "2026-08-29")]
def stdSimplex (π•œ : Type u_2) (ΞΉ : Type u_1) [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] :
Set (ΞΉ β†’ π•œ)

The standard simplex in the space of functions ΞΉ β†’ π•œ is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

Equations
Instances For
    source
    @[deprecated Convexity.StdSimplex.range_toFun_comp_weights (since := "2026-08-29")]
    theorem stdSimplex_eq_inter (π•œ : Type u_2) (ΞΉ : Type u_1) [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] :
    stdSimplex π•œ ΞΉ = (β‹‚ (x : ΞΉ), {f : ΞΉ β†’ π•œ | 0 ≀ f x}) ∩ {f : ΞΉ β†’ π•œ | βˆ‘ x : ΞΉ, f x = 1}
    source
    @[deprecated Convexity.StdSimplex.instConvexSpace (since := "2026-08-29")]
    theorem convex_stdSimplex (π•œ : Type u_2) (ΞΉ : Type u_1) [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [IsOrderedRing π•œ] :
    Convex π•œ (stdSimplex π•œ ΞΉ)
    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem stdSimplex_of_subsingleton (π•œ : Type u_2) (ΞΉ : Type u_1) [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [Subsingleton π•œ] :
    stdSimplex π•œ ΞΉ = Set.univ
    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem stdSimplex_of_isEmpty_index (π•œ : Type u_2) (ΞΉ : Type u_1) [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [IsEmpty ΞΉ] [Nontrivial π•œ] :
    stdSimplex π•œ ΞΉ = βˆ…

    The standard simplex in the zero-dimensional space is empty.

    source
    @[deprecated Convexity.StdSimplex.instUnique (since := "2026-08-29")]
    theorem stdSimplex_unique (π•œ : Type u_2) (ΞΉ : Type u_1) [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [ZeroLEOneClass π•œ] [Nonempty ΞΉ] [Subsingleton ΞΉ] :
    stdSimplex π•œ ΞΉ = {fun (x : ΞΉ) => 1}
    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem mem_Icc_of_mem_stdSimplex {π•œ : Type u_2} {ΞΉ : Type u_1} [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [IsOrderedAddMonoid π•œ] {f : ΞΉ β†’ π•œ} (hf : f ∈ stdSimplex π•œ ΞΉ) (x : ΞΉ) :
    f x ∈ Set.Icc 0 1

    All values of a function f ∈ stdSimplex π•œ ΞΉ belong to [0, 1].

    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem stdSimplex_subset_Icc (π•œ : Type u_2) {ΞΉ : Type u_1} [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [IsOrderedAddMonoid π•œ] :
    stdSimplex π•œ ΞΉ βŠ† Set.Icc 0 1

    stdSimplex π•œ ΞΉ is a subset of the unit cube

    source
    @[deprecated Convexity.StdSimplex.single (since := "2026-08-29")]
    theorem single_mem_stdSimplex (π•œ : Type u_2) {ΞΉ : Type u_1} [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [DecidableEq ΞΉ] [ZeroLEOneClass π•œ] (i : ΞΉ) :
    Pi.single i 1 ∈ stdSimplex π•œ ΞΉ
    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem ite_eq_mem_stdSimplex (π•œ : Type u_2) {ΞΉ : Type u_1} [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [DecidableEq ΞΉ] [ZeroLEOneClass π•œ] (i : ΞΉ) :
    (fun (x : ΞΉ) => if i = x then 1 else 0) ∈ stdSimplex π•œ ΞΉ
    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem segment_single_subset_stdSimplex (π•œ : Type u_2) {ΞΉ : Type u_1} [Semiring π•œ] [PartialOrder π•œ] [Fintype ΞΉ] [DecidableEq ΞΉ] [ZeroLEOneClass π•œ] [IsOrderedRing π•œ] (i j : ΞΉ) :
    segment π•œ (Pi.single i 1) (Pi.single j 1) βŠ† stdSimplex π•œ ΞΉ

    The edges are contained in the simplex.

    source
    @[deprecated "no replacement" (since := "2026-08-29")]
    theorem stdSimplex_fin_two (π•œ : Type u_2) [Semiring π•œ] [PartialOrder π•œ] [ZeroLEOneClass π•œ] [IsOrderedRing π•œ] :
    stdSimplex π•œ (Fin 2) = segment π•œ (Pi.single 0 1) (Pi.single 1 1)
    source
    @[deprecated Convexity.StdSimplex.equivIcc (since := "2026-08-29")]
    def stdSimplexEquivIcc (π•œ : Type u_1) [Ring π•œ] [PartialOrder π•œ] [IsOrderedRing π•œ] :
    ↑(stdSimplex π•œ (Fin 2)) ≃ ↑(Set.Icc 0 1)

    The standard one-dimensional simplex in Fin 2 β†’ π•œ is equivalent to the unit interval. This bijection sends the zeroth vertex Pi.single 0 1 to 0 and the first vertex Pi.single 1 1 to 1.

    Equations
    Instances For
      source
      @[simp]
      theorem stdSimplexEquivIcc_symm_apply_coe (π•œ : Type u_1) [Ring π•œ] [PartialOrder π•œ] [IsOrderedRing π•œ] (x : ↑(Set.Icc 0 1)) :
      ↑((stdSimplexEquivIcc π•œ).symm x) = ![1 - ↑x, ↑x]
      source
      @[simp]
      theorem stdSimplexEquivIcc_apply_coe (π•œ : Type u_1) [Ring π•œ] [PartialOrder π•œ] [IsOrderedRing π•œ] (f : ↑(stdSimplex π•œ (Fin 2))) :
      ↑((stdSimplexEquivIcc π•œ) f) = ↑f 1
      source
      @[simp, deprecated Convexity.StdSimplex.equivIcc_single_zero (since := "2026-08-29")]
      theorem stdSimplexEquivIcc_zero (π•œ : Type u_1) [Ring π•œ] [PartialOrder π•œ] [IsOrderedRing π•œ] :
      (stdSimplexEquivIcc π•œ) ⟨Pi.single 0 1, β‹―βŸ© = 0
      source
      @[simp, deprecated Convexity.StdSimplex.equivIcc_single_one (since := "2026-08-29")]
      theorem stdSimplexEquivIcc_one (π•œ : Type u_1) [Ring π•œ] [PartialOrder π•œ] [IsOrderedRing π•œ] :
      (stdSimplexEquivIcc π•œ) ⟨Pi.single 1 1, β‹―βŸ© = 1
      source
      @[deprecated "no replacement" (since := "2026-08-29")]
      theorem convexHull_basis_eq_stdSimplex (R : Type u_1) (ΞΉ : Type u_2) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype ΞΉ] [DecidableEq ΞΉ] :
      (convexHull R) (Set.range fun (i j : ΞΉ) => if i = j then 1 else 0) = stdSimplex R ΞΉ

      stdSimplex π•œ ΞΉ is the convex hull of the canonical basis in ΞΉ β†’ π•œ.

      source
      @[deprecated "no replacement" (since := "2026-08-29")]
      theorem convexHull_rangle_single_eq_stdSimplex (R : Type u_1) (ΞΉ : Type u_2) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype ΞΉ] [DecidableEq ΞΉ] :
      (convexHull R) (Set.range fun (i : ΞΉ) => Pi.single i 1) = stdSimplex R ΞΉ

      stdSimplex π•œ ΞΉ is the convex hull of the points Pi.single i 1 for i : ΞΉ.

      source
      theorem Convexity.ConvexSpace.AffineMap.convex_range {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {X : Type u_3} [ConvexSpace R X] {E : Type u_4} [AddCommGroup E] [Module R E] [ConvexSpace R E] [IsModuleConvexSpace R E] (f : ConvexSpace.AffineMap R X E) :
      Convex R (Set.range ⇑f)
      source
      theorem Set.convexHull_eq_range_iConvexComb {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (s : Set E) :
      (convexHull R) s = range ⇑(Convexity.StdSimplex.affineMapMk fun (x : ↑s) => ↑x)

      The convex hull of a set s is the range of the affine map StdSimplex R s β†’ E which sends x : s to x : E.

      source
      @[deprecated Set.convexHull_eq_range_iConvexComb (since := "2026-08-29")]
      theorem Set.Finite.convexHull_eq_image {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (s : Set E) :
      (convexHull R) s = range ⇑(Convexity.StdSimplex.affineMapMk fun (x : ↑s) => ↑x)

      Alias of Set.convexHull_eq_range_iConvexComb.

      The convex hull of a set s is the range of the affine map StdSimplex R s β†’ E which sends x : s to x : E.

      source
      @[deprecated Convexity.StdSimplex.isClosedEmbedding_toFun_comp_weights (since := "2026-08-29")]
      theorem isClosed_stdSimplex (π•œ : Type u_1) (ΞΉ : Type u_2) [Fintype ΞΉ] [TopologicalSpace π•œ] [Semiring π•œ] [PartialOrder π•œ] [OrderClosedTopology π•œ] [ContinuousAdd π•œ] :
      IsClosed (stdSimplex π•œ ΞΉ)

      stdSimplex π•œ ΞΉ is closed.

      source
      @[deprecated Convexity.StdSimplex.compactSpace (since := "2026-08-29")]
      theorem isCompact_stdSimplex (π•œ : Type u_1) (ΞΉ : Type u_2) [Fintype ΞΉ] [TopologicalSpace π•œ] [Semiring π•œ] [PartialOrder π•œ] [OrderClosedTopology π•œ] [ContinuousAdd π•œ] [CompactIccSpace π•œ] [IsOrderedAddMonoid π•œ] :
      IsCompact (stdSimplex π•œ ΞΉ)

      stdSimplex π•œ ΞΉ is compact.

      source
      @[deprecated Convexity.StdSimplex.compactSpace (since := "2026-08-29")]
      instance stdSimplex.instCompactSpace_coe (π•œ : Type u_1) (ΞΉ : Type u_2) [Fintype ΞΉ] [TopologicalSpace π•œ] [Semiring π•œ] [PartialOrder π•œ] [OrderClosedTopology π•œ] [ContinuousAdd π•œ] [CompactIccSpace π•œ] [IsOrderedAddMonoid π•œ] :
      CompactSpace ↑(stdSimplex π•œ ΞΉ)
      source
      @[deprecated Convexity.StdSimplex.range_toFun_comp_weights_subset_closedBall (since := "2026-08-29")]
      theorem stdSimplex_subset_closedBall {ΞΉ : Type u_1} [Fintype ΞΉ] :
      stdSimplex ℝ ΞΉ βŠ† Metric.closedBall 0 1

      Every vector in stdSimplex π•œ ΞΉ has max-norm at most 1.

      source
      @[deprecated Convexity.StdSimplex.isBounded_range_toFun_comp_weights (since := "2026-08-29")]
      theorem bounded_stdSimplex (ΞΉ : Type u_1) [Fintype ΞΉ] :
      Bornology.IsBounded (stdSimplex ℝ ΞΉ)

      stdSimplex ℝ ΞΉ is bounded.

      source
      @[deprecated Convexity.StdSimplex.pathConnectedSpace (since := "2026-08-29")]
      theorem isPathConnected_stdSimplex (ΞΉ : Type u_1) [Fintype ΞΉ] [Nonempty ΞΉ] :
      IsPathConnected (stdSimplex ℝ ΞΉ)

      stdSimplex ℝ ΞΉ is path connected.

      source
      @[deprecated Convexity.StdSimplex.pathConnectedSpace (since := "2026-08-29")]
      instance instPathConnectedSpaceElemForallRealStdSimplexOfNonempty (ΞΉ : Type u_1) [Fintype ΞΉ] [Nonempty ΞΉ] :
      PathConnectedSpace ↑(stdSimplex ℝ ΞΉ)
      source
      @[deprecated Convexity.StdSimplex.homeomorphI (since := "2026-08-29")]
      def stdSimplexHomeomorphUnitInterval :
      ↑(stdSimplex ℝ (Fin 2)) β‰ƒβ‚œ ↑unitInterval

      The standard one-dimensional simplex in ℝ² = Fin 2 β†’ ℝ is homeomorphic to the unit interval.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem stdSimplexHomeomorphUnitInterval_apply_coe (f : ↑(stdSimplex ℝ (Fin 2))) :
        ↑(stdSimplexHomeomorphUnitInterval f) = ↑f 1
        source
        @[simp]
        theorem stdSimplexHomeomorphUnitInterval_symm_apply_coe (x : ↑(Set.Icc 0 1)) :
        ↑(stdSimplexHomeomorphUnitInterval.symm x) = ![1 - ↑x, ↑x]
        source
        @[simp, deprecated Convexity.StdSimplex.homeomorphI_single_zero (since := "2026-08-29")]
        theorem stdSimplexHomeomorphUnitInterval_zero :
        stdSimplexHomeomorphUnitInterval ⟨Pi.single 0 1, β‹―βŸ© = 0
        source
        @[simp, deprecated Convexity.StdSimplex.homeomorphI_single_one (since := "2026-08-29")]
        theorem stdSimplexHomeomorphUnitInterval_one :
        stdSimplexHomeomorphUnitInterval ⟨Pi.single 1 1, β‹―βŸ© = 1

        Diameter of a Standard Simplex (sup metric) #

        source
        @[deprecated Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall (since := "2026-08-29")]
        theorem diam_stdSimplex_le {ΞΉ : Type u_1} [Fintype ΞΉ] :
        Metric.diam (stdSimplex ℝ ΞΉ) ≀ 1

        The (sup metric) diameter of a standard simplex is less than or equal to 1.

        source
        @[simp, deprecated Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_zero (since := "2026-08-29")]
        theorem diam_stdSimplex_of_subsingleton {ΞΉ : Type u_1} [Fintype ΞΉ] [Subsingleton ΞΉ] :
        Metric.diam (stdSimplex ℝ ΞΉ) = 0

        The (sup metric) diameter of a standard simplex indexed by a subsingleton is 0.

        source
        @[simp, deprecated Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_one (since := "2026-08-29")]
        theorem diam_stdSimplex {ΞΉ : Type u_1} [Fintype ΞΉ] [Nontrivial ΞΉ] :
        Metric.diam (stdSimplex ℝ ΞΉ) = 1

        The (sup metric) diameter of a standard simplex indexed by a nontrivial index is 1.

        source
        @[instance_reducible, macro_inline, deprecated "no replacement" (since := "2026-08-29")]
        instance stdSimplex.instFunLikeElemForall {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] :
        FunLike (↑(stdSimplex S X)) X S
        Equations
        source
        @[deprecated Convexity.StdSimplex.ext (since := "2026-08-29")]
        theorem stdSimplex.ext {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(stdSimplex S X)} (h : ⇑s = ⇑t) :
        s = t
        source
        theorem stdSimplex.ext_iff {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(stdSimplex S X)} :
        s = t ↔ ⇑s = ⇑t
        source
        @[simp, deprecated Convexity.StdSimplex.weights_nonneg (since := "2026-08-29")]
        theorem stdSimplex.zero_le {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(stdSimplex S X)) (x : X) :
        0 ≀ s x
        source
        @[simp, deprecated Convexity.StdSimplex.total (since := "2026-08-29")]
        theorem stdSimplex.sum_eq_one {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(stdSimplex S X)) :
        βˆ‘ x : X, s x = 1
        source
        @[simp, deprecated Convexity.StdSimplex.total_fin_two (since := "2026-08-29")]
        theorem stdSimplex.add_eq_one {S : Type u_1} [Semiring S] [PartialOrder S] (s : ↑(stdSimplex S (Fin 2))) :
        s 0 + s 1 = 1
        source
        @[simp, deprecated Convexity.StdSimplex.weights_apply_le_one (since := "2026-08-29")]
        theorem stdSimplex.le_one {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] (s : ↑(stdSimplex S X)) (x : X) :
        s x ≀ 1
        source
        @[deprecated Convexity.StdSimplex.map (since := "2026-08-29")]
        theorem stdSimplex.image_linearMap {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X β†’ Y) :
        ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X βŠ† stdSimplex S Y
        source
        @[deprecated Convexity.StdSimplex.map (since := "2026-08-29")]
        noncomputable def stdSimplex.map {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X β†’ Y) (s : ↑(stdSimplex S X)) :
        ↑(stdSimplex S Y)

        The map stdSimplex S X β†’ stdSimplex S Y that is induced by a map f : X β†’ Y.

        Equations
        Instances For
          source
          @[simp, deprecated "no replacement" (since := "2026-08-29")]
          theorem stdSimplex.map_coe {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X β†’ Y) (s : ↑(stdSimplex S X)) :
          ⇑(map f s) = (FunOnFinite.linearMap S S f) ⇑s
          source
          @[simp, deprecated Convexity.StdSimplex.map_id (since := "2026-08-29")]
          theorem stdSimplex.map_id_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] (x : ↑(stdSimplex S X)) :
          map id x = x
          source
          @[deprecated Convexity.StdSimplex.map_comp (since := "2026-08-29")]
          theorem stdSimplex.map_comp_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype X] [Fintype Y] [Fintype Z] [IsOrderedRing S] (f : X β†’ Y) (g : Y β†’ Z) (x : ↑(stdSimplex S X)) :
          map g (map f x) = map (g ∘ f) x
          source
          @[reducible, inline, deprecated Convexity.StdSimplex.single (since := "2026-08-29")]
          abbrev stdSimplex.vertex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) :
          ↑(stdSimplex S X)

          The vertex corresponding to x : X in stdSimplex S X.

          Equations
          Instances For
            source
            @[simp, deprecated "no replacement" (since := "2026-08-29")]
            theorem stdSimplex.vertex_coe {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) :
            ⇑(vertex x) = Pi.single x 1
            source
            @[simp, deprecated Convexity.StdSimplex.map_single (since := "2026-08-29")]
            theorem stdSimplex.map_vertex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [DecidableEq X] [DecidableEq Y] (f : X β†’ Y) (x : X) :
            map f (vertex x) = vertex (f x)
            source
            @[deprecated Convexity.StdSimplex.continuous_map (since := "2026-08-29")]
            theorem stdSimplex.continuous_map {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [TopologicalSpace S] [IsTopologicalSemiring S] (f : X β†’ Y) :
            Continuous (map f)
            source
            @[deprecated Convexity.StdSimplex.single_injective (since := "2026-08-29")]
            theorem stdSimplex.vertex_injective {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [Nontrivial S] [DecidableEq X] :
            Function.Injective vertex
            source
            @[deprecated Convexity.StdSimplex.instNonempty (since := "2026-08-29")]
            instance stdSimplex.instNonemptyElemForall {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [Nonempty X] :
            Nonempty ↑(stdSimplex S X)
            source
            @[deprecated Convexity.StdSimplex.instNontrivial (since := "2026-08-29")]
            instance stdSimplex.instNontrivialElemForall {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [Nontrivial S] [Nontrivial X] :
            Nontrivial ↑(stdSimplex S X)
            source
            @[deprecated Convexity.StdSimplex.instSubsingleton (since := "2026-08-29")]
            instance stdSimplex.instSubsingletonElemForall {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [Subsingleton X] :
            Subsingleton ↑(stdSimplex S X)
            source
            @[instance_reducible, deprecated Convexity.StdSimplex.instUnique (since := "2026-08-29")]
            instance stdSimplex.instUniqueElemForall {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [Unique X] :
            Unique ↑(stdSimplex S X)
            Equations
            source
            @[simp, deprecated Convexity.StdSimplex.weights_apply_eq_one (since := "2026-08-29")]
            theorem stdSimplex.eq_one_of_unique {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [Unique X] (s : ↑(stdSimplex S X)) (x : X) :
            s x = 1

            Barycenter of a Standard Simplex #

            source
            @[deprecated Convexity.StdSimplex.barycenter (since := "2026-08-29")]
            def stdSimplex.barycenter {X : Type u_2} [Fintype X] {π•œ : Type u_5} [Field π•œ] [LinearOrder π•œ] [IsStrictOrderedRing π•œ] [Nonempty X] :
            ↑(stdSimplex π•œ X)

            The barycenter of a standard simplex is the center of mass of the set of vertices (equally weighted).

            Equations
            Instances For
              source
              @[simp, deprecated Convexity.StdSimplex.weights_barycenter_apply (since := "2026-08-29")]
              theorem stdSimplex.barycenter_apply {X : Type u_2} [Fintype X] {π•œ : Type u_5} [Field π•œ] [LinearOrder π•œ] [IsStrictOrderedRing π•œ] [Nonempty X] (x : X) :
              ↑barycenter x = (↑(Fintype.card X))⁻¹

              The barycenter of a standard simplex has coordinates (Fintype.card X)⁻¹ at each index.

              source
              @[deprecated "no replacement" (since := "2026-08-29")]
              theorem stdSimplex.barycenter_eq_centerMass {X : Type u_2} [Fintype X] {π•œ : Type u_5} [Field π•œ] [LinearOrder π•œ] [IsStrictOrderedRing π•œ] [Nonempty X] [DecidableEq X] :
              ↑barycenter = Finset.univ.centerMass (fun (x : X) => 1) fun (i : X) => Pi.single i 1

              The barycenter equals the (equal weight) center of mass of vertices (Finset.centerMass).