claimroutineinferred_dep

Double normal derivative bound and full C2

Bounds the double normal derivative, giving a full C2C^2 bound
completes the C2C^2 estimate
Claim·§A The Dirichlet problem on a periodic fiber·inside thmDirichlet problem for quaternionic Monge-Ampère

Statement (paper)

At the boundary, the double normal derivative ψνν\psi_{\nu\nu} is bounded: compression of QQ to the quaternionic orthogonal complement of ν\nu gives D≥cID\ge cI, and the Schur formula (for m>1m>1; the identity Q=gtQ=g_t for m=1m=1) yields ψνν=gt/det⁡D+z∗D−1z−c1≤C\psi_{\nu\nu}=g_t/\det D+z^*D^{-1}z-c_1\le C. Together with Equation  this gives D2ψ≤CID^2\psi\le CI throughout the domain, and since Δψ=tr⁡Q>0\Delta\psi=\tr Q>0, every real Hessian eigenvalue is at least −(4m−1)C-(4m-1)C, which is the full C2C^2 bound on ψ\psi.

In plain English

At the boundary the double normal derivative ψνν\psi_{\nu\nu} is bounded above by a constant CC, which together with the interior directional bound gives D2ψ≤CID^2\psi\le CI everywhere. Since Δψ=tr⁡Q>0\Delta\psi=\tr Q>0, every real Hessian eigenvalue is at least −(4m−1)C-(4m-1)C, so ψ\psi has a full C2C^2 bound.

Why it's here

With the mixed normal-tangential bound, this supplies the last missing entry of the boundary Hessian: compressing QQ to the orthogonal complement of ν\nu gives D≥cID\ge cI, and the Schur formula (or Q=gtQ=g_t when m=1m=1) then bounds ψνν\psi_{\nu\nu} above. A one-sided upper Hessian bound plus positive Laplacian gives a two-sided bound, which is the C2C^2 estimate that the Evans-Krylov step uses to place D2ψD^2\psi in a compact convex set.
Classified routine:
Standard double-normal boundary estimate in the Caffarelli–Nirenberg–Spruck (1985) method for Monge–Ampère Dirichlet problems, adapted to the quaternionic setting via a Schur complement; the two-sided bound from an upper Hessian bound plus positive Laplacian is elementary.

Uses

lemMoore determinant and cofactor propertiesclaimMixed normal-tangential derivatives bounded at boundarylemHessian calculus in quaternionic coordinates

Used by

claimEvans-Krylov C^{2,alpha} estimate

Sources

PaperOpen
Section
§A The Dirichlet problem on a periodic fiber
Page
—
Label
—
Line
sections/dirichlet.tex:150
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Double normal derivative via Schur; full C2 bound" rests on claim-thm-dirichlet-3
  • info
    inferred_dep
    outline: "Double normal derivative via Schur; full C2 bound" rests on lem:hessian-calculus