claimroutineinferred_dep

Laplacian of X_0 gives wall flux minus interior

Gives ΔzX0\Delta_zX_0 as wall flux minus interior term ∫A:Σ\int A:\Sigma
A-part of the energy flux identity
Claim·§4.3 Cancelling the full determinant·inside propEnergy flux identity with full wall normal

Statement (paper)

For the term X0X_0, which integrates (−u)μ(-u)\mu, taking M=AM=A in (with the sign changed) gives that ΔzX0\Delta_z X_0 equals the boundary contribution B(z)=∫ρ G(r)∗AwG(r) δ(r) dζ\mathcal B(z)=\int \rho\,G(r)^*A_{\rm w}G(r)\,\delta(r)\dd\zeta minus the interior term ∫ΩzA:Σ  dζ\int_{\Omega_z}A:\Sigma\,\dd\zeta (the latter coming from ). On the wall only AwA_{\rm w} contributes, since the image of C(H(r))C(H(r)) is perpendicular to ν\nu.

In plain English

For the term X0X_0, which integrates (−u)μ(-u)\mu, the Laplacian ΔzX0\Delta_z X_0 equals the wall flux B(z)=∫ρ G(r)∗AwG(r) δ(r) dζ\mathcal B(z)=\int \rho\,G(r)^*A_{\rm w}G(r)\,\delta(r)\dd\zeta minus the interior term ∫ΩzA:Σ  dζ\int_{\Omega_z}A:\Sigma\,\dd\zeta.

Why it's here

This applies the moving-domain Green formula with M=AM=A (sign flipped), with the interior term supplied by the Schur energy identity. On the wall only AwA_{\rm w} survives because the image of C(H(r))C(H(r)) is perpendicular to ν\nu. It gives the AA-part of the identity in the proposition, namely the boundary integral and the nonnegative interior term A:ΣA:\Sigma.
Classified routine:
Direct application of the paper's moving-domain Green formula (previous claim) with M=A and a sign change, combined with the Schur energy identity. This is bookkeeping within the proof of the energy flux proposition.

Uses

claimGreen formula on moving total domain

Used by

Nothing in the paper

Sources

PaperOpen
Section
§4.3 Cancelling the full determinant
Page
—
Label
—
Line
sections/energy.tex:250
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Laplacian of X_0 equals wall flux minus terms" rests on claim-prop-energy-flux-1