ExitMeanValue

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

Nonnegativity of the one-point extension

The exit decomposition of a resolvent datum is an extended-real statement, so it is carried by nonnegative continuous data vanishing at infinity. This file records the one fact about the one-point extension that the decomposition needs: the extension of a nonnegative function is nonnegative, at the added point as well as on the live space.

theorem DivergenceFormProcess.Form.onePointRealExtension_nonneg {X : Type u_1} {f : X → ℝ} (hf : ∀ (y : X), 0 ≤ f y) (z : OnePoint X) : 0 ≤ onePointRealExtension f z

The zero extension of a nonnegative observable is nonnegative.