MATHLIBANNEX / CANONICAL DECLARATION CARD

The divergence-free cofactor identity

MathlibAnnex.Piola.divergence_cofactorRowField_eq_zero

theorem

Cancels the Hessian terms that arise when differentiating a cofactor row.

Statement

Let be , and fix . Let be the th standard coordinate vector, with coordinates . Define the scalar coordinate maps and the derivative matrix by Thus rows are output coordinates and columns are differentiation directions. Let be the fixed th cofactor row field: Then, at every ,

Assumptions

The hypothesis is twice continuous differentiability on the whole coordinate space. There is no invertibility, compact-support, or boundary assumption. A row is supplied; the zero-dimensional case consequently has no row to check.

Conclusion

Every cofactor row field of the derivative is divergence-free, pointwise. The input and output coordinate indices remain distinct in the cancellation below.

Notes

Here and are scalar functions, whereas and are vector-valued maps. For any vector field , . Thus taking the derivative in direction and then taking coordinate is precisely the th term in the divergence.

Proof route

Differentiate one coordinate first. Rowwise differentiation and row multilinearity express it using . In the divergence sum, the terms indexed by and cancel: their second derivatives agree and their two-row determinants have opposite signs.

Proof steps

  1. Differentiate one cofactor coordinate, not the whole divergence at once. Write the th row of as

    For fixed ,

    Only the rows with vary. The finite product rule in the determinant expansion therefore gives

    This is the rowwise derivative formula: each summand differentiates just one nonconstant row. The assumption makes every row being differentiated a map.

  2. Expand the differentiated row and then take the divergence. The coordinate row satisfies

    Define, displaying both replaced rows,

    Linearity of the determinant in row turns Step 1 into

    Finally sum over and reorder these finite sums:

  3. Identify the two symmetries. For each fixed , equality of mixed second derivatives gives

    The matrices and differ by interchanging rows and : these rows are in the first and in the second. Hence

    For , the two rows coincide and each determinant is zero. There is no matrix-invertibility hypothesis in either step.

  4. Perform the cancellation. For a fixed , call the inner finite sum . Relabel and , and then use Step 3:

    Thus over , so . Substitution into Step 2 gives .

Main citations

Lean source signature (exact)

theorem divergence_cofactorRowField_eq_zero
    {n : ℕ} {H : (Fin n → ℝ) → (Fin n → ℝ)}
    (hH : ContDiff ℝ 2 H) (i : Fin n) (x : (Fin n → ℝ)) :
    ∑ j, fderiv ℝ (cofactorRowField H i) x (Pi.single j 1) j = 0
In the source Mathematical meaning
{n : ℕ} {H : (Fin n → ℝ) → (Fin n → ℝ)} (hH : ContDiff ℝ 2 H) The map is on the whole space.
(i : Fin n) (x : (Fin n → ℝ)) The fixed cofactor row and arbitrary evaluation point .
cofactorRowField H i The vector field , with derivative matrix entries : output index , input direction .
Pi.single j 1 The standard direction , with coordinates .
In the source Mathematical meaning
fderiv ℝ (cofactorRowField H i) x (Pi.single j 1) j Differentiate the vector field in direction , then take its th output coordinate: .
∑ j, fderiv ℝ (cofactorRowField H i) x (Pi.single j 1) j = 0 The conclusion is the pointwise identity .
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set
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_cofactorRowField_eq_zero

Accepted content SHA-256: e586a6536e27c03ab4425c4b10c551655da32a43be1170c424c4b06bb2f20a4d

Accepted source guide SHA-256: cca27385be48b2092fc739c16a4889a53b2d3d714458b0ba9aa893468bfe29d2

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑