The height quantile of a convex set

Let s be a set of positive finite volume in a finite-dimensional Euclidean space and e a unit vector. The height ⟪e, x⟫ of a point x drawn uniformly from s has the law (volume[|s]).map fun x ↦ ⟪e, x⟫. Its cumulative distribution function at c is the proportion of the volume of s lying below the hyperplane ⟪e, x⟫ = c, and it is continuous because hyperplanes are null.

For a convex set the cumulative distribution function takes a value strictly between 0 and 1 exactly at the heights of interior points of s, and it is strictly increasing there. Hence the quantile function of the height law is a strictly increasing continuous parametrization of the open interval ⟪e, interior s⟫ by the levels in Ioo 0 1. If s is moreover bounded and Borel, the derivative of the volume below a hyperplane is the volume of the hyperplane section, which is positive at the height of an interior point. The inverse function theorem then shows that at every level τ ∈ Ioo 0 1 the quantile z has derivative volume s / volume {y ∈ (ℝ ∙ e)ᗮ | y + z τ • e ∈ s}. For an arbitrary bounded set s of positive volume, measurable or not, inverse transform sampling shows that the average of the quantile over the levels is the mean height, that is, the height of the centroid of s; here volume[|s] is the conditional measure of volume on s, which is supported on a measurable hull of s.

This volume-fraction parametrization of heights is the change of variables in the Kneser–Süss proof of the equality case of the Brunn–Minkowski inequality for convex bodies: two bodies of equal volume are compared along each direction at heights cutting off equal volume fractions.

Main results

• TauCeti.nullSingletonClass_map_inner_cond: the height law has no atoms.
• TauCeti.cdf_map_inner_cond: the cumulative distribution function of the height law.
• TauCeti.continuous_cdf_map_inner_cond: it is continuous.
• Convex.cdf_map_inner_cond_mem_Ioo_iff: for a convex set it lies strictly between 0 and 1 exactly at the heights of interior points.
• Convex.strictMonoOn_cdf_map_inner_cond: it is strictly increasing there.
• Convex.image_quantile_map_inner_cond_Ioo: the quantile maps Ioo 0 1 onto the heights of interior points.
• Convex.quantile_map_inner_cond_mem_image_interior: each interior level goes to the height of an interior point.
• Convex.volume_real_hyperplaneSection_quantile_pos, Convex.continuousOn_volume_real_hyperplaneSection_quantile: the hyperplane section at the quantile has positive volume, depending continuously on the level.
• Convex.hasDerivAt_quantile_map_inner_cond: the derivative of the quantile.
• TauCeti.setIntegral_quantile_map_inner_cond: the quantile averages to the height of the centroid.

References

• H. Kneser and W. Süss, Die Volumina in linearen Scharen konvexer Körper, Mat. Tidsskr. B (1932), 19–25, for the volume-fraction comparison of convex bodies.
• R. Schneider, Convex Bodies: The Brunn–Minkowski Theory, 2nd ed., Cambridge University Press, 2014, Section 7.1, for an exposition of the Kneser–Süss argument.

theorem TauCeti.nullSingletonClass_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (he : ‖e‖ = 1) (s : Set E) : MeasureTheory.NullSingletonClass (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s])

The law of the height along a unit vector of a point drawn uniformly from any set has no atoms, since hyperplanes are null.

theorem TauCeti.cdf_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs0 : MeasureTheory.volume s ≠ 0) (hsi : MeasureTheory.volume s ≠ ⊤) (c : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s])) c = MeasureTheory.volume.real {x : E | x ∈ s ∧ inner ℝ e x ≤ c} / MeasureTheory.volume.real s

The cumulative distribution function of the height along e of a point drawn uniformly from s is the proportion of the volume of s below the hyperplane at height c.

theorem TauCeti.continuous_cdf_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (he : ‖e‖ = 1) (hs0 : MeasureTheory.volume s ≠ 0) (hsi : MeasureTheory.volume s ≠ ⊤) : Continuous ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]))

The cumulative distribution function of the height law of a set of positive finite volume is continuous, since hyperplanes are null.

theorem Convex.cdf_map_inner_cond_mem_Ioo_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (he : ‖e‖ = 1) (hs0 : MeasureTheory.volume s ≠ 0) (hsi : MeasureTheory.volume s ≠ ⊤) {c : ℝ} : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s])) c ∈ Set.Ioo 0 1 ↔ c ∈ (fun (x : E) => inner ℝ e x) '' interior s

For a convex set of positive finite volume, the cumulative distribution function of the height law lies strictly between 0 and 1 exactly at the heights of interior points.

theorem Convex.strictMonoOn_cdf_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (he : ‖e‖ = 1) (hs0 : MeasureTheory.volume s ≠ 0) (hsi : MeasureTheory.volume s ≠ ⊤) : StrictMonoOn (↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]))) (↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s])) ⁻¹' Set.Ioo 0 1)

For a convex set of positive finite volume, the cumulative distribution function of the height law is strictly increasing where it lies strictly between 0 and 1.

theorem Convex.image_quantile_map_inner_cond_Ioo {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (he : ‖e‖ = 1) (hs0 : MeasureTheory.volume s ≠ 0) (hsi : MeasureTheory.volume s ≠ ⊤) : (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile '' Set.Ioo 0 1 = (fun (x : E) => inner ℝ e x) '' interior s

For a convex set of positive finite volume, the quantile function of the height law maps the levels in Ioo 0 1 onto the heights of interior points.

theorem Convex.quantile_map_inner_cond_mem_image_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (he : ‖e‖ = 1) (hs0 : MeasureTheory.volume s ≠ 0) (hsi : MeasureTheory.volume s ≠ ⊤) {τ : ℝ} (hτ : τ ∈ Set.Ioo 0 1) : (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile τ ∈ (fun (x : E) => inner ℝ e x) '' interior s

For a convex set of positive finite volume, the quantile function of the height law takes every level in Ioo 0 1 to the height of an interior point.

theorem Convex.volume_real_hyperplaneSection_quantile_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (hsb : Bornology.IsBounded s) (hs0 : MeasureTheory.volume s ≠ 0) (he : ‖e‖ = 1) {τ : ℝ} (hτ : τ ∈ Set.Ioo 0 1) : 0 < MeasureTheory.volume.real {y : ↥(ℝ ∙ e)ᗮ | ↑y + (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile τ • e ∈ s}

The hyperplane section of a bounded convex set of positive volume at its height quantile has positive finite volume at every level in Ioo 0 1.

theorem Convex.continuousOn_volume_real_hyperplaneSection_quantile {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (hsb : Bornology.IsBounded s) (hs0 : MeasureTheory.volume s ≠ 0) (he : ‖e‖ = 1) : ContinuousOn (fun (τ : ℝ) => MeasureTheory.volume.real {y : ↥(ℝ ∙ e)ᗮ | ↑y + (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile τ • e ∈ s}) (Set.Ioo 0 1)

The volume of the hyperplane section of a bounded convex set of positive volume at its height quantile is continuous on the levels in Ioo 0 1.

theorem Convex.hasDerivAt_quantile_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {e : E} {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (hs : Convex ℝ s) (hsb : Bornology.IsBounded s) (hsm : MeasurableSet s) (hs0 : MeasureTheory.volume s ≠ 0) (he : ‖e‖ = 1) {τ : ℝ} (hτ : τ ∈ Set.Ioo 0 1) : HasDerivAt (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile (MeasureTheory.volume.real s / MeasureTheory.volume.real {y : ↥(ℝ ∙ e)ᗮ | ↑y + (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile τ • e ∈ s}) τ

Derivative of the height quantile. For a bounded Borel convex set s of positive volume and a unit vector e, the quantile function z of the height law along e is differentiable at every level τ ∈ Ioo 0 1, with derivative the volume of s divided by the volume of the hyperplane section of s at height z τ.

theorem TauCeti.integrableOn_quantile_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (hsb : Bornology.IsBounded s) (hs0 : MeasureTheory.volume s ≠ 0) : MeasureTheory.IntegrableOn (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile (Set.Ioo 0 1) MeasureTheory.volume

The quantile function of the height law of an arbitrary bounded set of positive volume (measurable or not) is integrable on the levels Ioo 0 1.

theorem TauCeti.setIntegral_quantile_map_inner_cond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (hsb : Bornology.IsBounded s) (hs0 : MeasureTheory.volume s ≠ 0) : ∫ (τ : ℝ) in Set.Ioo 0 1, (MeasureTheory.Measure.map (fun (x : E) => inner ℝ e x) MeasureTheory.volume[|s]).quantile τ = inner ℝ e (∫ (x : E), x ∂MeasureTheory.volume[|s])

The mean height. The average over the levels Ioo 0 1 of the quantile function of the height ⟪e, x⟫ of a point x drawn from the conditional measure volume[|s] of an arbitrary bounded set s of positive volume (measurable or not) is the height of the centroid ∫ x, x ∂(volume[|s]).