MATHLIBANNEX / CANONICAL DECLARATION CARD

Positivity of the determinant maximum

MathlibAnnex.DeterminantFrame.determinantMaximum_pos

theorem

A uniformly scaled dual basis supplies a positive comparison determinant.

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. Let be an absolute maximizing frame and put . Then .

Assumptions

Only the finite-dimensional real normed space and the specified basis are inputs. Dimension zero is allowed. The maximum is taken over the closed dual unit balls, not over unit spheres.

Conclusion

The attained absolute maximum is strictly positive. Consequently a maximizing frame has nonzero determinant, but it need not be unique.

Proof route

Exhibit an admissible scaled dual basis and compare its positive determinant with the attained maximum.

Proof steps

  1. Scale all coordinate functionals by the same amount. Let be the dual coordinate functional and set

    These are the coordinate functionals, sum of their norms, and common scaling factor. Since every term of is nonnegative and ,

    Thus admissibility of the scaled coordinate frame applies to this same .

  2. Insert the comparison value into the maximum. The basis identity gives

    Use the scaled coordinate matrix and its determinant, then the maximizing comparison with :

    When , , and the empty determinant is , so the same inequality proves the result.

The proof uses the positive scale, the nonnegative row-size sum, each row norm bounded by that sum, the scaled row and the scaled coordinate frame. These are proof-context definitions, not extra arguments in the exact signature. Their common scalar is , and each row evaluates as .

Main citations

Lean source signature (exact)

/-- The basis-dependent determinant maximum is positive.  In dimension zero,
`coordinateRowSize = 0`, the empty determinant is `1`, and the same proof applies. -/
theorem determinantMaximum_pos (b : Basis (Fin n) ℝ E) :
    0 < determinantMaximum b

The explicit input is the basis; the theorem proves positivity of the maximum defined from that basis.

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 .
maximizingFrame b The selected absolute maximizing frame in the admissible set.
determinantMaximum b The real number , using the specified basis .
0 < determinantMaximum b The conclusion is . There is no extra hypothesis that a varying frame is independent or has positive determinant.

The bracketed hypotheses describe ; they are not conditions on a new frame. The theorem includes .

Names from the source comment and proof context:

In the source Mathematical meaning
coordinateRowSize b; coordinateScale b In the source comment and proof context, and , where .
coordinateFrame b The comparison frame ; its matrix is . These named objects are used in the proof, not additional theorem inputs.
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.determinantMaximum_pos

Accepted content SHA-256: 88c7250e9ce9f5c0ca4075df9465864b85e3b171bda1c39334633047151abe4f

Accepted source guide SHA-256: 22c18235cae3d2c2b36ea48aa250e62c3b1302f0b08e2b3a55449b759e4dae95

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑