Convex.nullMeasurableSet
theorem Convex.nullMeasurableSet :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {s : Set E}, Convex ℝ s → MeasureTheory.NullMeasurableSet s μ
The theorem states that for any convex set in a finite dimensional real vector space, it is null measurable with respect to an additive Haar measure on that space. In other words, the set can be approximated by a measurable set up to a set of null measure as measured by an additive Haar measure. Here, a set being convex means that any line segment connecting two points in the set lies entirely within the set. A vector space is said to be finite dimensional if it has a finite number of dimensions, i.e., it is spanned by a finite basis. An additive Haar measure is a measure that is invariant under translations in the given vector space.
More concisely: Every convex subset of a finite-dimensional real vector space is null measurable with respect to an additive Haar measure.
|
Convex.addHaar_frontier
theorem Convex.addHaar_frontier :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {s : Set E}, Convex ℝ s → ↑↑μ (frontier s) = 0
The theorem titled "Convex.addHaar_frontier" states that for any convex set `s` in a finite-dimensional real vector space `E` that is equipped with norms, measurable space structure, Borel space structure, and a measure `μ` which satisfies the property of being an additive Haar measure, the Haar measure of the frontier of the set `s` is zero. The frontier of a set is defined as the set of points that are in the closure of the set `s` but not in its interior. In simpler terms, it asserts that the "boundary" of a convex set in such a space has zero additive Haar measure.
More concisely: The Haar measure of the frontier of any convex set in a finite-dimensional real vector space equipped with norms, measurable space structure, Borel space structure, and an additive Haar measure is zero.
|