MATHLIBANNEX / CANONICAL DECLARATION CARD

Weak Piola identity for a compactly supported test field

MathlibAnnex.BilipschitzOrientation.weak_piola

theorem

Uses coordinate perturbations to show that the signed pullback of a test-field divergence has zero integral.

Statement

Let and let have the sup norm . Let be open, and let be globally Lipschitz maps whose restrictions and are mutually inverse. Fix a number such that

Write for the Fréchet derivative of at when it exists, and set at other points. Define the signed Jacobian by .

Let be a vector field, and choose a compact set such that for . Write and define All integrals use Lebesgue measure on these fixed coordinates. Then

Assumptions

The field is continuously differentiable on all of . Its chosen compact set lies in and contains ; need not equal the closure of that set. No second derivative of is assumed.

The sets are open. The inverse and image conditions are The global bounds use specified constants and : The estimates hold on all of , not just on or . The inverse identities are required only on and .

Conclusion

The integral of the signed Jacobian times the pulled-back divergence vanishes. For , the divergence is an empty sum and the conclusion is immediate. In positive dimension the proof below integrates determinant differences produced by compactly supported perturbations.

The argument integrates each determinant difference as one integrable function. It never subtracts two possibly divergent integrals over the whole ambient space. The absolute values in the integrability estimates do not replace the signed determinant in the theorem.

Proof route

For each coordinate, construct a compactly supported perturbation of . Its determinant difference equals one term of the desired integrand. Prove that difference is integrable, use the null-Lagrangian identity to make its integral zero, and sum the coordinate identities.

Proof steps

  1. Obtain a compact preimage and a Lipschitz test field. The relevant identities are

    The derivative vanishes off because the complement of the closed set is open and is identically zero there. Continuity of on the compact set gives a number such that for every . The compact-field Lipschitz lemma applies to this global derivative bound and the field , and yields a global Lipschitz bound for .

    For the preimage identity, the lower metric estimate makes globally injective. If , then , so . Conversely for . This is the exact preimage formula. The set is compact because is continuous.

  2. Define the coordinate perturbations. The case is already settled; write . For , let be the th coordinate vector and let . Define

    The inclusion holds because whenever , and is closed. Hence is compact. The maps , and are Lipschitz, so and are globally Lipschitz. Write for the derivative of where it exists and for the zero linear map otherwise. These are the maps and compact supports used in Step 4.

  3. Calculate the determinant difference. At a point where is differentiable, put and . Then

    The matrix has the identity rows except that row is . Row-linearity gives

    Indeed, a term with has two equal rows, whereas the term is . Thus

    Define, on all of ,

    By Rademacher’s theorem for the globally Lipschitz map , the calculation proves for -almost every .

  4. Prove integrability and apply the null-Lagrangian identity. For the maps and compact set from Step 2,

    The two finite integrals follow from compact-set integrability of derivative minors, applied separately to and on . In dimension , selecting all rows in coordinate order makes the minor the determinant itself. Outside , vanishes on a neighborhood, so there and their total derivatives agree. This is the off-support determinant-difference identity. Consequently,

    The null-Lagrangian output is

    Here the compact-perturbation theorem is applied to these same : both are globally Lipschitz, has compact support, , and the selected minor uses every coordinate in order. Finally, the almost-everywhere equality in Step 3 gives

  5. Restrict to the source set and sum. For , Step 1 gives , and therefore and . Hence

    Using the defining coordinate sum for divergence, we obtain

    The sum may pass through the integral because each is integrable by Step 4.

Main citations

Lean source signature (exact)

theorem weak_piola {n : ℕ} (D : BiLipschitzOpenData n)
    (W : CompactC1VectorField (Fin n → ℝ)) (hW : W.carrier ⊆ D.target) :
    ∫ x in D.source,
      divergence W (D.f x) * (fderiv ℝ D.f x).det ∂volume = 0
In the source Mathematical meaning
(D : BiLipschitzOpenData n) The record described in this Card: open , maps restricting to inverse bijections , global upper Lipschitz bounds , and global lower bound with . The source name D is not the derivative symbol.
D.source; D.target; D.f; D.g The local mathematical objects , respectively, throughout this Card.
(W : CompactC1VectorField (Fin n → ℝ)) The pair consisting of a chosen compact carrier and a global vector field with nonzero set contained in , in the cited test-field type.
(hW : W.carrier ⊆ D.target) The carrier satisfies . It contains the closed support of but need not equal it.
divergence W (D.f x) The pulled-back divergence , where .
In the source Mathematical meaning
(fderiv ℝ D.f x).det The signed Jacobian .
∫ x in D.source, divergence W (D.f x) * (fderiv ℝ D.f x).det ∂volume = 0 The output . Compact perturbations in the proof are auxiliary constructions, not added inputs.
Exact surrounding binder context (separate excerpts)

Exact source lines 19–25:

noncomputable section

open Set MeasureTheory Filter
open scoped BigOperators ENNReal NNReal Topology

namespace MathlibAnnex
namespace BilipschitzOrientation

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

Exact content identity

Declaration: MathlibAnnex.BilipschitzOrientation.weak_piola

Accepted content SHA-256: 0c048dc1cede12ab8b6f85e6951993e567470888327ea3ddcbbfabb5c32a128b

Accepted source guide SHA-256: c47a6385914233bc64b3984cfcd992899a3872ac1e5205c8bce2b871a55ceffa

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑