Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.BoundaryGeometry

← Mathematical handbook

Compactness and shape of the sharp boundary #

source
theorem Papers.AnsariRockelSteinmassl2026RhoGamma.region_compact :
IsCompact region
source
theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_endpoints :
upperRho (-1) = -1 ∧ upperRho 1 = 1
source
theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_concave :
ConcaveOn ℝ (Set.Icc (-1) 1) upperRho
source
theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_strictMono :
StrictMonoOn upperRho (Set.Icc (-1) 1)

Strict increase follows from mixing a boundary optimizer with M.

source
theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_continuous :
ContinuousOn upperRho (Set.Icc (-1) 1)

Continuity includes both limiting endpoints, using compactness and endpoint rigidity.