MATHLIBANNEX / CANONICAL DECLARATION CARD

A common inverse estimate from row Cramer

MathlibAnnex.DeterminantFrame.inverseBoundConstant_bound

theorem

Controls all near-maximal inverse frames by an explicit basis-dependent constant.

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 the dual coordinate functionals, and put and . Fix . Define For and every ,

Assumptions

The only deficit hypothesis is ; the frame satisfies both the dual-row contraction condition and the displayed determinant lower bound. The coefficient is arbitrary. There is no extra hypothesis.

Conclusion

The same positive works for every frame in this near-maximal set and every coefficient. The coordinate inverse and matrix inverse are distinct maps; the resulting norm is the given norm of .

Proof route

Use row Cramer with a scaled coordinate functional, divide by the determinant gap, and transport the coordinate bound through the inverse coordinate map.

Proof steps

  1. Read the row-Cramer identity one coordinate at a time. Since and ,

    For , let denote the matrix obtained by replacing row with . The row-Cramer formula is

    Here specifies the replaced row, while runs over the basis coordinates. Apply provider row form of Cramer to and the row ; its determinant hypothesis is the nonvanishing just shown. The provider uses , so its column replacement is exactly the row replacement above.

  2. Multiply by the coefficients and show the two sums. For the same functional and the given column ,

    The second line interchanges two finite sums; the third is matrix multiplication. Finally, linearity of and the definition of give

    Thus these calculations give the row-replacement identity in basis coordinates, with this same . The column is a coordinate vector; only is the corresponding vector of .

  3. Select one coordinate and bound its numerator. Fix and take . The definition of gives

    This is scaled-row admissibility. Hence replacing any row of the admissible frame with this gives another admissible frame, by admissible row replacement, and the determinant maximum gives

    In Step 2 the functional evaluation is now exactly

    Taking absolute values in that identity and bounding each summand yields

    This is the Cramer numerator bound for the same frame, coefficient column and scaled coordinate functional.

  4. Divide by the gap and return to the given norm. Since and , the previous estimate implies

    This is the coordinatewise inverse estimate. Taking the maximum over and then applying the operator norm of gives

    The argument with a coordinate is for . When , both vectors are zero, and , so the conclusion is immediate. In every dimension and the leading in ensures positivity.

The coordinate factor and ambient inverse constant are the displayed ; positivity of that constant requires the same gap. the common inverse-bound structure stores exactly a real , a proof , and the uniform inverse estimate. the nonzero determinant criterion and reconstruction through the inverse frame also give , so is injective, as in frame-map injectivity. The functional row is evaluation on the basis; expansion of a functional in these coordinates and the transposed Cramer replacement justify the scalar identity used above. The row replacement operation and replacement determinant keep the frame, its matrix and its evaluation map distinct.

Main citations

Lean source signature (exact)

/-- The explicit Cramer estimate transported back through the inverse coordinate map. -/
theorem inverseBoundConstant_bound (b : Basis (Fin n) ℝ E)
    {η : ℝ} (hηD : η < determinantMaximum b) {B : Frame n E}
    (hB : B ∈ nearMaxFrames b η) (c : Fin n → ℝ) :
    ‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)‖ ≤
      inverseBoundConstant b η * ‖c‖

The hypotheses are hηD and hB; c is an arbitrary vector, not a further bound.

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.
determinantMaximum b The real number , using the specified basis .
hηD : η < determinantMaximum b The input hypothesis .
hB : B ∈ nearMaxFrames b η The frame called B satisfies for every and . Together with the gap, this implies .
(c : Fin n → ℝ); ‖c‖ An arbitrary coordinate vector and its sup norm .
frameMatrix b B The real matrix .
(frameMatrix b B)⁻¹.mulVec c The vector . ⁻¹ is matrix inverse and mulVec is matrix multiplication by a column.
(coordinateEquiv b).symm (…) The vector . symm selects the inverse coordinate isomorphism; the norm outside this expression is the norm of .
In the source Mathematical meaning
inverseBoundConstant b η , where and .
‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)‖ ≤ inverseBoundConstant b η * ‖c‖ The complete conclusion , for this frame and every supplied coefficient vector.

Braces allow Lean to infer a parameter. Parentheses provide explicit arguments. →L[ℝ] in the surrounding definitions denotes a continuous real linear map.

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

Accepted content SHA-256: 19f4ef4c81f82be19fbdddbef2b0612b3e7a770bdf8a166c617b562568245df9

Accepted source guide SHA-256: ebd0581a963aededaa6753c3d0ec9e22b754fde2d8f624d16a916fc2d5e495fc

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑