MATHLIBANNEX / CANONICAL DECLARATION CARD

The absolute Jacobian integral of a radial sphere extension

MathlibAnnex.Sphere.radialExtension_integral_abs_det

theorem

Identifies the integral of the absolute Jacobian over an open source unit ball with the volume of the closed target unit ball.

Statement

Let , put , and let have its standard sup norm and Lebesgue measure . Let be continuous seminorms on with specified positive constants satisfying The lower bounds make and norms. Define their unit spheres by and . Let be a bijection satisfying Its radial extension, read as a map in the fixed coordinates, is For , the normalized vector belongs to , so this expression is defined. Put At a differentiability point , let be the Fréchet derivative and set At other points set . Thus is the absolute Jacobian, not a norm of or a determinant of the nonlinear map itself. Then where the finite measure on the right is identified with its real value.

Assumptions

The dimension is the positive integer . The maps defining and are continuous seminorms with the displayed positive comparison bounds. The sphere map is a bijective isometry for the distances induced by and .

The derivative and the measure in the integral use the fixed coordinate space , whereas the unit spheres use and . No linearity or everywhere differentiability of is assumed.

Conclusion

The left side is the integral of the nonnegative function over the open -unit ball. At a differentiability point, with coordinate vectors and component functions , the integrand is explicitly The right side is the volume of the closed -unit ball in the same coordinates. The theorem uses the absolute Jacobian and does not assert that the radial extension is linear.

Changing from the norm or to the sup norm changes the normed-space structure, not the coordinate vector. The reference Lebesgue normalization remains fixed. At a point without a derivative, the source takes the zero linear map; since , its determinant is zero, exactly matching the definition of above.

Proof route

Prove global Lipschitz control and the exact open-ball image. Apply the nonnegative area formula after removing the null nondifferentiability set, justify the real integral, and use the zero-measure boundary of the target ball.

Proof steps

  1. Control the map and identify its image. Radius preservation and the inverse radial extension give

    In particular, is injective. The radial three-Lipschitz estimate and the comparison bounds give

    This is the reference-coordinate Lipschitz bound for the same . Define the open target ball . The radius identity gives . Conversely, for , take ; then and . Hence

    as stated by the exact open-ball image theorem.

  2. Remove null complements on the source and target. Set

    Then

    The first is Rademacher’s theorem applied to the Lipschitz bound of Step 1. The second is the equal-dimensional Lipschitz null-image theorem for that same map and the null set ; it is recorded in the radial image-exception lemma. The set is measurable. Since is injective and ,

    Thus the omitted target subset is null and .

  3. Apply the nonnegative area formula. Write for the nonnegative extended integral, valued in . The formula is

    Apply the injective nonnegative area formula with measurable domain , map , derivative at each , injectivity from Step 1, and reference Lebesgue measure . Step 2 then yields

    The first equality uses . These are extended nonnegative integrals; real integrability is established next.

  4. Verify integrability of the same integrand. Put . This is compact by the comparison bounds. The integrability estimate is

    For compact-set integrability of Lipschitz derivative minors, use , its reference-coordinate Lipschitz bound, the compact set , and all coordinates in increasing order. The resulting minor is ; taking the absolute value gives . This application is recorded by integrability of the radial absolute determinant. Since , we have .

    Because , its finite extended integral is the same number as its real integral. Taking real values in Step 3 therefore gives

    with the finite measure on the right read as a real number.

  5. Replace the open target ball by the closed ball. The boundary identities are

    The boundary description follows from the norm-ball description; its measure is zero by the convex-set boundary theorem. Both steps are used in the open/closed target-volume lemma. Finiteness follows from compactness of the closed -unit ball. Substitution into Step 4 gives the stated equality

Main citations

Lean source signature (exact)

theorem radialExtension_integral_abs_det {m : ℕ}
    {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}
    (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :
    ∫ x in MX.p.ball 0 1,
      |ContinuousLinearMap.det (fderiv ℝ (fun y : Fin (m + 1) → ℝ =>
        (show Fin (m + 1) → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from y))) x)|
      ∂volume = MY.closedUnitBallVolume
In the source Mathematical meaning
{m : ℕ} {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)} The positive dimension and the two stored seminorms on the fixed sup-norm coordinate space , with the positive comparison bounds stated in this Card.
Space MX; Space MY The same coordinate vectors equipped with norms and . This changes the norm used for sphere distances, not the reference coordinate measure.
(Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) The given bijective isometry , with .
show Space MX from y Regard the same vector with norm ; this is not an additional transformation.
radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from y) The radial value : zero at zero, and otherwise.
show Fin (m + 1) → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from y) Read that same value back in the fixed reference coordinates. The entire function under the derivative is .
ContinuousLinearMap.det (fderiv ℝ (fun y : Fin (m + 1) → ℝ => (show Fin (m + 1) → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from y))) x) The determinant of the derivative of this whole coordinate map. The surrounding absolute-value bars in the signature give .
In the source Mathematical meaning
MX.p.ball 0 1 The open source ball .
∂volume = MY.closedUnitBallVolume The complete equality is , where . The cited volume definition takes the real value of its finite measure. The same reference Lebesgue measure is used throughout.
Exact surrounding binder context (separate excerpts)

Exact source lines 17–21:

noncomputable section
open Set Metric Function MeasureTheory
open scoped NNReal ENNReal
namespace MathlibAnnex.Sphere
open EquivalentSeminorm

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

Exact content identity

Declaration: MathlibAnnex.Sphere.radialExtension_integral_abs_det

Accepted content SHA-256: 56ec5070e1442d28fe4a6cb353623cd07932f03dbb626fb7c9a61afa9531c6a0

Accepted source guide SHA-256: e5c0746e9e0e08f7b2c08e6d46428030523d68af142dee003519e02cdfcc7579

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑