MATHLIBANNEX / CANONICAL DECLARATION CARD

Almost-contractive linear recovery with exact volume scaling

MathlibAnnex.PluckerRecovery.nonempty_linearCertificate_of_pluckerBodies_eq

theorem

Recovers one bijective linear factor with a norm estimate and exact volume scaling.

Statement

Let and with the reference sup norm and standard Lebesgue measure . The continuous norms have fixed positive comparison constants Set , and , , as positive finite real numbers. For a real linear map , let be its matrix in the standard bases. The minor-coordinate space has one coordinate for each increasing -tuple of distinct rows from , and Define the signed generator set and its real convex hull by Define in the same way using . The generators are vectors of minors, not linear maps. Suppose and for every . There exist , real linear maps , a real linear bijection with

Assumptions

The coordinate dimension is positive. The inputs are the norms with the stated positive comparison bounds, , and equality for every nonnegative . The nonzero leading minors used in the proof are obtained during the construction, not assumed.

Conclusion

The same bijection factors the selected representatives and satisfies both the norm estimate and the exact volume equation. No upper restriction is required.

Proof route

Anchor the common raw point at a nonzero leading coordinate, recover its chart factor, and compute the estimate and volume identity for that factor.

Proof steps

  1. Anchor the same representatives. Let be the maximum absolute determinant of a family of real linear functionals dominated by , and choose target satellite parameters with . The absolute maximizing target base has

    Thus every target support maximizer has nonzero leading minor coordinate, by the leading-coordinate lemma. anchored common raw selection supplies one and the same contractive , with signs , the target condition whenever , and

    Here selects the first rows. Let and be the corresponding square matrices. Both are nonsingular because their determinants give the nonzero coordinate , up to nonzero signs and volumes. Put . Each coordinate gives

    This is the weighted minor relation. Its nonzero anchor uses the determinant gap, including when .

  2. Recover the factor, row by row. Put

    The maximal minors of are times those of . The same proportionality holds for any ordered row selection: sorting contributes the same permutation sign on both sides, and a repeated row makes both determinants zero. This is the passage from increasing to ordered minors.

    Fix corresponding row vectors of and of . Applying the proportionality to the leading block and to its th-row replacement gives

    Row Cramer gives each coordinate of the two normalized rows. Substituting both proportionalities, with , gives

    This is the source’s row-coordinate calculation for these two matrices and this fixed row. Equality in every coordinate now yields

    Thus on all rows, as recorded by the chart factor theorem. Both leading blocks are nonsingular, so this same is invertible by chart factor invertibility. Since is onto,

    For fixed the factor is unique: implies , hence . This uniqueness concerns the fixed representatives, not all possible choices of them.

  3. Evaluate the same factor in the norm estimate. If , injectivity gives . Homogeneity of the target lower condition at gives

    If , both sides are zero. The resulting universal non-strict estimate is the factor model bound. There is no division by .

  4. Compute its determinant and volume. The leading minor of gives . Substitute into the weighted leading-minor relation:

    Cancel to obtain . Taking absolute values, using and , gives

    The signed determinant identity and absolute volume identity use this same factor.

Factor uniqueness in the proof is for fixed anchored representatives; the public certificate only asserts existence. It does not publicly store the intermediate maps’ two contractivity fields. Different common-point selections can differ.

Main citations

Lean source signature (exact)

theorem nonempty_linearCertificate_of_pluckerBodies_eq
    {m : ℕ} (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) {ε : ℝ} (hε : 0 < ε)
    (hBodies : ∀ N : ℕ, MathlibAnnex.PluckerBody.body MX N = MathlibAnnex.PluckerBody.body MY N) :
    Nonempty (LinearCertificate MX MY ε)
In the source Mathematical meaning
Fin (m + 1) → ℝ; →L[ℝ] The reference , , with sup norm; arrows mean continuous real linear maps. Source indices correspond to formula indices .
MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ); MX.p; MY.p The two continuous norms and their positive comparison constants. The applications MX.p x and MY.p x mean .
MX.closedUnitBall; MY.closedUnitBall; MX.closedUnitBallVolume; MY.closedUnitBallVolume The sets and their real Lebesgue volumes . These finite nonnegative measures are read as real numbers.
hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N For every nonnegative , the real convex hulls and are equal. The source body is the convex hull of the vectors , where is real linear and for every . The target body uses in place of .
hε : 0 < ε; Nonempty (LinearCertificate MX MY ε) Positive and existence of one record carrying all twelve fields below.

The inputs are the two norm models, hε and hBodies. The conclusion Nonempty (LinearCertificate MX MY ε) asserts that all twelve fields below can be filled for the same chosen objects.

Related structure, shown separately: The twelve-field linear certificate.

structure LinearCertificate {m : ℕ}
    (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) (ε : ℝ) where
  q : ℕ
  sourceMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin ((m + 1) + q) → ℝ)
  targetMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin ((m + 1) + q) → ℝ)
  linearMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)
  factor : targetMap.comp linearMap = sourceMap
  range_sourceMap_eq_range_targetMap : Set.range sourceMap = Set.range targetMap
  injective : Function.Injective linearMap
  surjective : Function.Surjective linearMap
  one_sub_mul_seminorm_linearMap_le : ∀ x, (1 - ε) * MY.p (linearMap x) ≤ MX.p x
  det : ℝ
  det_eq : det = ContinuousLinearMap.det linearMap
  closedUnitBallVolume_mul_abs_det : MX.closedUnitBallVolume * |det| = MY.closedUnitBallVolume
In the source Mathematical meaning
q : ℕ The extra coordinate dimension , so the common codomain is . This field is not the target norm .
sourceMap The continuous real linear map .
targetMap The continuous real linear map .
linearMap The same continuous real linear factor .
factor : targetMap.comp linearMap = sourceMap , that is, for every ; .comp is composition in this order.
range_sourceMap_eq_range_targetMap Equality of the image sets .
injective implies .
surjective For each there is such that .
one_sub_mul_seminorm_linearMap_le The estimate for every .
det : ℝ The stored real value of ; its identification is recorded by the next field.
In the source Mathematical meaning
det_eq : det = ContinuousLinearMap.det linearMap The field det equals . This is the determinant of the square linear factor , not of either rectangular map.
closedUnitBallVolume_mul_abs_det Using det_eq, this field states , for the same .

Exact definitions: the signed generator set; its real convex hull.

Surrounding assumptions and aliases.

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

Exact content identity

Declaration: MathlibAnnex.PluckerRecovery.nonempty_linearCertificate_of_pluckerBodies_eq

Accepted content SHA-256: b079b84f15ab93a5cabc899b7d29f497ca4248d03dadecee1748b96afb1f855e

Accepted source guide SHA-256: 8c1e0fb1cbe47d104f9c2750a5fe7f090c99c9eff7e1827c6889a9633a0e8f76

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑