Standard simplex barycentric coordinates

This module defines standard simplex coordinates as nonnegative weights summing to one, with their induced topology and relative interior.

def NRR.StandardSimplex (d : ℕ) : Type

Barycentric coordinates of the standard d-simplex.

Equations

• NRR.StandardSimplex d = { w : Fin (d + 1) → ℝ // (∀ (i : Fin (d + 1)), 0 ≤ w i) ∧ ∑ i : Fin (d + 1), w i = 1 }

@[instance_reducible]

instance NRR.StandardSimplex.instTopologicalSpace (d : ℕ) : TopologicalSpace (StandardSimplex d)

Equations

• NRR.StandardSimplex.instTopologicalSpace d = TopologicalSpace.induced Subtype.val inferInstance

@[instance_reducible]

instance NRR.StandardSimplex.instCoeFunForallFinHAddNatOfNatReal (d : ℕ) : CoeFun (StandardSimplex d) fun (x : StandardSimplex d) => Fin (d + 1) → ℝ

Equations

• NRR.StandardSimplex.instCoeFunForallFinHAddNatOfNatReal d = { coe := fun (w : NRR.StandardSimplex d) => ↑w }

@[simp]

theorem NRR.StandardSimplex.nonneg {d : ℕ} (w : StandardSimplex d) (i : Fin (d + 1)) : 0 ≤ ↑w i

@[simp]

theorem NRR.StandardSimplex.sum_eq_one {d : ℕ} (w : StandardSimplex d) : ∑ i : Fin (d + 1), ↑w i = 1

def NRR.StandardSimplex.IsInterior {d : ℕ} (w : StandardSimplex d) : Prop

The relative interior of the standard simplex.

Equations

• w.IsInterior = ∀ (i : Fin (d + 1)), 0 < ↑w i