MATHLIBANNEX / CANONICAL DECLARATION CARD

The signed Jacobian integral is a sign times target volume

MathlibAnnex.BilipschitzOrientation.integral_det_fderiv_eq_signed_volume

theorem

Uses preconnectedness to obtain a constant, positive measure to identify its sign, and finite measure to integrate it.

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

Assume that is preconnected (it has no separation into two nonempty relatively open subsets) and that its Lebesgue measure satisfies .

Write for the Fréchet derivative of at when it exists, and set at other points. Define the signed Jacobian by . Then there exists such that Here the finite measure is identified with its real value, so this is an equality of real numbers.

Assumptions

The target is preconnected, has positive Lebesgue measure, and has finite Lebesgue measure: These conditions are additional to openness and the following inverse and global metric assumptions.

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 is either or . The sign is obtained from the maps; it is not fixed in advance.

The proof uses the three target hypotheses at different stages: preconnectedness gives an almost-everywhere constant, positive measure identifies its value as a sign, and finite measure permits integration of that constant.

Proof route

Identify the almost-everywhere constant value of the transported sign at a point outside its null exceptional set. Then substitute the constant function into signed transfer.

Proof steps

  1. Obtain a constant and identify its value. Define

    By constancy of the transported sign, applied with the assumed preconnectedness of , there is for which the set

    satisfies . Since , choose . Then

    This is the positive-measure sign-identification lemma with the same almost-everywhere equality and the hypothesis . Put .

  2. Integrate using finite target measure. The relevant integrability calculation is

    Thus the observable satisfies the hypothesis of signed transfer. With the same maps and sets, that formula and Step 1 give

    The replacement of by uses . The final integral is finite because has finite measure.

Main citations

Lean source signature (exact)

theorem integral_det_fderiv_eq_signed_volume {n : ℕ}
    (D : BiLipschitzOpenData n) (hpre : IsPreconnected D.target)
    (hpos : 0 < volume D.target) (hfinite : volume D.target ≠ ∞) :
    ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧
      ∫ x in D.source, (fderiv ℝ D.f x).det ∂volume =
        ε * (volume D.target).toReal
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.
(hpre : IsPreconnected D.target) The separate target preconnectedness assumption.
(hpos : 0 < volume D.target) The positive-measure assumption , used to identify an a.e. constant with one of the two sign values.
(hfinite : volume D.target ≠ ∞) The separate finite-measure assumption , used for integrability of the constant target weight.
∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧ The conclusion chooses one real sign ; it is not a prescribed input.
In the source Mathematical meaning
∫ x in D.source, (fderiv ℝ D.f x).det ∂volume The real integral of the signed Jacobian of .
ε * (volume D.target).toReal The equal real quantity . Finiteness identifies the extended measure with its real value; this conversion is confined to the source expression.
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.integral_det_fderiv_eq_signed_volume

Accepted content SHA-256: f17cc47db523e628895b64c4138c01c916cd3b2cfaafb433e0e9f4993475de29

Accepted source guide SHA-256: d67ae7011cb95787bfef811e676e9a8d30b2f96d1175d1c5c57190cc8f907e54

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑