claimroutineinferred_dep

Descent to three slots and parameter dependence

Descends solution to three slots and gives smooth parameter dependence
transfers existence to the original domain
Claim·§A The Dirichlet problem on a periodic fiber·inside thmDirichlet problem for quaternionic Monge-Ampère

Statement (paper)

The unique solution uu on Ω~\widetilde\Omega is invariant under translations in every added periodic coordinate, hence descends to a solution on Ω\Omega, and every solution on Ω\Omega lifts to Ω~\widetilde\Omega, so uniqueness holds on Ω\Omega; the same lift gives comparison on subdomains, in particular on the balls in the three-slot fibers. For moving domains, pulling the lifted equation back to a fixed domain gives coefficients and boundary data depending smoothly on the parameters with linearization conjugate to the Dirichlet isomorphism, so the implicit function theorem in each C0k+2,αC^{k+2,\alpha}_0 gives smooth dependence of the solutions on the parameters up to the boundary, and the strict inequalities used to choose b,b′b,b' persist locally in the parameters.

In plain English

The solution on the lifted domain Ω~\widetilde\Omega is translation invariant in the added periodic coordinates, so it descends to Ω\Omega, and solutions on Ω\Omega lift back, which gives uniqueness and comparison on Ω\Omega and on subdomains such as balls in the three-slot fibers. For smoothly varying data and domains, the solutions depend smoothly on the parameters up to the boundary, and the strict inequalities that fix b,b′b,b' persist locally.

Why it's here

The existence and estimates are proved on the enlarged domain Ω~\widetilde\Omega, and this step transfers them to the original three-slot setting Ω\Omega, using the comparison and uniqueness from the first claim. Parameter dependence comes from pulling back to a fixed domain, where the linearization is conjugate to the Dirichlet isomorphism, so the implicit function theorem applies. This completes the uniqueness, barrier-constant and parameter-dependence parts of the theorem, building on the existence from the closedness claim.
Classified routine:
Follows directly from uniqueness and comparison (claim-thm-dirichlet-1), since translates of the solution are again solutions, combined with a standard implicit function theorem argument in Hölder spaces for smooth parameter dependence of elliptic Dirichlet problems.

Uses

claimComparison, uniqueness and continuity method setupclaimClosedness of solvable parameters and boundary smoothness

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Descent to three slots and parameter dependence" rests on claim-thm-dirichlet-1
  • info
    inferred_dep
    outline: "Descent to three slots and parameter dependence" rests on claim-thm-dirichlet-6