claimroutine
Green formula on moving total domain
Green formula on the moving domain leaves only a wall flux with full normal
integration by parts behind the flux identity
Statement (paper)
Let be a smooth function compactly supported in the parameter domain, and let be a Hermitian matrix field with divergence-free real columns. Then on the total domain , with near the boundary, smooth and on , one has
where , is the unit outward normal with quaternionic column , and on .
In plain English
For a smooth compactly supported test function and a Hermitian matrix field with divergence-free real columns, equals minus a boundary term over the lateral wall of . Here near the wall with smooth and there, is the quaternionic normal column, and .
Why it's here
This is the integration-by-parts identity on the total space, where the wall moves with , that the proposition rests on. Because the divergence-free columns of kill the interior terms, the only leftover is a wall flux involving the full normal . The later claims apply it with and to get the wall flux term and the full determinant.
Classified routine:
Standard Green/divergence-theorem integration by parts twice, using the divergence-free columns of M (the Piola-type identity for cofactor-like fields) so that only the lateral boundary flux survives; an adaptation of the classical argument to a domain whose wall moves with the parameter z.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §4.3 Cancelling the full determinant
- Page
- —
- Label
—- Line
sections/energy.tex:217
Leannot aligned
Phase 2 aligns this node to a Lean declaration.