MATHLIBANNEX / CANONICAL DECLARATION CARD

A volume-normalized linear contraction obtained by a limit

MathlibAnnex.PluckerRecovery.nonempty_limitCertificate_of_pluckerBodies_eq

theorem

Takes a compact operator limit preserving the exact volume equation.

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. Assume for every . There is one real linear with

Assumptions

The positive-dimensional coordinates, norm models and equality of every finite body are the inputs. No distortion parameter is supplied.

Conclusion

The same real linear bijection is contractive from the norm to the norm and has the exact determinant-volume normalization. Only ball inclusion is asserted here; equality of the two ball images is proved separately.

Proof route

Choose vanishing distortions, bound the maps in one compact operator ball, and pass the estimate and determinant equation to the same subsequence limit.

Proof steps

  1. Choose and bound the sequence. Set . For each , linear recovery at the positive parameter gives

    Because and ,

    Consequently . These are the half-distortion estimate and the reference-norm estimate, applied to the selected certificates.

  2. Apply compactness in the operator space. For real linear maps , use the reference operator norm . All maps belong to the same closed operator ball . The real space of linear maps is finite-dimensional, so this ball is compact. The compact subsequence construction returns strictly increasing and one with in operator norm. For each fixed ,

    Strict increase gives and hence . In compact subsequence selection, the input sequence lies in one compact set in a first-countable space; the output is a limit in that set and a strictly increasing subsequence. The continuous evaluation map and its RHS is , giving the same pointwise limit.

  3. Pass the norm estimate to that limit. Continuity of gives . Therefore

    Every term is at most , so . If , then , giving . These are the limit contraction and its ball inclusion.

  4. Pass the volume identity to the same map. The determinant is continuous in the entries, so . Thus

    This is the limit determinant-volume equation. Since , the determinant cannot vanish. It makes injective, and an injection from finite-dimensional to itself is surjective. Store this same in every field.

The subsequence and its convergence are construction evidence, not extra public fields. Operator compactness uses the reference sup norm; contraction compares the stored norms .

Main citations

Lean source signature (exact)

/-- Equality of all finite Plücker bodies yields a limit recovery certificate. -/
theorem nonempty_limitCertificate_of_pluckerBodies_eq {m : ℕ}
    (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))
    (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) :
    Nonempty (LimitCertificate 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 . 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 .
Nonempty (LimitCertificate MX MY) Existence of one record with all seven fields below, without a supplied .

There is no supplied error parameter in this theorem. From the two norm models and hBodies, the final Nonempty (...) asserts existence of one map with all seven properties below.

Related structure, shown separately: The seven-field limit certificate.

structure LimitCertificate {m : ℕ}
    (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) where
  linearMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)
  seminorm_linearMap_le : ∀ x, MY.p (linearMap x) ≤ MX.p x
  image_closedUnitBall_subset : linearMap '' MX.closedUnitBall ⊆ MY.closedUnitBall
  closedUnitBallVolume_mul_abs_det : MX.closedUnitBallVolume * |ContinuousLinearMap.det linearMap| = MY.closedUnitBallVolume
  det_ne_zero : ContinuousLinearMap.det linearMap ≠ 0
  injective : Function.Injective linearMap
  surjective : Function.Surjective linearMap
In the source Mathematical meaning
linearMap The chosen continuous real linear map .
seminorm_linearMap_le for every .
image_closedUnitBall_subset : every vector with satisfies .
closedUnitBallVolume_mul_abs_det , for this same and these finite real volumes.
det_ne_zero .
In the source Mathematical meaning
injective If , then .
surjective Every is for some .

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_limitCertificate_of_pluckerBodies_eq

Accepted content SHA-256: f75c8b9f4dde311c3da7804a52d8a34ebabbe6c9c6d8e0d84645606f46bf634f

Accepted source guide SHA-256: cc39bf21afd8952fd7945189e07f9c0deee09ac5bf62c9a6ab3723f1b2466016

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑