MATHLIBANNEX / CANONICAL DECLARATION CARD

The set average of derivative generators

MathlibAnnex.Plucker.derivativeAverage

def

Separates the volume-scaled integrand from the normalization of its average.

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

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 .

Definition

The separate derivative-generator definition fixes the entire integrand, coordinate by coordinate: The average uses the probability measure , so the multiplier inside the integrand and the normalization outside it are distinct. If is integrable, evaluating a coordinate commutes with integration and gives

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. No Lipschitz, differentiability or integrability condition on is part of this definition. 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 result lies in . Membership in a Plücker body requires additional hypotheses.

Lean uses a total Bochner integral, equal to zero when the vector integrand is not integrable. This convention does not certify integrability. Its total derivative at a nondifferentiability point is zero; the empty determinant when is still .

Main citations

Lean source signature (exact)

/-- The set average of derivative generators over the model closed unit ball. -/
def derivativeAverage {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))
    (f : (Fin n → ℝ) → (Fin N → ℝ)) :
    Matrix.MaximalMinorIndex n (Fin N) → ℝ :=
  ⨍ x in M.closedUnitBall, derivativeGenerator M f x ∂volume

This definition takes an arbitrary function f; it assumes neither differentiability nor integrability.

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 : (Fin n → ℝ) → (Fin N → ℝ) A function . The plain arrow does not assert linearity or continuity.
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.
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 .
volume; ∂volume The fixed reference Lebesgue measure ; the second notation specifies the measure of integration.
In the source Mathematical meaning
⨍ x in M.closedUnitBall, ... ∂volume The set average , with already present inside .
derivativeAverage M f The vector , not the average of the linear maps .

Lean assigns the vector integral the value zero when its integrand is not integrable. The displayed definition is not a claim that this integrability condition holds.

Exact definitions used in this reading: Derivative-generator function.

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

Accepted content SHA-256: ab8c5a421ca98424ccc38a7f916ad67102db45535cf6ffb5824dea08c1af5b00

Accepted source guide SHA-256: 20e17826a5be32466058acb4334a395320dd81c492ee3dbee69d047ce30b084e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑