Equal Plücker bodies yield matching generators with an almost-isometric representative

MathlibAnnex.FiniteRecovery.nonempty_almostIsometryMatch_of_all_body_eq

theorem

Selects common minor coordinates with a target almost-isometric representative.

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 a dimension , one minor vector , and real linear maps with

Assumptions

The two norm models, , and body equality for every finite target dimension are inputs. No upper restriction on is required.

Conclusion

One dimension and one raw minor vector are shared. Both maps are contractive, but only is required to have the almost lower condition. The signs need not coincide.

Proof route

Choose target satellite parameters, refine the same support on the two compact raw sets, then extract the two representatives.

Proof steps

Choose parameters for the target norm. Let be the maximum absolute determinant of -dominated base rows; its positivity is the determinant-maximum lemma. Put . Then . Apply the target satellite package with . It supplies , radius , net and with strict satellite budget . Fix and the oriented linear support of its selected absolute maximizer.
Choose a common raw point in this support direction. For the selected linear functional , set
The raw-slice theorem applied to the target parameters says that every has a real linear representative such that
The two raw sets are compact and nonempty and have equal convex hulls by the input at this . Apply common raw selection to these sets, this same , and the displayed property of every point in its target maximum slice. It returns
with the displayed target-representative properties. This selects a particular common raw point; it does not infer that the two raw sets are equal.
Extract two representatives of the same point. Source raw membership gives , its contractivity and . Target goodness gives , contractivity, lower condition and . Thus
The fixed-dimension construction places these same maps in all nine fields, retaining the separate signs.

The lower condition is required only for the target representative . No lower estimate for or square factorization map is asserted at this stage.

Main citations

Lean source signature (exact)

theorem nonempty_almostIsometryMatch_of_all_body_eq
    {m : ℕ} (MX MY : NormModel (m + 1)) {ε : ℝ} (hε : 0 < ε)
    (hBodies : ∀ N : ℕ, MathlibAnnex.PluckerBody.body MX N = MathlibAnnex.PluckerBody.body MY N) :
    Nonempty (AlmostIsometryMatch 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 : NormModel (m + 1); MX.p; MY.p`	`NormModel n` is the source alias for `EquivalentSeminorm (Fin n → ℝ)`. Thus these are the two continuous norms , with and the displayed two-sided comparisons. 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 . Real volumes are the toReal of the finite extended measures.
`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 (AlmostIsometryMatch MX MY ε)`	Positive and existence of one record carrying all nine fields below. Nonempty asserts existence, not uniqueness.

The inputs before the final colon are the two norm models, the positive-error hypothesis and all body equalities. The conclusion Nonempty (...) asserts existence of a record with the fields displayed separately below.

Related structure, shown separately: The nine-field matching certificate.

structure AlmostIsometryMatch {m : ℕ}
    (MX MY : NormModel (m + 1)) (ε : ℝ) where
  ambientDim : ℕ
  z : PluckerCoord (m + 1) ambientDim
  sourceMap : Coord (m + 1) →L[ℝ] SupCoord ambientDim
  targetMap : Coord (m + 1) →L[ℝ] SupCoord ambientDim
  isContraction_sourceMap : MX.IsContraction sourceMap
  isContraction_targetMap : MY.IsContraction targetMap
  finMapAlmostIsometric_targetMap : FinMapAlmostIsometric MY ε targetMap
  eq_ballVolumeScaledMaximalMinors_sourceMap_or_neg :
    z = MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MX sourceMap ∨
      z = - MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MX sourceMap
  eq_ballVolumeScaledMaximalMinors_targetMap_or_neg :
    z = MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MY targetMap ∨
      z = - MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MY targetMap

In the source	Mathematical meaning
`ambientDim : ℕ`	The selected nonnegative integer .
`z : PluckerCoord (m + 1) ambientDim`	The common vector , whose coordinates are indexed by increasing -tuples of rows.
`sourceMap : Coord (m + 1) →L[ℝ] SupCoord ambientDim`	The continuous real linear map .
`targetMap : Coord (m + 1) →L[ℝ] SupCoord ambientDim`	The continuous real linear map .
`isContraction_sourceMap`	The assertion for every .
`isContraction_targetMap`	The assertion for every .
`finMapAlmostIsometric_targetMap`	For every with , . This is only a property of the target map.

In the source	Mathematical meaning
`eq_ballVolumeScaledMaximalMinors_sourceMap_or_neg`	or . The disjunction is represented by the one sign .
`eq_ballVolumeScaledMaximalMinors_targetMap_or_neg`	or . It concerns the same , but its sign need not equal .

The clauses concern one common record; ∀ means for every and ∨ means or.

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.FiniteRecovery.nonempty_almostIsometryMatch_of_all_body_eq

Accepted content SHA-256: 423229ca69e303c9e5a56a08f1719344670f047d0a6be68d119667472af8eeac

Accepted source guide SHA-256: de6f3bbc263bf654e7be4fcd424f5e6d1ad3e6b99746c7e29ff271554192e613

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73