MATHLIBANNEX / CANONICAL DECLARATION CARD

All Plücker bodies determine the norm up to linear isometry

MathlibAnnex.EquivalentSeminorm.nonempty_linearIsometryEquiv_of_pluckerBodies_eq

theorem

Recovers a real linear equivalence preserving the two supplied norms.

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 exists a real linear bijection satisfying

Assumptions

The two norm models and equality of every finite Plücker body are inputs.

Conclusion

The isometry is between equipped with and equipped with . Preservation of the reference sup norm is not the conclusion.

Proof route

Keep the same limit map and its ball image, recover the norms from positive scaled sublevel sets, and promote that map to a linear equivalence.

Proof steps

  1. Choose the limit map once. Input the two norm models and body equalities to limit recovery. It supplies bijective , contraction, ball inclusion and the exact determinant-volume equation. ball image equality for that certificate gives for the same .

  2. Read both gauges from the ball image. For each , homogeneity, linearity and bijectivity give

    The middle equivalence uses . Its reverse implication also uses injectivity: if with , then . If the two nonnegative numbers and differed, their positive midpoint would satisfy one comparison and not the other. Thus ; at both values are zero. The norm reconstruction from a bijective ball image takes positive definiteness of , the real linear bijection and exact ball image as inputs, and returns this equality at each .

  3. Retain that map in the equivalence. Bijectivity promotes the same to a real linear equivalence. Store it and in the two fields of the model isometry structure. No sphere restriction is specified by these fields.

The recovered equivalence preserves and on the same coordinate vectors; it need not preserve the reference sup norm.

Main citations

Lean source signature (exact)

/-- Equality of all finite Plücker bodies gives an equivalence preserving the stored norms. -/
theorem nonempty_linearIsometryEquiv_of_pluckerBodies_eq {m : ℕ}
    (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))
    (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) :
    Nonempty (LinearIsometryEquiv 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 (LinearIsometryEquiv MX MY) Existence of a real linear equivalence preserving the two stored norms, with the fields below.

From the two norm models and hBodies, the output Nonempty (...) asserts existence of one linear equivalence with the norm-preservation field below.

Related structure, shown separately: The norm-preserving linear-equivalence structure.

/-- A linear equivalence preserving the two stored seminorms. -/
structure LinearIsometryEquiv (MX : EquivalentSeminorm E) (MY : EquivalentSeminorm F) where
  toLinearEquiv : E ≃ₗ[ℝ] F
  map_p_eq : ∀ x, MY.p (toLinearEquiv x) = MX.p x
In the source Mathematical meaning
toLinearEquiv : E ≃ₗ[ℝ] F A bijective real linear map, together with its inverse. Here the two carriers are both , and the map is the selected .
map_p_eq : ∀ x, MY.p (toLinearEquiv x) = MX.p x for every . The source and target model parameters select which norm is applied on each side.

Surrounding assumptions and aliases.

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

Exact content identity

Declaration: MathlibAnnex.EquivalentSeminorm.nonempty_linearIsometryEquiv_of_pluckerBodies_eq

Accepted content SHA-256: f97501ad5aec2527ce2b2188acf6ce634ddb722f1fd641685d661e2a4050a3d0

Accepted source guide SHA-256: d8c3ceec1cea7b2596e3363e9ae717e5701a6330c73f051cfec5982b98c2f231

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑