MATHLIBANNEX / CANONICAL DECLARATION CARD

One boundary extension with all five analytic properties

MathlibAnnex.Plucker.exists_extension_with_derivativeAverage_mem

theorem

Keeps boundary agreement, contraction, derivative control, integrability and average membership on one witness.

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. The boundary is the unit sphere .

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

For any function , write for its Fréchet derivative where it exists and for the zero linear map otherwise. Write for its derivative-generator function and for the average of that function over . The integrand and normalization are The integrals use the fixed reference measure, even when distances are measured with .

Let satisfy for all . There is one function with all five properties:

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 boundary map is -Lipschitz for the -distance and the coordinate sup norm on . No differentiability of , nonempty sphere, or positive dimension is required. 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

The single extension satisfies the displayed five properties simultaneously. Its average is taken over with reference Lebesgue measure. This asserts existence of a common witness, not uniqueness.

The radial extension of a sphere isometry is a separate construction. This theorem does not identify its witness with a radial map.

Proof route

Extend coordinatewise in the induced norm, return to reference coordinates, then derive the remaining properties for that same function.

Proof steps

  1. Construct an extension in the correct metric. On the same vectors of , use the distance . If is empty, take . Otherwise write for coordinate of and, for , use

    Fix . The boundary Lipschitz inequality and the triangle inequality give, for every ,

    The infimum is finite: this is a lower bound, and gives a finite upper bound. For and ,

    Taking the infimum in the first inequality yields . For any , the triangle inequality in the defining formula gives

    The second bound follows by also interchanging and . Hence the coordinate map satisfies

    For the target is the zero space and these assertions still hold, without taking a maximum of an empty family. The scalar McShane construction and its finite-coordinate version prove precisely these extension properties. The source theorem chooses a witness of that result; all following steps use that one , read in the original reference coordinates.

  2. Pass this same extension to its derivative. The first output gives

    The reference-norm Lipschitz conversion supplies a global -Lipschitz bound. Apply the almost-everywhere directional bound with the same , seminorm , upper constant , and restricting set . Its output is the third property, for all , almost everywhere on .

  3. Prove integrability for this witness. Let bound the compact generator set . The derivative bound just obtained gives

    The total derivative is measurable; continuous volume-scaled minors make this finite-coordinate vector strongly measurable. Compactness of the signed generators supplies , and the ball has finite measure. These are the actual inputs of integrability under the seminorm increment bound, which yields the fourth property for the same .

  4. Average without changing the witness. We now have

    Apply derivative-average membership to exactly these two outputs. It gives . Together with the two extension properties in Step 1, this is one existential witness with all five conclusions.

Main citations

Lean source signature (exact)

/-- Every seminorm-Lipschitz boundary map has an extension with its prescribed
trace, almost everywhere contractive derivative, integrable derivative
generator, and derivative average in the Plücker body. -/
theorem exists_extension_with_derivativeAverage_mem {n N : ℕ}
    (M : EquivalentSeminorm (Fin n → ℝ)) (g : M.unitSphere → (Fin N → ℝ))
    (hg : ∀ u v, ‖g u - g v‖ ≤ M.p ((u : Fin n → ℝ) - (v : Fin n → ℝ))) :
    ∃ f : (Fin n → ℝ) → (Fin N → ℝ),
      (∀ x y, ‖f x - f y‖ ≤ M.p (x - y)) ∧
      (∀ u : M.unitSphere, f u = g u) ∧
      (∀ᵐ x ∂volume.restrict M.closedUnitBall, M.IsContraction (fderiv ℝ f x)) ∧
      IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume ∧
      derivativeAverage M f ∈ PluckerBody.body M N

Before the final colon, M, g and hg are inputs. After it, ∃ f says that there exists one function satisfying all five clauses joined by ∧ (“and”).

In the source Mathematical meaning
{n N : ℕ} Arbitrary nonnegative integers . Braces mean that Lean may infer these parameters; they are not extra assumptions.
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 .
M.unitSphere The unit sphere .
g : M.unitSphere → (Fin N → ℝ) The given boundary map . The source calls it , while the mathematical text calls it .
(u : Fin n → ℝ); f u Regard the sphere point as the same coordinate vector in ; hence means .
hg : ∀ u v, ‖g u - g v‖ ≤ M.p (...) The boundary hypothesis for all .
M.closedUnitBall; M.closedUnitBallVolume and , with the finite measure read as a real number.
fderiv ℝ f x The real Fréchet derivative , with the zero linear map used when is not differentiable at .
derivativeGenerator M f x The vector ; its coordinate is .
generators M N The set . Its elements are minor-coordinate vectors, not the maps .
PluckerBody.body M N : all finite convex combinations of the signed vectors in the generator set just described.
derivativeAverage M f The vector , not the average of the linear maps .

The five output clauses, in their source order, mean:

In the source Mathematical meaning
∀ x y, ‖f x - f y‖ ≤ M.p (x - y) for every .
∀ u : M.unitSphere, f u = g u for every .
∀ᵐ x ∂volume.restrict M.closedUnitBall, M.IsContraction (fderiv ℝ f x) For Lebesgue-almost every , for every direction . The exceptional null set does not depend on .
In the source Mathematical meaning
IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume The same is measurable up to a null set on and .
derivativeAverage M f ∈ PluckerBody.body M N The same extension satisfies .

Here ∀ᵐ means “for almost every”, volume.restrict M.closedUnitBall is restricted to , and ∈ is set membership. These five lines are conclusions about the chosen , not hypotheses imposed on the original boundary map .

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

Exact surrounding binder context (separate excerpts)

Exact source lines 14–19:

noncomputable section

open Set MeasureTheory
open MathlibAnnex.EquivalentSeminorm

namespace MathlibAnnex.Plucker

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

Exact content identity

Declaration: MathlibAnnex.Plucker.exists_extension_with_derivativeAverage_mem

Accepted content SHA-256: 9880f3b568c873c74b81a9bb3688a98b29fb5dc53016872a2a1b71df9af71736

Accepted source guide SHA-256: 9083fd3b3ec1ac4401c7b1797cae71b933f8e92cac393b94f84e98594a6d25d9

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑