MATHLIBANNEX / CANONICAL DECLARATION CARD

Smooth compact perturbations preserve the determinant integral difference

MathlibAnnex.Piola.integral_det_fderiv_add_sub_eq_zero_of_contDiff

theorem

Builds a finite telescope from single-output perturbations with compactly supported fluxes.

Statement

Fix and let be , with compactly supported. Then

Assumptions

Both maps are smooth of all finite orders, as stated in the exact theorem. Only must have compact support. No decay or global integrability is assumed for or for its determinant separately. Here and below and are scalar coordinate maps. Compact support means that is compact.

Conclusion

The determinant difference is integrable and has integral zero. This statement is an integral of a difference; it does not assert equality of two separately integrable whole-space determinants.

The one-coordinate integral lemma needs only a base map and a compactly supported scalar perturbation. The theorem here retains its stronger stated hypotheses and applies that lemma to each smooth hybrid.

Proof route

Add the components of one at a time, prove each determinant increment integrable with zero integral, and add the finitely many increments.

Proof steps

  1. For , define the smooth hybrid map by its coordinates:

    Then , , and for ,

    Each scalar coordinate is smooth and has compact support, since

  2. Apply the component-flux identity with base , scalar , and row . Smoothness supplies the required and hypotheses. The flux is and compactly supported because its support is contained in that of . The compact-support divergence theorem gives

    This increment is integrable: it is continuous and vanishes outside the compact support of , since there is locally zero and its derivative is zero.

  3. Choose any ordering of the coordinates and write its successive subsets as . Pointwise telescoping gives

    Every summand is integrable by the preceding step. Linearity of the integral is therefore legitimate for this finite sum, and its integral is the sum of zeros. No splitting into the two unrestricted determinant integrals is used.

Main citations

Lean source signature (exact)

theorem integral_det_fderiv_add_sub_eq_zero_of_contDiff
    {m : ℕ} {g u : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}
    (hg : ContDiff ℝ (↑(⊤ : ℕ∞)) g) (hu : ContDiff ℝ (↑(⊤ : ℕ∞)) u)
    (huc : HasCompactSupport u) :
    ∫ x, (LinearMap.det ((fderiv ℝ (fun y => g y + u y) x).toLinearMap) -
      LinearMap.det ((fderiv ℝ g x).toLinearMap)) = 0
In the source Mathematical meaning
{m : ℕ} {g u : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)} The positive dimension , base map and perturbation on .
(hg : ContDiff ℝ (↑(⊤ : ℕ∞)) g) (hu : ContDiff ℝ (↑(⊤ : ℕ∞)) u) Both maps are , meaning continuously differentiable at every finite order.
(huc : HasCompactSupport u) Only is required to have compact support .
fun y => g y + u y The pointwise sum , whose derivative is used in the first determinant.
In the source Mathematical meaning
LinearMap.det ((fderiv ℝ (fun y => g y + u y) x).toLinearMap) - LinearMap.det ((fderiv ℝ g x).toLinearMap) The entire integrand ; these are signed determinants of the same-size derivative maps.
∫ x, (LinearMap.det ((fderiv ℝ (fun y => g y + u y) x).toLinearMap) - LinearMap.det ((fderiv ℝ g x).toLinearMap)) = 0 The conclusion integrates this difference over all with Lebesgue measure and gives zero. It does not assume that the two separate whole-space determinant integrals are finite.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set MeasureTheory Filter
open scoped BigOperators Topology

namespace MathlibAnnex
namespace Piola

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

Exact content identity

Declaration: MathlibAnnex.Piola.integral_det_fderiv_add_sub_eq_zero_of_contDiff

Accepted content SHA-256: a793404962f66d63ae5b1099565e0fcb6b449d11285c7f82cf00c7117b2ef924

Accepted source guide SHA-256: 3b922fceda2d66468f42d46e654bb7524c00fdb0a0f47c4a94db8fad7d5e21f1

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑