Concavity of truncated-volume roots

def Grunbaum.trunc {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : Set (Euc d)

The part of C cut out by the sublevel halfspace of ℓ at t.

Equations

• Grunbaum.trunc C ℓ t = C ∩ ⇑ℓ ⁻¹' Set.Iic t

noncomputable def Grunbaum.truncRoot {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : ℝ

The dimension-normalized root of a truncation's volume.

Equations

• Grunbaum.truncRoot C ℓ t = (MeasureTheory.volume (Grunbaum.trunc C ℓ t) ^ (↑d + 1)⁻¹).toReal

noncomputable def Grunbaum.cdfRoot {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : ℝ

The dimension-normalized root of the truncation's volume ratio.

Equations

• Grunbaum.cdfRoot C ℓ t = ((MeasureTheory.volume (Grunbaum.trunc C ℓ t) / MeasureTheory.volume C) ^ (↑d + 1)⁻¹).toReal

def Grunbaum.truncDomain {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) : Set ℝ

Thresholds for which the corresponding truncation is nonempty.

Equations

• Grunbaum.truncDomain C ℓ = {t : ℝ | (Grunbaum.trunc C ℓ t).Nonempty}

theorem Grunbaum.isCompact_trunc {d : ℕ} {C : Set (Euc d)} (hC : IsCompact C) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : IsCompact (trunc C ℓ t)

theorem Grunbaum.volume_trunc_ne_top {d : ℕ} {C : Set (Euc d)} (hC : IsCompact C) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : MeasureTheory.volume (trunc C ℓ t) ≠ ⊤

theorem Grunbaum.truncRoot_combo {d : ℕ} {C : Set (Euc d)} (hCconv : Convex ℝ C) (hCcomp : IsCompact C) (ℓ : Euc d →L[ℝ] ℝ) {s t a b : ℝ} (hs : (trunc C ℓ s).Nonempty) (ht : (trunc C ℓ t).Nonempty) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a * truncRoot C ℓ s + b * truncRoot C ℓ t ≤ truncRoot C ℓ (a * s + b * t)

theorem Grunbaum.convex_truncDomain {d : ℕ} {C : Set (Euc d)} (hCconv : Convex ℝ C) (ℓ : Euc d →L[ℝ] ℝ) : Convex ℝ (truncDomain C ℓ)

theorem Grunbaum.concaveOn_truncRoot {d : ℕ} {C : Set (Euc d)} (hCconv : Convex ℝ C) (hCcomp : IsCompact C) (ℓ : Euc d →L[ℝ] ℝ) : ConcaveOn ℝ (truncDomain C ℓ) (truncRoot C ℓ)

theorem Grunbaum.cdfRoot_eq {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : cdfRoot C ℓ t = (MeasureTheory.volume C ^ (↑d + 1)⁻¹).toReal⁻¹ * truncRoot C ℓ t

theorem Grunbaum.concaveOn_cdfRoot {d : ℕ} {C : Set (Euc d)} (hCconv : Convex ℝ C) (hCcomp : IsCompact C) (ℓ : Euc d →L[ℝ] ℝ) : ConcaveOn ℝ (truncDomain C ℓ) (cdfRoot C ℓ)