ShiftedResolventRegularity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Interior regularity witnesses for the shifted resolvents #
The interior estimates the divergence-form layer consumes are packaged here as
predicates on the coefficient field: HasContinuousShiftedResolvents for a
continuous representative on the open set, and HasLocalHolderShiftedResolvents
and HasLocalHolderPenalizedResolvents for the local Hölder form.
Stating the layer against a witness rather than against a smallness hypothesis keeps the analytic input in one place: a caller supplies the witness once and every downstream statement is indexed by it.
The interior regularity witness. For every positive shift and every
L² datum with an essential bound, the shifted resolvent has a representative
continuous on the open domain. No boundary value is asserted, and no bound on
the representative is asserted: the statement mentions only the L² class.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The freezing route to the witness. A coefficient whose symmetric part
is the scalar field nu • 1 and whose skew part is continuous on the domain has
continuous interior representatives, with no restriction on the size of the
skew part.
Restriction of the freezing route to a subdomain. The witness itself
does not restrict along V ⊆ U, because the resolvent of V is a different
operator; the hypotheses of the freezing route do, so the witness for the
subdomain is available whenever the coefficient is continuous on U.
The quantitative interior regularity witness. It adds one clause to
HasContinuousShiftedResolvents: at every point of the domain there is a
radius, depending on the point but not on the datum, on which every
representative of the shifted resolvent of a datum with essential bound M
that is continuous there obeys the explicit interior Hölder bound of the
small-contrast Schauder estimate, with gradient budget (min mu lam)⁻¹ ‖f‖ and
forcing budget B * M. The radius does not see the datum at all, and the
constant sees it only through ‖f‖ and M. On a bounded domain the first of
these is controlled by the second, since ‖f‖ ≤ M * |U| ^ (1 / 2), and the
constant is increasing in its gradient budget; so the bound is uniform over
every family of data with a common essential bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quantitative witness for the penalized family. One radius and one constant, both free of the penalization index, serve the whole penalized sequence of a fixed datum at each point of the part domain.
Equations
- One or more equations did not get rendered due to their size.