MATHLIBANNEX / CANONICAL DECLARATION CARD

Maximal-minor integral differences for Lipschitz perturbations

MathlibAnnex.NullLagrangian.integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith

theorem

Passes the smooth compact-perturbation identity to Lipschitz maps through local strong convergence.

Statement

Fix and be globally Lipschitz, with compactly supported. Fix a set of output indices . Define and the signed selected minor Then

Assumptions

There are finite constants such that, for all , The support convention is , and only this set must be compact. The fixed selection consists of distinct output coordinates in increasing order, so its existence entails . Differentiability everywhere and a boundary condition are not assumed.

Conclusion

The same signed minor occurs in both terms, and their difference is integrable with integral zero. No absolute value is placed around either determinant, and separate whole-space integrability of the two minors is not claimed.

The coordinate projection is contractive for the sup norms. Postcomposition is a continuous linear map on operator spaces, preserves subtraction, and has norm at most one. Its determinant equals the maximal minor of the standard matrix in precisely the increasing row order.

Proof route

Smooth both maps, use one compact set for all small-parameter perturbations, pass each restricted determinant integral to the limit, and finally identify the whole-space difference.

Proof steps
  1. The support lemma provides a compact containing and also for every sufficiently small positive . Lipschitz maps are locally integrable, so mollification is linear: . These mollifications are . Apply the smooth compact-perturbation theorem to and ; output selection preserves compact support. The chain rule identifies their derivatives with selected square operators and gives

  2. Outside , is locally zero. The two maps then agree on a neighborhood, so their derivatives, and thus their selected minors, agree there. The previous integral therefore equals its restriction to . This argument only needs local equality; it does not require differentiability of the unsmoothed maps at every point.

  3. Apply strong local convergence of mollified derivatives to and to , on this same compact . For , contractivity and linearity give

    Continuous linear postcomposition preserves eventual membership; the limiting derivative belongs to by its Lipschitz bound. Thus all hypotheses of determinant-integral continuity hold with measure restricted to . Its output is for each of these two maps.

  4. The smooth selected minors are integrable on compact . For the limiting maps , the bound and give the same integrability. Thus both terms may be integrated separately on . Using Step 3 for each term,

    This proves the restricted difference integral is zero; it does not subtract unrestricted whole-space integrals.

  5. Outside , the original perturbation is locally zero, so there as well. The difference is integrable on and equals zero outside; it is therefore integrable on the whole space and has the same integral. This proves the asserted whole-space identity without requiring mollification to preserve any boundary values.

Main citations

Lean source signature (exact)

theorem integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith
    {m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))
    {g u : (Fin (m + 1) → ℝ) → (Fin N → ℝ)}
    {Cg Cu : ℝ≥0} (hg : LipschitzWith Cg g) (hu : LipschitzWith Cu u) (huc : HasCompactSupport u) :
    ∫ x, (maximalMinorIntegrand s (fun y => g y + u y) x -
      maximalMinorIntegrand s g x) = 0
In the source Mathematical meaning
{m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N)) The domain dimension and fixed increasingly ordered selection of output coordinates.
{g u : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} The base map and perturbation from to , with sup norms.
{Cg Cu : ℝ≥0} (hg : LipschitzWith Cg g) (hu : LipschitzWith Cu u) The global bounds and for all , with nonnegative constants.
(huc : HasCompactSupport u) The perturbation has compact support .
In the source Mathematical meaning
maximalMinorIntegrand s (fun y => g y + u y) x - maximalMinorIntegrand s g x The signed difference , where and .
∫ x, (maximalMinorIntegrand s (fun y => g y + u y) x - maximalMinorIntegrand s g x) = 0 The whole-space Lebesgue integral of this difference equals zero. The same increasing selection occurs in both terms, without absolute values.
Exact surrounding binder context (separate excerpt)
noncomputable section
open Set MeasureTheory Filter
open scoped BigOperators Topology ENNReal NNReal
namespace MathlibAnnex
namespace NullLagrangian
Exact content identity

Declaration: MathlibAnnex.NullLagrangian.integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith

Accepted content SHA-256: 633190ad10fc198b21cc65efb19b0cb7005ec47f94d93528baa9aa946cfd1d58

Accepted source guide SHA-256: e27e54b001d5707a6f62e402d4543bd8359472c1f4b062b9dfe9751a21307c65

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑