MATHLIBANNEX / CANONICAL DECLARATION CARD

A common orientation sign for the radial derivative average

MathlibAnnex.Plucker.derivativeAverage_comp_linear_radial

theorem

Identifies the whole minor vector using one signed Jacobian integral.

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. Also put and .

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

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 any linear map and put . For a function , write for its Fréchet derivative where it exists and for the zero linear map otherwise. Define and . Then there is one sign such that

Assumptions

The dimension is positive: . Both and are continuous seminorms with the displayed positive norm comparisons. The sphere map is a bijective chord-distance isometry. The map is arbitrary linear; there is no contraction assumption on it. The output dimension may be zero.

Conclusion

One scalar sign works for the full vector, including all selected minors. If , the vector identity is in the one-element empty-coordinate space; the same scalar construction still applies.

Notes

The derivative and every integral use the fixed sup-norm coordinates and reference Lebesgue measure. The sign is not chosen independently for individual minors.

Proof route

Use signed orientation on open balls, compute linear-composition minors, and cancel the average normalization.

Proof steps

  1. Supply the signed-Jacobian inputs. Use the same radial map and its inverse . The radial norm and inverse identities give

    The global reference-norm bounds are

    These follow from the -Lipschitz radial estimate in the model norms and the positive comparison bounds. The same identities map onto , with inverse . Both sets are open; is convex and contains zero, hence is preconnected and has positive measure. Also , so its measure is finite. The exact radial input construction records these inputs.

    Write for the derivative of where it exists and for zero otherwise, and set . Apply the signed Jacobian integral theorem with source , target , forward map , inverse , and the bounds just displayed. It supplies one sign and

    For the last equality, the relevant boundary and measure identities are

    The null-sphere lemma identifies the sphere with the boundary of the convex open ball and proves that it is null. The open/closed ball-volume identity gives the last equality. No absolute determinant is substituted.

  2. Compute every minor with the same inner determinant. At a differentiability point of ,

    Selecting rows commutes with multiplication by the square matrix ; determinant multiplicativity then proves the second equality. The exact linear-composition identity gives

    The global Lipschitz bound on gives differentiability almost everywhere. The linear map is Lipschitz, so is Lipschitz. Compact-set integrability of derivative generators applied to on makes the vector integrable. Apply the same result to on , and let be the all-row index. Its determinant coordinate gives

    Coordinate projection and multiplication by the finite constant preserve integrability. Thus both the scalar integral and the vector coordinates used below are justified.

  3. Cancel the normalization and insert the one sign. For every ,

    The first two equalities use integrability and . The third discards exactly , whose measure is zero by The null-sphere lemma. The coordinate radial-average theorem records those first three lines; the last substitutes the signed integral from Step 1. The sign was chosen before any row index, so it is common to every coordinate. Reassembling the vector gives .

Main citations

Lean source signature (exact)

/-- The full radial average is exactly one orientation sign times the target
generator. No contraction hypothesis on the linear map is introduced. -/
theorem derivativeAverage_comp_linear_radial {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 → ℝ)) :
    ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧
      derivativeAverage MX (fun x => A (show Fin (m + 1) → ℝ from
        radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x))) =
        ε • Matrix.ballVolumeScaledMaximalMinors MY A

The inputs specify two norms, a sphere isometry and an arbitrary linear map. The conclusion is an existence statement about a single sign.

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 ; no contraction inequality is assumed.
show Space MX from x The same coordinate vector , regarded as having norm .
radialExtension (X := Space MX) (Y := Space MY) Δ The map , with and for . The named arguments specify the source norm and target norm .
show Fin (m + 1) → ℝ from ... Read the resulting vector in the original sup-norm coordinates. No additional mathematical map is applied.
fun x => A (...) The entire function , ; means .
derivativeAverage MX (...) , where and . The derivative is read in the reference coordinates, with zero at nondifferentiability points.
Matrix.ballVolumeScaledMaximalMinors MY A , where and .
In the source Mathematical meaning
∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧ ... There exists a real ε with or , and the following vector equality holds for that same sign. Here means “or” and means “and”.
... = ε • Matrix.ballVolumeScaledMaximalMinors MY A . The dot multiplies every minor coordinate by the one scalar .

Exact definitions used in this reading: Set-average definition. The mathematical proof keeps and for these same radial maps. Its signed integrand is distinct from the absolute integrand used in the absolute-area Card. The single output sign is shared by all minor coordinates.

Exact surrounding binder context (separate excerpts)

Exact source lines 16–19:

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

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

Exact content identity

Declaration: MathlibAnnex.Plucker.derivativeAverage_comp_linear_radial

Accepted content SHA-256: 0e7ea02ecc81f88e0f8ec2c926430d384d7e72de01feb5d2563920f636facc9b

Accepted source guide SHA-256: 9bd09b5ac6b436fd4a74c33f8f6759541be90735a9ec39b3c044e1dd14fb8b64

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑