MATHLIBANNEX / CANONICAL DECLARATION CARD

A target contraction generator lies in the source body

MathlibAnnex.PluckerBody.normalizedGenerator_mem_of_sphereIsometry

theorem

Transfers membership through two extensions with the same boundary trace.

Statement

Let , put , and give and their coordinate sup norms. Let be the fixed coordinate Lebesgue measure on . Let be continuous real seminorms with specified positive constants such that

Both and are norms. For each define the closed unit ball, unit sphere, and real reference volume by The finite 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 its two volume-scaled versions. 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

Let be a bijection preserving chord distances, so Read its radial extension on the reference coordinates: For , positivity of makes , so this is defined.

Let be a -contraction, meaning for all . Then its target generator belongs to the source body:

Assumptions

The dimension is . The norms have the stated continuity and positive comparison constants; is a bijective chord-distance isometry. Here must be a -contraction. The integration measure remains fixed, and is any nonnegative integer.

Conclusion

The positively signed target vector belongs to , regardless of the orientation sign of the radial extension.

The historical name “normalized generator” refers here to the volume-multiplied vector . It is not division by .

Proof route

Extend the boundary contraction, compare its average with a radial average, then use sign symmetry.

Proof steps

  1. Form the boundary map and extend it. Let for . Then

    The contraction hypothesis and chord isometry supply exactly the input of the boundary-extension theorem. Choose its single witness . For any , write for its Fréchet derivative where it exists and for zero otherwise. Define

    The five outputs are

  2. Compare two extensions only on the boundary. Put . For every ,

    The equality holds because . The maps may differ away from the boundary. Let denote the operator norm for the two coordinate sup norms. Their global reference-norm estimates are

    For the second, use linearity of and the radial -Lipschitz estimate with the comparison constants; it is not a -Lipschitz assertion for the radial extension.

  3. Transfer the minor integrals and normalize. For each , the boundary comparison gives

    Apply the boundary-equality theorem for maximal-minor integrals with the continuous seminorm , compact ball , positive dimension , maps , and the global Lipschitz bounds of Step 2. Its remaining hypothesis is exactly on , also established in Step 2. This produces the displayed equality for the same row selection . Compact-set integrability of derivative generators applied separately to and on justifies their vector integrals. For either or ,

    The cancellation uses . Substituting the equal minor integrals yields

    This is the average comparison from boundary traces; it compares the averages, not the functions away from their common boundary.

  4. Insert the signed radial average and remove its sign. The common-sign radial-average theorem supplies and

    Read from the known member at the right: Step 1 gives ; Step 3 identifies this vector with ; the radial-average formula identifies it with . If , this already gives the conclusion. If , body sign symmetry applied to gives .

Main citations

Lean source signature (exact)

/-- A normalized target generator belongs to the source body under a unit-sphere isometry. -/
theorem normalizedGenerator_mem_of_sphereIsometry {m N : ℕ}
    {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}
    (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)
    (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) (hA : MY.IsContraction A) :
    Matrix.ballVolumeScaledMaximalMinors MY A ∈ body MX N

The final colon separates the inputs from the membership conclusion. In particular, hA is a hypothesis on A, not a new map.

In the source Mathematical meaning
{m N : ℕ}; Fin (m + 1) → ℝ; Fin N → ℝ , , , . Coordinate vectors have the sup norm; braces mark parameters Lean can infer.
MX; MY The continuous seminorms and , with their positive lower and upper comparison constants stated in this Card.
Space MX; Space MY The same vectors of , now with norms and , respectively.
sphere (0 : Space MX) 1; sphere (0 : Space MY) 1 and . The arguments are center and radius .
Δ : ... ≃ᵢ ... A bijective isometry : for all . The symbol in the code asserts both bijectivity and distance preservation.
A : ... →L[ℝ] ... A continuous real-linear map .
hA : MY.IsContraction A The target-norm contraction bound for every ; it is the norm stored in , not .
Matrix.ballVolumeScaledMaximalMinors MY A The vector , where and .
generators MX N , where .
In the source Mathematical meaning
body MX N The source body , a set of minor-coordinate vectors.
... ∈ body MX N The conclusion : a vector scaled using the target volume belongs to the body formed using the source norm.

Exact definitions used in this reading: Signed generator set; Convex-body definition.

Exact surrounding binder context (separate excerpts)

Exact source lines 15–18:

noncomputable section
open Set Metric Function MeasureTheory
open scoped NNReal ENNReal BigOperators
namespace MathlibAnnex.PluckerBody

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

Exact content identity

Declaration: MathlibAnnex.PluckerBody.normalizedGenerator_mem_of_sphereIsometry

Accepted content SHA-256: d0157f88f3d702b5365e3797e3b8a11c8764945986637091085e6fd4585ebec1

Accepted source guide SHA-256: bb5e9ff6f537f5d87b15ac86e9a8f0a428a9316f1dd69f711ce424e2ef96083b

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑