The positive-coordinate interior of the standard simplex

The definition and measurability result are independent of Dirichlet parameters. The historical ProbabilityTheory declaration names are retained for compatibility.

def ProbabilityTheory.stdSimplexInterior {ι : Type u_1} [Fintype ι] : Set (ι → ℝ)

The interior of Convexity.StdSimplex.coordinateSet ℝ ι relative to its affine hull.

Equations

• ProbabilityTheory.stdSimplexInterior = {u : ι → ℝ | u ∈ Convexity.StdSimplex.coordinateSet ℝ ι ∧ ∀ (i : ι), 0 < u i}

theorem ProbabilityTheory.measurableSet_stdSimplexInterior {ι : Type u_1} [Fintype ι] : MeasurableSet stdSimplexInterior

The stdSimplexInterior is a measurable set.

theorem ProbabilityTheory.mem_stdSimplexInterior_perm {ι : Type u_1} [Fintype ι] (σ : Equiv.Perm ι) (u : ι → ℝ) : u ∘ ⇑σ ∈ stdSimplexInterior ↔ u ∈ stdSimplexInterior

Permuting coordinates preserves the positive-coordinate simplex interior.

theorem ProbabilityTheory.ae_mem_stdSimplexInterior {ι : Type u_1} [Fintype ι] : ∀ᵐ (u : ι → ℝ) ∂MeasureTheory.Measure.stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι), u ∈ stdSimplexInterior

Almost every point of the simplex is in its positive-coordinate interior. For an empty index type the simplex measure is zero.

def Convexity.StdSimplex.positiveInterior {ι : Type u_1} : Set (StdSimplex ℝ ι)

The positive-coordinate interior as a set of intrinsic simplex points.

Equations

• Convexity.StdSimplex.positiveInterior = {s : Convexity.StdSimplex ℝ ι | ∀ (i : ι), 0 < s.weights i}

theorem Convexity.StdSimplex.isOpen_positiveInterior {ι : Type u_1} [Finite ι] : IsOpen positiveInterior

theorem Convexity.StdSimplex.image_coordinates_positiveInterior {ι : Type u_1} [Fintype ι] : coordinates '' positiveInterior = ProbabilityTheory.stdSimplexInterior

The intrinsic interior has exactly the existing ambient positive-coordinate image.

theorem Convexity.StdSimplex.ae_mem_positiveInterior {ι : Type u_1} [Fintype ι] : ∀ᵐ (s : StdSimplex ℝ ι) ∂coordinateMeasure, s ∈ positiveInterior

Almost every intrinsic point has strictly positive coordinates.