claimroutineinferred_dep

Upper bound on boundary quotient u/r

Bounds

u/r\le C_1\sigma^{m_1}P_*

by comparing with

v_*=C_1\sigma^{m_1}rP_*

boundary quotient bound for the wall flux

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

Statement (paper)

For

r\le0

one has

0\le u/r\le C_1\sigma^{m_1}P_*

, with

C_1,m_1

large enough. This follows from the comparison

v_*\le u\le0

, where

v_*=C_1\sigma^{m_1}rP_*

satisfies

\det\big(B_{\mathrm{fib}}+H_{\mathrm{fib}}(v_*)\big)\ge\lambda\mu

and has the same zero boundary data as

u

In plain English

On the region

r\le0

, the quotient

u/r

is nonnegative and bounded above by

C_1\sigma^{m_1}P_*

for suitably large

C_1,m_1

. This follows by comparing

u

with the explicit function

v_*=C_1\sigma^{m_1}rP_*

, which lies below

u

and has the same zero boundary data.

Why it's here

The comparison function

v_*

is made a subsolution using the convexity of

rP_*

from the Hessian lower bound together with the density bound

\mu\le Cs^{-2d}\sigma^mP_*^d

, so that

\det(B_{\mathrm{fib}}+H_{\mathrm{fib}}(v_*))\ge\lambda\mu

. The Dirichlet problem's comparison principle then gives

v_*\le u\le0

, and dividing by

r\le0

yields the quotient bound that the later energy and wall-flux estimates use.

Classified routine:

Standard barrier argument: an explicit subsolution

v_*

is built from the Hessian lower bound (claim-prop-fixed-barrier-3) and the density bound (claim-prop-fixed-barrier-2). The comparison principle for the quaternionic Monge–Ampère Dirichlet problem (thm-dirichlet) then gives

v_*\le u\le0

, and dividing by

r\le0

yields the bound.

Uses

thmDirichlet problem for quaternionic Monge-AmpèreclaimCurrent and density bounds with wall decayclaimHessian lower bound for rP_*

Used by

claimEnergy and wall flux bounds

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Upper bound on boundary quotient u/r" rests on claim-prop-fixed-barrier-2
info
inferred_dep
outline: "Upper bound on boundary quotient u/r" rests on claim-prop-fixed-barrier-3