MATHLIBANNEX / CANONICAL DECLARATION CARD

Signed transfer from the absolute Jacobian formula

MathlibAnnex.BilipschitzOrientation.signed_area_transfer

theorem

Transfers an integrable function without first assuming that the Jacobian sign is constant.

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 .

All integrals use Lebesgue measure on these fixed coordinates. Let be integrable on . Then

Assumptions

The integrability hypothesis is . No connectedness assumption is made on or .

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 factor on the target is the sign of the source Jacobian evaluated at the inverse point . It may vary with . Both integrands are integrable on their respective sets.

The total derivative is measurable, its determinant is measurable, and the displayed two-valued sign is measurable. Since is continuous, is measurable as well. These facts justify the integrability assertion for used in the proof. The two global Lipschitz constants are exactly those supplied for and in the assumptions.

Proof route

Discard a null subset of and a null subset of , apply the injective absolute area formula, and use to restore the signed determinant.

Proof steps

  1. Identify the two null complements. Define

    Then

    The first equality is Rademacher’s theorem for the globally Lipschitz map on the finite-dimensional space . The second follows from . The third is preservation of null sets by an equal-dimensional Lipschitz map, with this same and ; it is also recorded by the target-exception lemma. The set is measurable because and the differentiability set are measurable.

    The inverse identities give

    Indeed, if , then and . Hence , so and .

  2. Apply the absolute formula to the signed function. Put . The sign is measurable and , so is integrable on and on . The formula to be used is

    For the injective absolute Jacobian formula, the domain is the measurable set , the map is , the derivative at each is (also a derivative within ), and the measure is . Injectivity on follows from on . With these same inputs, the corresponding integrability equivalence gives integrability of the right-hand integrand.

  3. Substitute the inverse and remove the null complements. For ,

    The second identity is the signed determinant identity at this differentiability point. Therefore

    Substituting this equality into Step 2 and using the null complements from Step 1 gives

    The first and last replacements are justified by and , respectively. The source integrability obtained in Step 2 is preserved by the first replacement.

Main citations

Lean source signature (exact)

theorem signed_area_transfer {n : ℕ} (D : BiLipschitzOpenData n)
    {φ : (Fin n → ℝ) → ℝ} (_hφ : IntegrableOn φ D.target) :
    ∫ x in D.source, φ (D.f x) * (fderiv ℝ D.f x).det ∂volume =
      ∫ y in D.target, φ y * targetJacobianSign D y ∂volume
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.
{φ : (Fin n → ℝ) → ℝ} (_hφ : IntegrableOn φ D.target) The scalar weight is integrable on for Lebesgue measure. The underscore in the hypothesis name does not remove this assumption.
(fderiv ℝ D.f x).det The signed Jacobian , with the total derivative convention stated in the body.
targetJacobianSign D The scalar function , where and for , for . Zero has sign under the cited definitions.
In the source Mathematical meaning
∫ x in D.source, φ (D.f x) * (fderiv ℝ D.f x).det ∂volume The source integral , with fixed coordinate Lebesgue measure .
∫ y in D.target, φ y * targetJacobianSign D y ∂volume The equal target integral . Both the weight and transported sign are evaluated at the same .
Exact surrounding binder context (separate excerpts)

Exact source lines 23–29:

noncomputable section

open Set MeasureTheory Filter
open scoped 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.signed_area_transfer

Accepted content SHA-256: 8abd331b0ff7b7ac74b238db75a3acf83fcbc42fa739d87353c82fce262d9802

Accepted source guide SHA-256: 3aca907950df5947776741b663d8284043b940fd54d211c7f3444e187ab27b5e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑