MATHLIBANNEX / CANONICAL DECLARATION CARD

A determinant difference bound in the sup operator norm

MathlibAnnex.ContinuousLinearMap.abs_det_sub_le_max

theorem

Controls determinant variation by replacing one matrix row at a time.

Statement

Let be a finite set of size , and give the sup norm (the zero norm on the zero space if ). For continuous real-linear maps , use the induced operator norm. If , then

For , both determinants are and the bound is .

Assumptions

The coordinate set is finite and may be empty. The coefficients are real and the operator norm is induced by the sup norm on both domain and codomain. Neither map is assumed invertible.

Conclusion

The coefficient counts the number of row replacements. The norm is specifically the sup operator norm; the estimate is not being asserted here with an unspecified norm on the same coordinate space.

The row estimate uses the sum of the absolute values of entries, not the Euclidean length of a row. This fits the sup norm through a sign vector. All coordinate matrices refer to the standard coordinate basis, so their determinants are the determinants of the original linear maps.

Proof route

The determinant is bounded by the product of the absolute row sums. A sign vector bounds each such row sum by the sup operator norm. In a one-row replacement, one row is a row of and the other rows are rows of or ; summing the replacement bounds gives the result.

Proof steps

  1. Bound a determinant by its row sums. Let be a real square matrix, and let denote the permutations of . Expanding the determinant gives

    The second inequality includes all functions , rather than only bijections; every added summand is nonnegative. The last equality is distributivity: expanding the product chooses one column independently in each row. This is precisely the row-sum bound needed below, not a bound by Euclidean row lengths.

  2. Bound each row sum by the operator norm. Let now be the standard matrix of a continuous real-linear map , so for the coordinate vector . For a fixed row , choose

    Then , and therefore

    Apply this with , , and . These three applications provide the bounds for every row appearing in the next step.

  3. Estimate one row replacement. Assume and choose one enumeration of for both rows and columns. Write and . Define

    Thus is the matrix of and that of . For , let have row equal to and every other row equal to that of . Linearity of the determinant in row gives

    Step 2 bounds the row sums of by

    Substituting these bounds into Step 1 yields

    There is one difference row and exactly other rows. For , the product over the other rows is the empty product .

  4. Sum the replacement bounds. Since and in the standard coordinates,

    This is the stated bound. If , there are no replacements and both empty determinants are , giving separately.

Main citations

Lean source signature (exact)

theorem abs_det_sub_le_max
    {ι : Type u} [Fintype ι] [DecidableEq ι]
    (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) :
    |LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) -
      LinearMap.det (Q : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))| ≤
      (Fintype.card ι : ℝ) *
        (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖
In the source Mathematical meaning
{ι : Type u} [Fintype ι] [DecidableEq ι] The finite coordinate set of size . Equality decisions support finite-index operations, rather than restrict the maps geometrically.
(P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) The continuous real-linear endomorphisms of with its sup norm. Their norms are the induced operator norms.
LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) , obtained by forgetting the continuity certificate without changing the map. The analogous expression gives .
(Fintype.card ι : ℝ) The real number counting the rows.
(max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) For , . Natural-number subtraction makes the exponent at .
In the source Mathematical meaning
‖P - Q‖ The sup operator norm of the difference .
|LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) - LinearMap.det (Q : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))| ≤ (Fintype.card ι : ℝ) * (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ The displayed full inequality is when ; at it reads .
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Equiv Finset
open scoped BigOperators

namespace MathlibAnnex

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

Exact content identity

Declaration: MathlibAnnex.ContinuousLinearMap.abs_det_sub_le_max

Accepted content SHA-256: 5f4d67395dbe0ba5df4b29d5df0eff5476d758d834bc02cb9031efe32d276f5c

Accepted source guide SHA-256: f3fbd6ce3f86e42fde4e741cc1984c4d33829563ebc554ed37cd7c38217db202

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑