Lemma 4, proof — interior cone point gives positive coefficients
ProvedMcFadden1974.QPTest.interior_gives_positive_coefficientsconditional-logitconvex-geometrylinear-optimizationp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be the convex cone generated by the vectors . If zero lies in the interior of , then strictly positive scalars can represent zero:
The scalars can be rescaled so that every coefficient is at least one. Thus the quadratic program (22) attains a minimum of zero. This is the constructive half of the cone argument in Lemma 4.
Formalization Note The representation includes all ordered pairs, even those with zero weighted difference.
Preamble
import Definitions.Def_McFadden1974_QPTest_ChoiceData set_option autoImplicit false
Formal statement
namespace McFadden1974.QPTest
/-- McFadden (1974), p. 117 (PDF 13), Lemma 4, proof, second paragraph.
If zero is interior to the generated cone, a strictly positive coefficient
exists for every ordered index triple, yielding zero; rescaling those
coefficients gives a feasible zero of (22). The paper's abbreviated sum is
read with the `i,j` sums present, as required by equation (22). -/
theorem interior_gives_positive_coefficients {N K : ℕ} (d : ChoiceData N K)
(h : (0 : EuclideanSpace ℝ (Fin K)) ∈ interior d.coneSet) :
(∃ α : (n : Fin N) → Fin (d.J n) → Fin (d.J n) → ℝ,
(∀ n i j, 0 < α n i j) ∧
(∑ n, ∑ i, ∑ j, α n i j • d.w n i j) = 0) ∧
IsLeast ((fun y : EuclideanSpace ℝ (Fin K) => ‖y‖ ^ 2) '' d.qpFeasible) 0 := by sorry
end McFadden1974.QPTest
Source
McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press (1974), p. 117, Lemma 4, proof, second paragraph (PDF p. 13)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.