lemmaroutine

Fiber energy comparable to X_0

Shows n−1n+1X0≤F≤nn+1X0\frac{n-1}{n+1}X_0\le\mathcal F\le\frac{n}{n+1}X_0 on each fiber
transfers bounds between X0X_0 and the fiber energy
Lemma·lem:energy-comparison·§4.4 Size of the energy on a fiber

Statement (paper)

On every spatial fiber, F=n−1n+1X0+1λn(n+1)∫ΩzGfib(u)∗C(Du)Gfib(u) dζ. \mathcal F=\frac{n-1}{n+1}X_0+ \frac{1}{\lambda n(n+1)} \int_{\Omega_z}G_{\rm fib}(u)^*C(D_u)G_{\rm fib}(u)\dd\zeta . In particular, n−1n+1X0≤F≤nn+1X0\frac{n-1}{n+1}X_0\le\mathcal F\le\frac{n}{n+1}X_0.

In plain English

On each spatial fiber, the energy F\mathcal F equals n−1n+1X0\frac{n-1}{n+1}X_0 plus a nonnegative correction, 1λn(n+1)∫ΩzGfib(u)∗C(Du)Gfib(u) dζ\frac{1}{\lambda n(n+1)}\int_{\Omega_z}G_{\rm fib}(u)^*C(D_u)G_{\rm fib}(u)\,d\zeta. Hence n−1n+1X0≤F≤nn+1X0\frac{n-1}{n+1}X_0\le\mathcal F\le\frac{n}{n+1}X_0.

Why it's here

This turns the fiber energy F\mathcal F into a quantity comparable to X0X_0 with explicit constants, so later bounds on X0X_0 transfer to F\mathcal F in both directions. The later energy upper bound, wall flux bound and interior lower bound use this comparison. The upper bound requires the correction term to be at most 1n+1X0\frac{1}{n+1}X_0, which the stated sandwich asserts.
Classified routine:
An explicit algebraic identity for the fiber energy, obtained by direct computation (decomposing it into its X_0 part and a quadratic-form correction), with the bounds following from positivity and boundedness of C(D_u). It is technical bookkeeping supporting the paper's main energy argument rather than a new idea in itself.

Uses

Nothing else in the paper

Used by

propEnergy barrier on a fixed fiberclaimEnergy and wall flux boundsclaimInterior energy lower bound via ball quadraticclaimDeterminant energy and balance on pencil fibers

Sources

PaperOpen
Section
§4.4 Size of the energy on a fiber
Page
—
Label
lem:energy-comparison
Line
sections/energy.tex:315
Leannot aligned

Phase 2 aligns this node to a Lean declaration.