claimroutineinferred_dep

Energy and wall flux bounds

Bounds F\mathcal F above and shows ΔzF\Delta_z\mathcal F is exponentially small
numerator of the potential and the input bound
Claim·§5 Estimating the energy on a fixed fiber·inside propEnergy barrier on a fixed fiber

Statement (paper)

For all T∈RT\in\mathbb R and 2a≤s=∣τ∣≤32a\le s=|\tau|\le3, one has F(T,τ)≤Ca2σm∥gT∥pcpc\mathcal F(T,\tau)\le Ca^2\sigma^m\|g_T\|_{\pc}^{\pc} and ΔzF(T,τ)≤C(a/s)2σme−c0σ∥gT∥pcpc\Delta_z\mathcal F(T,\tau)\le C(a/s)^2\sigma^m e^{-c_0\sigma}\|g_T\|_{\pc}^{\pc}.

In plain English

For every TT and 2a≤s=∣τ∣≤32a\le s=|\tau|\le3, the fiber energy satisfies F(T,τ)≤Ca2σm∥gT∥pcpc\mathcal F(T,\tau)\le Ca^2\sigma^m\|g_T\|_{\pc}^{\pc}. Its Laplacian satisfies ΔzF(T,τ)≤C(a/s)2σme−c0σ∥gT∥pcpc\Delta_z\mathcal F(T,\tau)\le C(a/s)^2\sigma^m e^{-c_0\sigma}\|g_T\|_{\pc}^{\pc}, which is exponentially small.

Why it's here

This step turns the pointwise bounds into the two integral estimates needed for the barrier argument. The energy is comparable to X0X_0 by the energy comparison lemma. Both X0X_0 and the wall flux from the energy flux identity are then bounded using Aw≲s−2dσmP∗dA_{\mathrm w}\lesssim s^{-2d}\sigma^mP_*^d, the Gaussian wall decay, the quotient bound u/r≲σm1P∗u/r\lesssim\sigma^{m_1}P_*, the Jacobian from the fiber geometry lemma, and ∫P∗d+1≤∥gT∥pcpc\int P_*^{d+1}\le\|g_T\|_{\pc}^{\pc}. The resulting exponentially small bound on ΔzF\Delta_z\mathcal F is what is later divided by F\mathcal F to obtain the potential V(s)V(s).
Classified routine:
Direct bookkeeping consequence of the earlier nodes: the energy comparison lemma, the energy flux identity, and the current/wall-decay, quotient and Jacobian bounds, integrated against ∫P∗d+1≤∥gT∥pc\int P_*^{d+1}\le\|g_T\|^{\pc}. This turns the pointwise estimates into the two integral bounds.

Uses

lemFiber energy comparable to X_0lemFiber Hessian geometry and JacobianpropWave current is positive and divergence-freepropEnergy flux identity with full wall normalclaimSmoothed density P_* is regular and controlledclaimCurrent and density bounds with wall decayclaimUpper bound on boundary quotient u/r

Used by

claimChoosing gamma and K yields the barrier inequalities

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Energy upper bound and wall flux bound" rests on claim-prop-fixed-barrier-1
  • info
    inferred_dep
    outline: "Energy upper bound and wall flux bound" rests on claim-prop-fixed-barrier-2
  • info
    inferred_dep
    outline: "Energy upper bound and wall flux bound" rests on claim-prop-fixed-barrier-4