MATHLIBANNEX / CANONICAL DECLARATION CARD

Almost-everywhere constancy of the sign on a preconnected target

MathlibAnnex.BilipschitzOrientation.targetJacobianSign_ae_const

theorem

Obtains one constant from the weak equation and preconnectedness of 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

The target is preconnected: it cannot be written as the union of two disjoint, nonempty, relatively open subsets. The empty set is allowed.

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 Lebesgue measure on . Then there exists such that Equivalently, for Lebesgue-almost every .

Assumptions

The target is preconnected: it cannot be written as the union of two disjoint, nonempty, relatively open subsets. The empty set is allowed. This is an explicit hypothesis in addition to openness of . No positive-measure or finite-measure hypothesis is imposed.

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

A single real number agrees with the transported Jacobian sign outside a null subset of . If , every satisfies this equality; this declaration does not constrain that choice to in the empty case.

The pointwise bound supplies local integrability even if has infinite measure. When has positive measure, a chosen almost-everywhere constant can be identified with an actual sign value.

Proof route

The sign is locally integrable and satisfies the zero-weak-gradient equation. Apply the constancy theorem with domain and scalar function , using the explicit preconnectedness hypothesis.

Proof steps

  1. Supply local integrability and the weak equation. Since , every compact set satisfies

    The total derivative is measurable, the determinant and its two-valued sign are measurable, and is continuous. Thus is measurable and locally integrable on , as recorded by local integrability of the transported sign. The absolute-value equality is recorded by the source-sign bound and the transported-sign bound.

    For every vector field that is zero outside a compact subset of , write . Then

    This is the zero-weak-gradient theorem for the same maps, target set and Lebesgue measure.

  2. Apply constancy on this target. The hypotheses now read

    Apply the preconnected-domain constancy theorem with ambient space , Lebesgue measure , open set , and scalar function . Openness and preconnectedness are assumptions; Step 1 supplies local integrability and the weak equation. Its output is

    which is exactly the asserted conclusion. This application allows both and .

Main citations

Lean source signature (exact)

theorem targetJacobianSign_ae_const {n : ℕ}
    (D : BiLipschitzOpenData n) (hpre : IsPreconnected D.target) :
    ∃ c : ℝ, AEConstantOn volume (targetJacobianSign D) D.target c
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.
targetJacobianSign D The scalar function , where and for , for . Zero has sign under the cited definitions.
In the source Mathematical meaning
(hpre : IsPreconnected D.target) The additional input says that is preconnected; it permits and is not stored in the record.
∃ c : ℝ, AEConstantOn volume (targetJacobianSign D) D.target c The output supplies a real with almost everywhere for . This theorem does not return a certificate .
Exact surrounding binder context (separate excerpts)

Exact source lines 19–25:

noncomputable section

open Set MeasureTheory Filter
open scoped BigOperators ENNReal

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.targetJacobianSign_ae_const

Accepted content SHA-256: 66a3ddb7214180414637adb6147bcf1e39e79598327f5cab7379f850f75d28b9

Accepted source guide SHA-256: abf8fd774ca33384b054ab12b0a595ab02009197b7effd1ed1edf9f02540da73

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑