DefinitionDefinition: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Complex Stiefel and Grassmann optimization conventions

Definition

For $1 \leq r \leq n$ , set ${St}_{C} (n, r) = {X \in C^{n \times r} : X^{*} X = I_{r}}$ and ${Gr}_{C} (r, n) = {St}_{C} (n, r) / U (r)$ . The class $[X]$ represents the complex column space of $X$ ; two orthonormal frames represent the same space exactly when they differ by right multiplication by a unitary $r \times r$ matrix. Regard each complex matrix space as a real vector space and use the real Frobenius inner product $⟨ U, V ⟩_{R} : = Re tr (U^{*} V) .$ Give the complex Stiefel manifold its induced metric. On the complex Grassmann quotient, represent tangent vectors horizontally by matrices $Z$ with $X^{*} Z = 0$ and pair these representatives by $⟨ \cdot, \cdot ⟩_{R}$ . For $A = A_{0} + i A_{1} \in C^{n \times r}$ , write $ρ (A) : = (\begin{array}{cc} A_{0} & - A_{1} \\ A_{1} & A_{0} \end{array}) \in R^{2 n \times 2 r}$ for its realification, the real matrix acting on real/imaginary coordinates as $A$ acts on complex coordinates. Write $Herm (A) = (A + A^{*}) / 2$ .

Facts & Assumptions

Given: Integers $1 \leq r \leq n$ and complex matrix spaces with their usual real-coordinate topology.

[F1]

A Riemannian metric is a smooth positive-definite real bilinear pairing on each tangent space (Riemannian metric and riemannian manifold).

[F2]

The coordinatewise product on a finite real coordinate space is its Euclidean inner product (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F3]

Complex Stiefel frames are quotiented by the right unitary action, and graph charts give the Grassmannian's local coordinates (Stiefel spaces, Grassmannians, and tautological bundles).

Proof

technique · identify complex matrices with pairs of real matrices and verify the quotient pairing

1.1F1F2givenalgebra

Write $U = A + i B$ and $V = C + i D$ with real matrices. For $z = x + i y$ , $ρ (U) (x, y) = (A x - B y, B x + A y)$ , the real and imaginary parts of $U z$ ; hence $ρ (U V) = ρ (U) ρ (V)$ , $ρ (U)^{T} = ρ (U^{*})$ , and, when $U$ is invertible, $ρ (U^{- 1}) = ρ (U)^{- 1}$ . Also $⟨ U, V ⟩_{R} = tr (A^{T} C + B^{T} D)$ , the ordinary Euclidean inner product on the real and imaginary coordinates. It is real bilinear, symmetric, and positive on nonzero matrices by [F2]; its restriction to each real tangent space is positive definite, as required by [F1].

1.2F1F2F3givenalgebra

In a local complex Grassmann graph chart, choose a smooth orthonormal frame section $X (u)$ from the frame-bundle trivialization in [F3], and set $P (u) = X (u) X (u)^{*}$ . For a chart tangent $v$ , differentiating $X (u)^{*} X (u) = I$ makes $A = X (u)^{*} D X_{u} [v]$ skew-Hermitian. The first term $X (u) A$ is vertical: for every skew-Hermitian $A$ , the Cayley curve $Q (t) = (I_{r} - \frac{t}{2} A)^{- 1} (I_{r} + \frac{t}{2} A)$ satisfies $Q (t)^{*} Q (t) = I_{r}$ near zero and $Q (t) = I_{r} + t A + O (t^{2})$ . Thus the horizontal component $Z = (I - X (u) X (u)^{*}) D X_{u} [v]$ is the unique representative of $v$ . Then $D P_{u} [v] = Z X (u)^{*} + X (u) Z^{*}$ . For horizontal $Z, W$ , direct expansion gives $\frac{1}{2} Re tr ((Z X^{*} + X Z^{*})^{*} (W X^{*} + X W^{*})) = Re tr (Z^{*} W)$ . Hence the quotient pairing has smooth coefficients in every graph chart. In a local product chart of the frame bundle, matrix entries vary smoothly, so the ambient real Frobenius pairing has smooth coefficients on the complex Stiefel space as well.

2.1F3givenstep 1.1algebra∎

The complex frame quotient and its local graph charts are those of [F3]. For unitary $Q$ , cyclicity of trace and $Q Q^{*} = I$ give $⟨ U Q, V Q ⟩_{R} = Re tr (Q^{*} U^{*} V Q) = Re tr (U^{*} V)$ . Thus the right unitary action is isometric, and the Frobenius pairing of horizontal representatives is independent of the chosen orthonormal frame.

Depends on

Used by

Finite-budget Riemannian trust-region method Algorithm
Polar retraction on the complex Grassmannian Definition
Complex finite-basis PC-VAR optimization on Grassmann Example
Finite-dimensional complex Stiefel and Grassmann manifolds are compact Proposition
Gradient of a unitary-invariant Hermitian projector energy Proposition
Complex Stiefel and Grassmann tangent projections Theorem
The complex Grassmann polar map is a first-order retraction Theorem

Dependency tree · two levels

21 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

Peter A. Absil, Robert Mahony, and Rodolphe 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)
Nicholas D. S. Manton, Optimization algorithms exploiting unitary constraints, IEEE Transactions on Signal Processing 50 (2002), §§IV and VI (standard reference, not scraped)