The finite simplex of nonnegative real weights

The finite simplex Convexity.StdSimplex ℝ≥0 ι carries the topology induced by its weight vector. This makes continuity of probability vectors equivalent to continuity of their weights, including at zero weights. The weights also sum to one after casting them to ℝ.

This is the finite-coordinate construction of Mathlib's Convexity.StdSimplex.topologicalSpaceInduced. That construction requires a coefficient ring and therefore does not apply to ℝ≥0.

theorem Convexity.StdSimplex.sum_coe_weights {X : Type u_1} [Fintype X] (p : StdSimplex NNReal X) : ∑ i : X, ↑(p.weights i) = 1

The weights of a point of a standard simplex over ℝ≥0, cast to ℝ, sum to 1.

theorem Convexity.StdSimplex.sum_mul_coe_weights {X : Type u_1} [Fintype X] (p : StdSimplex NNReal X) (c : ℝ) : ∑ i : X, c * ↑(p.weights i) = c

Scaling the real weights of a point of a standard simplex over ℝ≥0 by c gives weights summing to c.

@[instance_reducible]

noncomputable instance Convexity.StdSimplex.instTopologicalSpaceNNReal (ι : Type u_3) [Finite ι] : TopologicalSpace (StdSimplex NNReal ι)

The coordinate topology on the finite simplex of nonnegative real weights.

theorem Convexity.StdSimplex.isEmbedding_toFun_comp_weights_nnreal {ι : Type u_2} [Finite ι] : Topology.IsEmbedding fun (p : StdSimplex NNReal ι) => ⇑p.weights

The finite nonnegative-real simplex embeds into its space of weight vectors.

theorem Convexity.StdSimplex.continuous_iff_toFun_comp_weights_nnreal {ι : Type u_2} [Finite ι] {X : Type u_3} [TopologicalSpace X] {f : X → StdSimplex NNReal ι} : Continuous f ↔ Continuous fun (x : X) => ⇑(f x).weights

Continuity into the finite nonnegative-real simplex is continuity of the weight vector.

theorem Convexity.StdSimplex.continuous_weights_apply_nnreal {ι : Type u_2} [Finite ι] (i : ι) : Continuous fun (p : StdSimplex NNReal ι) => p.weights i

Every weight is continuous on the finite nonnegative-real simplex.