Convex sets are null-measurable #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.add_haar_frontier), hence
s is a measure_theory.null_measurable_set (see convex.null_measurable_set).
theorem
convex.add_haar_frontier
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
{s : set E}
(hs : convex ℝ s) :
Haar measure of the frontier of a convex set is zero.
@[protected]
theorem
convex.null_measurable_set
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
{s : set E}
(hs : convex ℝ s) :
A convex set in a finite dimensional real vector space is null measurable with respect to an additive Haar measure on this space.