ExitMeanValueHarmonicPotential #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The vanishing-shift limit of the Dirichlet resolvents of an exhaustion cube #
The Dirichlet resolvents R^V_lam f of a fixed bounded measurable datum on an exhaustion cube
converge as the shift decreases to zero, and this file constructs the limit and bounds it.
Two facts drive everything. First, the Dirichlet resolvent of a datum bounded by D is bounded
by D times the uniform bound of the torsion function of the cube
uniformly in the shift: comparison with the
constant datum replaces the shift-dependent bound D / lam. Second, the resolvent identity
expresses the difference of the values at two shifts as the difference of the shifts times a
third Dirichlet resolvent, so the family is Lipschitz in the shift with a shift-independent
constant.
A Lipschitz real family on the positive half-line converges as its argument decreases to zero,
with an error proportional to the argument (exists_forall_abs_sub_le_of_lipschitz). The limit
is the Green potential of the cube; it vanishes off the cube, obeys the same uniform bound, is
measurable, and is approached at the linear rate recorded above.
Everything here is analytic: no process, and no hypothesis about one, appears. The identification of that limit with the zero-trace weak solution of the unshifted Dirichlet problem is a separate question and is not addressed here.
A Lipschitz family on the positive shifts #
A Lipschitz real family on the positive half-line has a limit at zero. If the values at two positive arguments differ by at most a constant times the difference of the arguments, then there is a real number approached at the linear rate as the argument decreases to zero.