CubeSetAtHarmonicPart #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The harmonic part of a resolvent datum on a translated triadic cube #
Fix a translated triadic cube cubeSetAt y n, a positive shift mu and a continuous datum g
vanishing at infinity, and write psi = R_mu g for the analytic resolvent supplied with the
process. The vanishing-shift family of ExitMeanValueCubeSetAtProcess.lean,
psi - R^V_lam g + (mu - lam) R^V_lam psi,
is rewritten here by linearity of the Dirichlet resolvent in its datum. With the residual
cubeSetAtResolventResidual = g - mu psi (restricted to the cube),
which does not depend on the shift, the family is
psi - R^V_lam (residual) - lam R^V_lam psi (cubeSetAtHarmonicApprox_eq).
The first Dirichlet resolvent converges to the Green potential of the residual as the shift
decreases to zero, and the second term carries a factor of the shift against a bound uniform in
the shift, so it vanishes. The limit is therefore
cubeSetAtHarmonicPart = psi - partGreenPotential (residual),
which agrees with psi off the cube because the Green potential does. This discharges the
predicate IsCubeSetAtResolventHarmonicPart of ExitMeanValueCubeSetAtProcess.lean for that
function, with no hypothesis beyond the data.
This is the statement of ExitMeanValueHarmonicPart.lean on the translated triadic cube, with
the shift-uniform bound supplied by PartTorsion.lean.
The residual datum #
The residual of a resolvent datum on a translated triadic cube: the datum less the shift times the resolvent, both restricted to the cube. It does not depend on the Dirichlet shift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Dirichlet resolvent of the cube as a shift-indexed part resolvent #
The Dirichlet resolvent of a continuous datum vanishing at infinity on a translated triadic cube is the shift-indexed Dirichlet resolvent of the part domain at the restricted datum.
The vanishing-shift family at the residual datum #
The vanishing-shift family, rewritten at the residual datum. At every positive shift the
family of ExitMeanValueCubeSetAtProcess.lean is the resolvent datum less the Dirichlet resolvent
of the residual less the shift times the Dirichlet resolvent of the datum.
The harmonic part #
The harmonic part of a resolvent datum on a translated triadic cube: the analytic resolvent of the datum less the Green potential of the residual.
Equations
- A.cubeSetAtHarmonicPart R y n mu g z = ((R.operator mu) g) z - A.partGreenPotential ⋯ (DivergenceFormProcess.Form.cubeSetAtResolventResidual R y n mu g) ⋯ ⋯ ⋯ z
Instances For
The harmonic part is continuous on the cube. The resolvent datum is continuous on the whole space and the Green potential is continuous on the cube.
The harmonic part discharges the vanishing-shift predicate. No hypothesis beyond the data appears: the limit defining the predicate exists and is the harmonic part.