MATHLIBANNEX / CANONICAL DECLARATION CARD

The average of contractive derivative generators lies in the body

MathlibAnnex.Plucker.derivativeAverage_mem_body

theorem

Uses closed-convex average membership for the actual derivative-generator function.

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

For a 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 .

Suppose and Then .

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 derivative bound holds in all directions simultaneously for almost every point of . Integrability of the vector is the other explicit hypothesis. Global Lipschitzness and everywhere differentiability are not 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 normalized vector average belongs to , with no extra multiplication by ball volume.

Proof route

Use the derivative as a contraction witness, then average in the closed convex body.

Proof steps

  1. Obtain almost-everywhere membership. At every point satisfying the derivative bound, and hence

    The positive-generator lemma takes this very derivative as its witness. Applied on the given full-measure set, it proves the displayed membership almost everywhere.

  2. Supply every average hypothesis. The input function is , the integration set is , and the receiving set is . We have

    The body is convex by definition. Compactness of the generators and compactness of their finite-dimensional convex hull make it closed. Apply the closed-convex set-average theorem to these inputs. It gives

    The left side is exactly by its definition.

Main citations

Lean source signature (exact)

/-- The average of integrable, almost everywhere contractive derivative
generators belongs to the model Plücker body. -/
theorem derivativeAverage_mem_body {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))
    {f : (Fin n → ℝ) → (Fin N → ℝ)}
    (hcontract : ∀ᵐ x ∂volume.restrict M.closedUnitBall,
      M.IsContraction (fderiv ℝ f x))
    (hint : IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume) :
    derivativeAverage M f ∈ PluckerBody.body M N

The named arguments hcontract and hint are assumptions. The expression after the final colon is the conclusion.

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 .
{f : ... → ...} An arbitrary function ; braces let Lean infer it from the other inputs.
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 .
hcontract : ∀ᵐ x ∂volume.restrict M.closedUnitBall, M.IsContraction (fderiv ℝ f x) Outside one Lebesgue-null subset of , for every . Here ᵐ means “for almost every”, and restricts to .
hint : IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume is Lebesgue-integrable on : it is measurable up to a null set and .
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.
In the source Mathematical meaning
derivativeAverage M f The vector , not the average of the linear maps .
derivativeAverage M f ∈ PluckerBody.body M N The conclusion ; means membership of this vector in this set.

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 13–18:

noncomputable section

open Set MeasureTheory
open scoped BigOperators ENNReal

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_mem_body

Accepted content SHA-256: 972810f9ab58287a3c528b4adfe340f672f47ba5ac106d8463be219ca8c1a253

Accepted source guide SHA-256: 36ef8b6dfa04bf0147839ef1b87122dcac2dc1fbf2b3cd685338bdb30c5b8bb1

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑