The feasible set of nonnegative weights with fixed linear moments
DefinitionHlawkaSchatten_DiagonalConstruction_SparsificationmomentFiber is the set of nonnegative weight vectors, indexed by an arbitrary finite type , satisfying three prescribed linear moment constraints: given a moment assignment and a target ,
This is the feasible set for the three-coordinate reduction step of the sharp diagonal construction. A theorem in the same source module shows that, when has nonnegative entries with every row sum positive (so the fiber is compact) and is continuous and concave on the nonnegative orthant , every is matched by some with and at most three nonzero coordinates. In the intended use, records the moments contributed by coordinate toward three fixed pair power sums of a coordinate triple, and holds their target values while the weights are varied; the definition itself is stated for an arbitrary moment matrix and target , with no reference to power sums.
import Mathlib.Analysis.Convex.Function
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.LinearAlgebra.Dimension.Finite
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Mathlib.Topology.Order.Compact
/-
Copyright (c) 2026 Ezzeri Esa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ezzeri Esa
-/
/-!
# Three constraints admit a sparse concave minimizer
For nonnegative coordinate weights, fixing three positive linear moments
gives a compact feasible set. Minimize the concave objective, then maximize
the sum of squared weights among its minimizers. A supported kernel
direction would produce two feasible perturbations whose average squared
size is strictly larger. Thus at most three weights are positive.
-/
namespace HlawkaSchatten.DiagonalConstruction
variable {ι : Type*} [Fintype ι]
def momentFiber (A : ι → Fin 3 → ℝ) (b : Fin 3 → ℝ) : Set (ι → ℝ) :=
{w | (∀ i, 0 ≤ w i) ∧ ∀ k, ∑ i, w i * A i k = b k}
end HlawkaSchatten.DiagonalConstruction
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.