MATHLIBANNEX / CANONICAL DECLARATION CARD

A component flux gives a determinant difference

MathlibAnnex.Piola.divergence_componentFlux_eq_det_sub

theorem

Expresses the change from one output-coordinate perturbation as a divergence.

Statement

Let be , let be , and fix . Let be the th standard coordinate vector and let denote an arbitrary real matrix. Write and Define the perturbed map and its flux by Then, for every ,

Assumptions

The differentiability assumptions are exactly on and on . The row and point are arbitrary. Compact support and invertibility are not required for this pointwise identity.

Conclusion

The determinant increment is the divergence of the explicitly defined vector field . If has compact topological support, then so does : with , one has . This separate support consequence is what permits the subsequent integration.

Notes

Only the th output coordinate changes, so only row of the derivative matrix changes. The row convention for the cofactor is essential to the identity.

Proof route

Apply the product rule, cancel the cofactor divergence by Piola, and recognize the remaining sum as a row-replacement determinant.

Proof steps

  1. Put and let be the row with entries . Coordinate vectors satisfy , and determinant multilinearity in one row consequently gives

    The finite-sum row-expansion lemmas justify this identity without an invertibility assumption.

  2. The cofactor field is : it is a polynomial in the entries of , which is because is . The product derivative is therefore valid, and Piola supplies its zero term:

  3. Differentiation gives , whose row is and whose other rows agree with . By linearity in that row,

    Subtract and insert the previous expression for the divergence. For the later support assertion, implies , so the support of is contained in that of ; taking closures preserves the inclusion.

Main citations

Lean source signature (exact)

theorem divergence_componentFlux_eq_det_sub
    {n : ℕ} {g : (Fin n → ℝ) → (Fin n → ℝ)} {φ : (Fin n → ℝ) → ℝ}
    (hg : ContDiff ℝ 2 g) (hφ : ContDiff ℝ 1 φ)
    (i : Fin n) (x : (Fin n → ℝ)) :
    ∑ j, fderiv ℝ (componentFlux g φ i) x (Pi.single j 1) j =
      LinearMap.det ((fderiv ℝ (singleOutputPerturb g φ i) x).toLinearMap) -
        LinearMap.det ((fderiv ℝ g x).toLinearMap)
In the source Mathematical meaning
{g : (Fin n → ℝ) → (Fin n → ℝ)} {φ : (Fin n → ℝ) → ℝ} The vector map and scalar function .
(hg : ContDiff ℝ 2 g) (hφ : ContDiff ℝ 1 φ) (i : Fin n) (x : (Fin n → ℝ)) The assumptions are , , with fixed output row and arbitrary point . No support condition is imposed.
componentFlux g φ i The vector field , whose scalar components are .
∑ j, fderiv ℝ (componentFlux g φ i) x (Pi.single j 1) j The divergence . The derivative acts on the whole vector field before its th component is taken.
In the source Mathematical meaning
singleOutputPerturb g φ i The perturbed vector map , defined in the cited declaration.
LinearMap.det ((fderiv ℝ (singleOutputPerturb g φ i) x).toLinearMap) - LinearMap.det ((fderiv ℝ g x).toLinearMap) The determinant increment . Forgetting the continuity certificate of a derivative does not change its linear map. This is the complete right side of the divergence identity.
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.divergence_componentFlux_eq_det_sub

Accepted content SHA-256: 3cc9f8af908a62b6ffc37136c15eb3dfc455e4e7c035797703b06f063709005d

Accepted source guide SHA-256: 3395ad2e21acce2f08cab3a89d044343b4013e2c6fa5cf7128e7da416be2afdb

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑