How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A repeated eigenvalue gives a continuum of Grassmann minimizers
Example
Let and minimize the rank-one trace objective on . Every line in is a global minimizer. The repeated bottom eigenvalue therefore produces a continuum of minimizers represented by one Grassmann critical set.
Facts & Assumptions
Given: The matrix and the rank-one Grassmann objective in the Example.
A Grassmann objective must be invariant under changing an orthonormal frame of the same subspace, and its gradient is the horizontal projection (Projected Euclidean gradients are the Stiefel and Grassmann gradients).
The horizontal tangent at a unit vector consists of vectors with (Tangent spaces and Frobenius projections on Stiefel and Grassmann).
Proof
For , , so the objective is well-defined on lines by [F1]. Since is positive semidefinite, for every unit . If , then and , so every such line is a global minimizer.
The vectors for are unit and give distinct lines: two such vectors span the same line only when their angles differ by a multiple of , which cannot occur for distinct parameters in this half-open interval. Thus they parametrize continuum many distinct lines. At each such , , so the ambient gradient and its horizontal projection vanish. The family is a continuum of Grassmann critical minimizers.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- P.-A. Absil, R. Mahony, and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Chapter 3 (2008) (standard reference, not scraped)
- Nicolas Boumal, An Introduction to Optimization on Smooth Manifolds (2023 prepublication) (standard reference, not scraped)