Normalized two-moment slices have graph diameter at most two
ProvedHirsch.normalized_two_moment_slice_diameter_twoformalizationgraph-diameterpolyhedra
For arbitrary real moments t_i and target mu, consider the normalized nonnegative slice of the simplex defined by sum_i s_i = 1 and sum_i t_i s_i = mu. Its vertex-edge graph has padded diameter at most two. No distinctness or genericity assumption is made on the moments, so repeated moments, empty slices, singleton slices, and lower-dimensional cases are included.
Preamble
import Mathlib import Definitions.Def_Hirsch_model open scoped BigOperators RealInnerProductSpace open Set Hirsch
Formal statement
namespace Hirsch
theorem normalized_two_moment_slice_diameter_two {n : ℕ}
(t : Fin n → ℝ) (mu : ℝ) :
DiamLE
{s : EuclideanSpace ℝ (Fin n) |
(∀ i, 0 ≤ s i) ∧
(∑ i, s i) = 1 ∧
(∑ i, t i * s i) = mu} 2 := by sorry
end HirschSource