MathlibAnnex.PluckerRecovery.LimitCertificate.image_unitBall_eq
theorem
Upgrades ball inclusion to equality by strict compact-subset volume comparison.
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. Let be a real linear map with the following properties: for every , , , , and is bijective. Then
Assumptions
The two norm models and one already fixed real linear map with the seven displayed certificate properties are inputs. In particular, its ball inclusion and determinant-volume equation must concern the same . Equality of Plücker bodies is not an input to this theorem.
Conclusion
Every image of a -unit-ball vector is in , and every point in is such an image.
Proof route
Compute the image volume for the same map and exclude a proper compact subset of the target unit ball.
Proof steps
Compute the volume of this same linear image. The change-of-variables formula gives
Here the first equality is the linear image-volume formula, used with Lebesgue measure , the continuous linear map , and the set . The second uses ; the third uses the assumed identity . This is the image-volume calculation for the map in the supplied certificate.
All volumes in this calculation are finite: are compact, is continuous, and Lebesgue measure is finite on compact sets. We therefore identify these finite measures with the same nonnegative real numbers throughout. The resulting equality of image and target measures concerns the same and that occur in the inclusion hypothesis.
Rule out a proper compact subset. Continuity of makes compact. If its known inclusion in were proper, strict measure loss inside a seminorm ball would give
The inputs at this use are Lebesgue measure, continuous seminorm , compactness of the subset, inclusion and inequality of the sets. The output contradicts Step 1. Thus . Equal measures of arbitrary sets alone would not justify equality.
The norm comparisons provide compact unit balls and positive finite volumes. Every volume used in the proof is finite; no infinite measure is treated as a real number.
Main citations
Lean source signature (exact)
/-- Inclusion and exact measure force equality: strict containment loses measure. -/
theorem image_unitBall_eq : C.linearMap '' MX.closedUnitBall = MY.closedUnitBall| 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. |
C : LimitCertificate MX MY; C.linearMap |
The parameter is supplied in the surrounding declaration context. It consists of the already fixed real linear map and exactly the six properties read in the following field rows. |
C.linearMap '' MX.closedUnitBall |
The set . The double apostrophe means set image. |
C.linearMap '' MX.closedUnitBall =
MY.closedUnitBall |
The whole conclusion , as sets rather than just as measures. |
volume; toReal |
volume is Lebesgue measure with values in
.
For a finite value, .toReal reads the same nonnegative
number as a real number. Here compactness establishes finiteness before
this operation is used. |
C.seminorm_linearMap_le |
For every , , about the supplied . |
C.image_closedUnitBall_subset |
, the inclusion to be strengthened. |
| In the source | Mathematical meaning |
|---|---|
C.closedUnitBallVolume_mul_abs_det |
, for the determinant of this same map. |
C.det_ne_zero; C.injective; C.surjective |
The other three inputs are , injectivity and surjectivity. Together with linearMap these exhaust the seven fields of the supplied certificate. |
The final equality is the conclusion about this supplied
.
The '' notation means image of a set, not a derivative. The
certificate assumptions come from the separately linked surrounding
source, rather than from an equality-of-bodies premise.
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.PluckerRecovery.LimitCertificate.image_unitBall_eq
Accepted content SHA-256: 9501ca8701e9c87788eae411cbaa361d60bc02a27377e052226e41abc195b98f
Accepted source guide SHA-256: a2dd665ae677fb439f3e4ca1bb955f05ebbff224ae739b17b62a4e93d591738b
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73