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
Claim·§4.3 Cancelling the full determinant·inside propEnergy flux identity with full wall normal

Statement (paper)

Let η=η(z)\eta=\eta(z) be a smooth function compactly supported in the parameter domain, and let MM be a Hermitian matrix field with divergence-free real columns. Then on the total domain Ω\Omega, with u=rρu=r\rho near the boundary, ρ\rho smooth and ρ≥0\rho\ge0 on r=0r=0, one has ∫ΩuMTTΔzη=∫Ωη M:H(u)−∫∂latΩη (ν∗Mν) ∂nu dS, \int_\Omega u M_{TT}\Delta_z\eta=\int_\Omega \eta\,M:H(u)-\int_{\partial_{\rm lat}\Omega}\eta\,(\nu^*M\nu)\,\partial_{\mathbf n}u\dd S, where ∂latΩ={r=0}\partial_{\rm lat}\Omega=\{r=0\}, n=∇r/∣∇r∣\mathbf n=\nabla r/|\nabla r| is the unit outward normal with quaternionic column ν=G(r)/∣∇r∣\nu=G(r)/|\nabla r|, and ∂nu=ρ∣∇r∣\partial_{\mathbf n}u=\rho|\nabla r| on r=0r=0.

In plain English

For a smooth compactly supported test function η(z)\eta(z) and a Hermitian matrix field MM with divergence-free real columns, ∫ΩuMTTΔzη\int_\Omega u M_{TT}\Delta_z\eta equals ∫Ωη M:H(u)\int_\Omega \eta\, M:H(u) minus a boundary term over the lateral wall {r=0}\{r=0\} of η(ν∗Mν)∂nu\eta(\nu^*M\nu)\partial_{\mathbf n}u. Here u=rρu=r\rho near the wall with ρ\rho smooth and ρ≥0\rho\ge0 there, ν=G(r)/∣∇r∣\nu=G(r)/|\nabla r| is the quaternionic normal column, and ∂nu=ρ∣∇r∣\partial_{\mathbf n}u=\rho|\nabla r|.

Why it's here

This is the integration-by-parts identity on the total space, where the wall moves with zz, that the proposition rests on. Because the divergence-free columns of MM kill the interior terms, the only leftover is a wall flux involving the full normal ν\nu. The later claims apply it with M=AM=A and M=C(H(B0+θu))M=C(H(B_0+\theta u)) 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.

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.