MATHLIBANNEX / CANONICAL DECLARATION CARD

The set of near-maximal dual frames

MathlibAnnex.DeterminantFrame.nearMaxFrames

def

Records a determinant deficit while keeping all dual rows contractive.

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. Write . For any , define a set of frames .

Definition

The complete defining set is

Assumptions

The space, basis and any real number are inputs. Neither nor is required to define this set.

Conclusion

A frame belongs precisely when it is admissible and its absolute determinant is at least . This definition neither chooses a frame nor asserts invertibility.

For every real , compactness of the near-maximal set follows by intersecting compact with the closed inequality set. If , nonemptiness with nonnegative deficit uses an absolute maximizing frame , since . If , membership gives and hence invertibility. These are separate consequences with different hypotheses.

Main citations

Lean source signature (exact)

/-- Frames whose determinant is within `η` of the attained maximum. -/
def nearMaxFrames (b : Basis (Fin n) ℝ E) (η : ℝ) : Set (Frame n E) :=
  {B | B ∈ unitFrameSet n E ∧
    determinantMaximum b - η ≤ |frameDeterminant b B|}

The arguments are the basis and the real deficit. The expression following := defines the set.

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 .
determinantMaximum b The real number , using the specified basis .
(η : ℝ) An arbitrary real number , with no sign assumption.
frameDeterminant b B for the frame called B, where .
In the source Mathematical meaning
Set (Frame n E) The output is a set of ordered families of continuous linear functionals.
{B | B ∈ unitFrameSet n E ∧ determinantMaximum b - η ≤ |frameDeterminant b B|} The whole defining set . A member must satisfy both conditions.

In {B | ...}, the bar means “such that”; the bars around frameDeterminant b B mean absolute value. ∧ means “and”. Neither condition is an additional requirement for forming the definition.

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.nearMaxFrames

Accepted content SHA-256: 2e4630db79e0df938f8e4afb4714f26bd877d3aa885d1ca0198f18d1d3320355

Accepted source guide SHA-256: 41ba9ced61ced25e983319b10170466a0d3db2d2c939c300353d611f7b2c90a1

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑