MATHLIBANNEX / CANONICAL DECLARATION CARD

The transported Jacobian sign has zero weak gradient

MathlibAnnex.BilipschitzOrientation.weakDivergenceZero_targetJacobianSign

theorem

Uses signed transfer and weak Piola with the same test field to obtain the weak equation on the target.

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 .

Define the source sign and its transport by In particular, a zero determinant gives sign , and for every .

Let be a vector field that vanishes outside a compact set . Its divergence is . With denoting Lebesgue measure, The assertion holds for every such and .

Assumptions

The test field is on all of , and its chosen compact set satisfies and on . Neither connectedness nor finite measure 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 scalar function has zero weak gradient on : its product with the divergence of every admissible test field has integral zero. This is the integral formulation of a weak equation for a scalar function, not the divergence of a vector-valued sign.

Compactness is imposed on a set outside which the test field vanishes, not on the open set . The statement itself does not require or assert that the sign is constant.

Proof route

The divergence of the test field is integrable. Substitute this function into signed transfer; the resulting source integral is zero by weak Piola.

Proof steps

  1. Verify integrability of the observable. Put . Then

    Indeed, is continuous because is , and it vanishes off because vanishes locally there. Its trace is therefore continuous and zero off the compact set . This is integrability of the compact-field divergence, applied to this same and . In particular, .

  2. Insert the observable into the two integral identities. The complete substitution is

    The second line is signed transfer with the maps , the sets , and the observable ; Step 1 supplies its integrability hypothesis. The last equality is weak Piola for the same and the inclusion . Since and were arbitrary, the weak equation follows.

Main citations

Lean source signature (exact)

theorem weakDivergenceZero_targetJacobianSign {n : ℕ}
    (D : BiLipschitzOpenData n) :
    WeakDivergenceZero volume D.target (targetJacobianSign D)
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.
In the source Mathematical meaning
targetJacobianSign D The scalar function , where and for , for . Zero has sign under the cited definitions.
WeakDivergenceZero volume D.target (targetJacobianSign D) The complete conclusion is the scalar predicate for every global test field with a compact carrier . volume is . It does not take an ordinary divergence of .
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.weakDivergenceZero_targetJacobianSign

Accepted content SHA-256: 4c3f7d4ed1c2ead75b23d6380f07535eb5fc21fb74de4b8b7e4f913aee4411d8

Accepted source guide SHA-256: 64c0658743eb29f824c419c2cc8ad85c03e2fa02e241a7b69b3e1b87a6c4519c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑