Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: grunwald-pales-2024-gini-stationary-test
bibkey: grunwaldpales2024gini
doi: null
url: https://arxiv.org/abs/2408.07658v1
triage: theorem
motivation_gids:
  - D5/S3/ArithSums/GiniStationaryTest/Result.result

Stationary characterization of Gini mean comparisons

Problem

R. Grünwald and Zs. Páles, Comparison of Gini means with fixed number of variables, arXiv:2408.07658v1, §4, state:

Conjecture 2. Assume that 0 = inf I · I⁻¹ and let n ≥ 3. Then ((r, s), (p, q)) ∈ Γ_n(I) if and only if, for all u₁, …, u_n ∈ ℝ₊ such that G^{[n]}{r,s}(u₁, …, u_n) = 1, ∃ρ ∈ ℝ such that χ′{p,q}(u_k) + ρχ′{r,s}(u_k) = 0 (k ∈ {1, …, n}) the inequality 1 ≤ G^{[n]}{p,q}(u₁, …, u_n) holds.

Here is a nonempty interval in and consists of the parameter pairs satisfying for every . The stationary test universally quantifies over positive normalized tuples satisfying the common-multiplier equations. It does not assert that every normalized tuple admits such a multiplier.

The formal reading is:

Source object or conditionLean encoding and meaning
, n : ℕ, 3 ≤ n, x : Fin n → ℝ, and ∀ i, x i ∈ I
Nonempty positive interval I ⊆ Set.Ioi 0, I.OrdConnected, and I.Nonempty
sInf ((fun z : ℝ × ℝ => z.1 / z.2) '' (I ×ˢ I)) = 0; the set is precisely , rather than a product of two scalar infima
, Defs.giniMean delegates to GiniMeanEndpointComparison.giniMean, namely
, the equal-parameter branch of Defs.giniMean
Defs.chi: for , and for
Defs.chiDeriv p q t := deriv (Defs.chi p q) t
Defs.Gamma n I: comparison for every tuple from
Stationary criterionDefs.stationaryTest n r s p q: positivity, , and existence of a common real multiplier imply
Claimed equivalenceDefs.claim: all the displayed interval conditions, all , and all real

Motivation

The proposed criterion would certify global comparison on intervals with arbitrarily large coordinate ratios using only interior stationary tuples after normalization. The positive half-line is such an interval, so a failure there refutes the full equivalence.

Gap

The source proves the bounded-interval characterization in Theorem 7 and states Conjectures 1 and 2. Searches for the title, arXiv identifier 2408.07658, DOI 10.1007/s00025-025-02370-0, and the authors with “Conjecture 2”, “counterexample”, or “proof” found no settlement. Grünwald’s 2025 Debrecen–Katowice seminar report (Ann. Math. Sil. 39(2) (2025), 381–394) restates the question. Conjecture 1 of the same paper is refuted in the endpoint comparison dossier. Citation indexes were not checked exhaustively. Interior stationarity alone does not control escape toward the boundary of the positive normalized simplex.

Route

Fix any , take , and choose and . Normalization gives . The characteristic derivatives are

The multiplier equations therefore put every coordinate on one level of . Distinct positive points on that level satisfy , and the level contains at most two positive points. A nonconstant normalized tuple has values . Put and . Each coordinate satisfies and , hence

Since , one has . Thus

Consequently on every nonconstant stationary tuple. The constant normalized tuple has every coordinate one and gives equality. This proves the stationary test.

Falsifier

For , use and . Then

The identity

gives because all denominators are positive and cubing preserves order. In particular, and give and . The pair passes the stationary test but lies outside for every .

Evidence

The theorem D5/S3/ArithSums/GiniStationaryTest/Result.result has the unconditional type ¬ Defs.claim. Its axiom closure is exactly propext, Classical.choice, and Quot.sound.

Its mathematical dependencies are Result.counterexample_family, Stationary.stationaryTest_one_zero_two_negOne, Stationary.chiDeriv_parameters, Witness.not_mem_Gamma, Witness.witness_comparison, and Witness.witness_identity, together with the private stationary level, moment, and finite-sum helpers. The existing unequal-parameter mean and highTuple come from GiniMeanEndpointComparison; real-power, derivative, finite-sum, and conditional-infimum facts come from Mathlib. The family theorem supplies both the stationary criterion and nonmembership for the same and parameters, and result specializes both conjuncts at . The quotient set of equals , whose infimum is zero.

ChatGPT Pro supplied the counterexample route; the Lean evidence supports the first triage item.

Triage

  1. PROVED — the stationary characterization fails in every dimension . Result.counterexample_family proves that passes the stationary test and is outside . Stationary.stationaryTest_one_zero_two_negOne proves the stationary part for every nonzero dimension. Result.result refutes the full universally quantified claim.

  2. PROVED in prose — every positive parameter scale. Fix and set . For either parameter pair or , and . The positive factor cancels from each multiplier equation, so normalization and stationarity transfer to . The proved stationary criterion and the increasing map give the scaled stationary criterion. Conversely, take for ; the same identity transfers the strict comparison reversal to .

  3. PROVED in prose — boundary escape. For , the positive tuple with has mean one. Its objective is , which tends to as . Thus the objective has infimum on the positive normalized simplex, despite being nonnegative at all its stationary tuples.

  4. PROVED in prose — comparison implies the stationary criterion. For any admissible and positive tuple , put and . The zero quotient infimum provides with . Set . Every lies between and , hence belongs to by interval connectedness. Comparison on and homogeneity give comparison at for all parameters, including equal parameters. If , the required inequality follows, whether or not is stationary.

  5. COMPUTED — a rational three-variable instance. At , the cubed comparison is , equivalently . These exact arithmetic values illustrate the proved family.

  6. OPEN — the comparison region. What is a correct characterization of when ?

ASSUMED-UNVERIFIED

The journal version’s text is unverified; the quotation and locators refer to arXiv:2408.07658v1. The literature scope does not establish an exhaustive literature or priority claim.

The positive-scale extension, boundary-escape limit, and general surviving implication are proved in prose above, not in the companion Lean modules. The Lean family fixes parameter scale and covers every .