MATHLIBANNEX / CANONICAL DECLARATION CARD

An attained absolute determinant maximum

MathlibAnnex.DeterminantFrame.exists_maximizingFrame

theorem

Selects a maximizing dual frame for a specified basis.

Statement

Let , let be a finite-dimensional real normed vector space, and fix an ordered basis . Write for the coordinate isomorphism, defined by , and give its coordinate space the sup norm (zero in dimension zero). A frame is an ordered family of continuous real linear functionals, with no independence assumed. Its matrix and evaluation map are The admissible frames form the product of closed dual unit balls The norm on need not be a coordinate sup norm. There is a frame such that

Assumptions

The space is finite-dimensional over and is its specified basis indexed by elements. Each admissible row lies in the closed operator unit ball. No independence of the varying frames, positive dimension, or uniqueness of a maximizing frame is assumed.

Conclusion

One admissible frame attains the maximum of the absolute determinant. The numerical maximum depends on , although its value does not depend on which maximizer is chosen. Positivity is a separate result.

Proof route

Use compactness of the finite product of dual balls and continuity of the absolute determinant.

Proof steps

  1. Supply the compact domain. The dual space is finite-dimensional, hence its closed unit ball is compact. The compact dual unit ball and finite product of these balls give

    The zero-frame witness is for every , so the domain is nonempty, also when .

  2. Maximize the correct function. Every entry is continuous, and the determinant is a finite sum of products of entries. Therefore is continuous, as in continuity of the frame determinant. Apply the extreme-value theorem to this continuous real function on the nonempty compact set . Its output is with the displayed comparison for every . This is an absolute maximum; no sign of is asserted.

The selected maximizer is named by the choice of maximizing frame and its value by the attained maximum. The coordinate identity is evaluation in basis coordinates. These names do not add uniqueness or a nonzero determinant to this theorem.

Main citations

Lean source signature (exact)

/-- Existence of an attained absolute determinant maximum. -/
theorem exists_maximizingFrame (b : Basis (Fin n) ℝ E) :
    ∃ B ∈ unitFrameSet n E,
      ∀ C ∈ unitFrameSet n E,
        |frameDeterminant b C| ≤ |frameDeterminant b B|

The basis is the explicit input. The result after the colon is the existence and maximizing property of one frame.

In the source Mathematical meaning
n; b : Basis (Fin n) ℝ E A nonnegative integer and the ordered basis of .
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] The ambient is a finite-dimensional real normed vector space, with its given norm (not necessarily a coordinate sup norm). These hypotheses occur in the separate surrounding excerpt.
Fin n → ℝ The coordinate space with the sup norm. Lean indexes the coordinates by ; the formulas here use .
Frame n E The ordered families with continuous and real linear. No independence is part of this type.
unitFrameSet n E The set . Its elements are families of functionals, not points of .
∃ B ∈ unitFrameSet n E There exists a frame . This chosen maximizing frame is called B in the source.
∀ C ∈ unitFrameSet n E The comparison is required for every , called C in the source.
In the source Mathematical meaning
frameDeterminant b C; frameDeterminant b B Respectively and , with .
|frameDeterminant b C| ≤ |frameDeterminant b B| The output comparison . The bars are absolute values, so no orientation sign is fixed.

Here ∀ means “for every”, ∃ means “there exists”, and ∈ means set membership. Juxtaposition such as unitFrameSet n E is function application, not multiplication.

Relevant surrounding context (separate exact excerpts)

Exact source lines 47–49:

variable {n : ℕ}
variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]

Full surrounding source. These excerpts are separate from the declaration above.

Surrounding assumptions and aliases: exact source, lines 37–49. The full original context is retained with the source evidence.

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

Exact content identity

Declaration: MathlibAnnex.DeterminantFrame.exists_maximizingFrame

Accepted content SHA-256: dbb5325a3743a839031e5cede9e311bc25abe486e04b062d2f3d4c544721760b

Accepted source guide SHA-256: 2ba8385db97c730d988234e7310a00804bf016106832f42d777a594bd7e1996c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑