ExitMeanValueHarmonicPart

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

The uniform bound of the residual datum on an exhaustion cube

The vanishing-shift family of the exit decomposition is rewritten by linearity of the Dirichlet resolvent in its datum, against the residual g - mu psi restricted to the cube, which does not depend on the shift. This file records the uniform bound that residual obeys, cubeResolventResidualBound, together with its nonnegativity.

The residual datum

noncomputable def DivergenceFormProcess.Form.cubeResolventResidualBound {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ℝ

The uniform bound of the residual datum.

Equations

• DivergenceFormProcess.Form.cubeResolventResidualBound R mu g = ‖g‖ + ↑mu * ‖(R.operator mu) g‖

theorem DivergenceFormProcess.Form.cubeResolventResidualBound_nonneg {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : 0 ≤ cubeResolventResidualBound R mu g