MathlibAnnex.PluckerBody.body
def
Takes the real convex hull of both signs of every contraction generator.
Statement
Let and give and their coordinate sup norms. Let be the fixed coordinate Lebesgue measure on . Let be a continuous real seminorm with specified constants such that
The lower bound makes a norm. Its closed unit ball and real reference volume are Here and below a finite Lebesgue measure is read as a real number when used as a scalar.
Let be the finite set of increasing -tuples of distinct rows from . The minor-coordinate space carries its sup norm. For a linear map , put in the standard coordinate basis. Write for its maximal-minor vector and for that vector scaled by . Their coordinates and scaling are
A -contraction is a linear map satisfying for every . Write for these maps. Write for the signed generator set and for its real convex hull, so
Definition
For each integer , choose weights with sum , signs , and maps . The body consists of all resulting finite convex combinations: The signed-generator definition is a separate declaration. The exact RHS of the present definition takes its real convex hull.
Assumptions
The source and target are finite real coordinate spaces with sup norms. The seminorm is continuous and has the stated positive lower and upper comparison constants. The measure is the original coordinate Lebesgue measure. The dimensions may be zero. When , the unique empty minor has determinant ; when , the minor-index set is empty and its function space has one element. Neither case is excluded.
Conclusion
This declaration defines . Compactness and average membership are separate theorems.
The zero map is a contraction, so generator nonemptiness supplies ; this vector need not be zero when . The two alternatives give generator sign symmetry. Consequently body sign symmetry says : negate each generator in a convex combination while keeping its nonnegative weights.
Main citations
- Exact
declaration and its source —
MathlibAnnex.PluckerBody.body - signed-generator
definition —
MathlibAnnex.PluckerBody.generators - generator
nonemptiness —
MathlibAnnex.PluckerBody.generators_nonempty - generator
sign symmetry —
MathlibAnnex.PluckerBody.generators_neg - body
sign symmetry —
MathlibAnnex.PluckerBody.body_neg
Lean source signature (exact)
/-- The convex hull of all signed model-contraction generators. -/
def body {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) (N : ℕ) :
Set (Matrix.MaximalMinorIndex n (Fin N) → ℝ) := convexHull ℝ (generators M N)This is a definition of a set. The final := gives its
defining expression.
| In the source | Mathematical meaning |
|---|---|
{n : ℕ}; (N : ℕ) |
Nonnegative integers
.
Lean may infer
from M; the output dimension
is an explicit argument of body. |
Fin n → ℝ; Fin N → ℝ |
The spaces and with their sup norms. A vector is a list of real coordinates, indexed from in Lean and from in the formulas here. |
M : EquivalentSeminorm (Fin n → ℝ) |
The continuous seminorm , with , and for every . |
Matrix.MaximalMinorIndex n (Fin N) |
The index set : choose distinct rows among the rows and read them in increasing order. A function of this type into is a minor-coordinate vector . |
M.closedUnitBall;
M.closedUnitBallVolume |
and , with the finite measure read as a real number. |
M.IsContraction B |
for every , where is real-linear. |
Matrix.ballVolumeScaledMaximalMinors M B |
, whose coordinate is . |
generators M N |
The set . Its elements are minor-coordinate vectors, not the maps . |
| In the source | Mathematical meaning |
|---|---|
convexHull ℝ (generators M N) |
The real convex hull of that set: . A point is a finite sum with , , and . |
Set (Matrix.MaximalMinorIndex n (Fin N) → ℝ) |
A set of minor-coordinate vectors, so the output is a subset of . |
generators M N applies the definition
generators to M and N; it does
not multiply them.
Exact definitions used in this reading: Signed generator set.
Exact surrounding binder context (separate excerpts)
Exact source lines 12–14:
noncomputable section
namespace MathlibAnnex.PluckerBodyRead exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.PluckerBody.body
Accepted content SHA-256: 47aa096afcfbabba850a581df4da7a16644022421b88caf15f80f6542bb10efd
Accepted source guide SHA-256: 1d77d3917585faa78f7a5b0bf31a2688b36eb63227f06925b19410275f2f65f3
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73