Maximal minors scaled by the reference ball volume

MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors

def

Fixes the volume factor and increasing-row signs.

Statement

Let and give and their coordinate sup norms. Let be the fixed coordinate Lebesgue measure on . Let be a continuous real seminorm with specified constants such that

The lower bound makes a norm. Its closed unit ball and real reference volume are Here and below a finite Lebesgue measure is read as a real number when used as a scalar.

Let be linear. Index its maximal minors by increasing row selections from , using . Write for the vector of these maximal minors and for its volume-scaled version. They are given by

Definition

This definition multiplies every maximal minor by . Increasing row order fixes each determinant sign. The real ball-volume definition takes the finite measure and reads it as the real scalar . The volume is finite and positive because The first inclusion puts zero in the interior (interior-point lemma); continuity makes the ball closed and the second bounds it, giving compactness. Positivity of Lebesgue measure on a nonempty open set and finiteness on compact sets give finite positive ball volume.

Assumptions

The source and target are finite real coordinate spaces with sup norms. The seminorm is continuous and has the stated positive lower and upper comparison constants. The measure is the original coordinate Lebesgue measure. No contraction assumption is imposed on . The dimensions may be zero. When , the unique empty minor has determinant ; when , the minor-index set is empty and its function space has one element. Neither case is excluded.

Conclusion

The output is a real vector with one coordinate for each increasing row selection . The reference coordinates and measure stay fixed.

Every linear map between these finite-dimensional spaces is continuous. The type of the source therefore does not narrow the stated class of maps.

/-- The maximal-minor vector multiplied by the model ball's Lebesgue volume. -/
def ballVolumeScaledMaximalMinors {n N : ℕ}
    (M : EquivalentSeminorm (Fin n → ℝ))
    (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) : MaximalMinorIndex n (Fin N) → ℝ :=
  M.closedUnitBallVolume • maximalMinors (LinearMap.toMatrix' A.toLinearMap)

noncomputable section

namespace MathlibAnnex.Matrix

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project