ExitMeanValueCubeSetAtProcess

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The vanishing-shift harmonic part on a translated triadic cube

The resolvent decomposition at the first exit from a domain and the vanishing-shift limit of its analytic right-hand side are developed on the centred exhaustion cubes in ExitMeanValue.lean. This file states the corresponding predicate on the translated triadic cube cubeSetAt y n, the carrier the localized Dirichlet problems of the field are posed on.

• IsCubeSetAtResolventHarmonicPart names the vanishing-shift limit: a function agreeing with psi = R_mu g off the cube which, on the cube, is the limit as the shift decreases to zero of psi - R^V_lam g + (mu - lam) R^V_lam psi.
• hasExitMeanValueOn_onePointRealExtension_of_forall_approx_cubeSetAt propagates the exit mean-value property of the cube to uniform limits.

The statements are on the one-point compactification, where the process lives. The analytic identification of the vanishing-shift limit with the a-harmonic extension of the boundary datum of the cube is a separate question and is not addressed here.

3. The vanishing-shift limit and the exit mean-value property

def DivergenceFormProcess.Form.WholeSpaceAnalyticData.IsCubeSetAtResolventHarmonicPart {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (h : HCPolySupport.Vec d → ℝ) : Prop

The vanishing-shift Dirichlet decomposition of a resolvent datum on a translated triadic cube. Write psi = R_mu g for the analytic resolvent supplied with the process. A function h on the live space is the harmonic part of psi on the cube when it agrees with psi off the cube and, on the cube, is the limit as the shift decreases to zero of psi - R^V_lam g + (mu - lam) R^V_lam psi,

where R^V_lam is the Dirichlet resolvent of the cube. Only the analytic Dirichlet resolvents of the cube and the analytic resolvent of the datum appear; no process does.

Equations

• One or more equations did not get rendered due to their size.

theorem DivergenceFormProcess.Form.hasExitMeanValueOn_onePointRealExtension_of_forall_approx_cubeSetAt {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (y : HCPolySupport.Vec d) (n : ℤ) {h : HCPolySupport.Vec d → ℝ} (hh : Measurable h) {M : ℝ} (hM : ∀ (z : HCPolySupport.Vec d), |h z| ≤ M) (happrox : ∀ eps > 0, ∃ (k : HCPolySupport.Vec d → ℝ), Measurable k ∧ (∃ (C : ℝ), ∀ (z : HCPolySupport.Vec d), |k z| ≤ C) ∧ StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension k) ∧ ∀ (z : HCPolySupport.Vec d), |k z - h z| ≤ eps) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension h)

The exit mean-value property of a translated triadic cube passes to uniform limits of the boundary data. This is the process side of a density argument: a uniform limit of zero extensions with the exit mean-value property has it too.