Convex sets are null-measurable

Let E be a finite dimensional real vector space, let μ be a Haar measure on E, let s be a convex set in E. Then the frontier of s has measure zero (see Convex.addHaar_frontier), hence s is a NullMeasurableSet (see Convex.nullMeasurableSet).

theorem Convex.addHaar_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (hs : Convex ℝ s) : ↑↑μ (frontier s) = 0

Haar measure of the frontier of a convex set is zero.

theorem Convex.nullMeasurableSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (hs : Convex ℝ s) : MeasureTheory.NullMeasurableSet s μ

A convex set in a finite dimensional real vector space is null measurable with respect to an additive Haar measure on this space.