claimroutineinferred_dep

Hessian lower bound for rP_*

Shows

H_{fib}(rP_*)\ge(1-C/D)P_*R

, so

rP_*

is convex

makes

rP_*

a subsolution barrier

Claim·§5 Estimating the energy on a fixed fiber·inside propEnergy barrier on a fixed fiber

Statement (paper)

With

R=H_{\mathrm{fib}}(r)

, which satisfies

R\ge c s^{-2}I

and

G_{\mathrm{fib}}(r)G_{\mathrm{fib}}(r)^*\le C R

, one has

H_{\mathrm{fib}}(rP_*)\ge (1-C/D)P_*R

In plain English

Let

R=H_{\mathrm{fib}}(r)

, which satisfies

R\ge c s^{-2}I

and

G_{\mathrm{fib}}(r)G_{\mathrm{fib}}(r)^*\le C R

. Then the fiber Hessian of the product

rP_*

is bounded below by

(1-C/D)P_*R

Why it's here

This is the product-rule step:

H_{\mathrm{fib}}(rP_*)=P_*R+rH_{\mathrm{fib}}(P_*)+

cross terms, and the claim shows the

P_*

-derivative terms are only a

C/D

fraction of

P_*R

. The Hessian and gradient bounds on

r

come from the fiber geometry lemma, and the derivative bounds on

P_*

at scale

Ds

come from the regularity claim, so the errors are

O(1/D)

relative to

P_*R

. The resulting convexity of

rP_*

supports the comparison function used in the boundary-quotient bound.

Classified routine:

Direct calculation from the Hessian product rule (lem-hessian-calculus) combined with the geometric bounds on r (lem-fiber-geometry) and the scale-Ds derivative bounds on P_* (claim-prop-fixed-barrier-1); the cross terms are absorbed by Cauchy–Schwarz, leaving an O(1/D) error relative to P_*R.

Uses

lemFiber Hessian geometry and JacobianlemHessian calculus in quaternionic coordinatesclaimSmoothed density P_* is regular and controlled

Used by

claimUpper bound on boundary quotient u/r

Sources

PaperOpen

Section: §5 Estimating the energy on a fixed fiber
Page: —
Label: —
Line: sections/barrier.tex:113

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Hessian lower bound for comparison function rP_*" rests on claim-prop-fixed-barrier-1