ExitMeanValueHarmonicDensity

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

Differences of harmonic parts and the density of the data

The harmonic parts of ExitMeanValueHarmonicPart.lean are attached to nonnegative continuous data vanishing at infinity, because the exit decomposition is an extended-real statement. A general datum is a difference of two nonnegative ones, so this file records what differences give.

One generic process fact comes first: the exit mean-value property is preserved by subtraction of bounded measurable functions (hasExitMeanValueOn_sub).

The analytic input is the density of the resolvent range. A positive C₀-contractive resolvent has dense range at every shift, and a continuous datum vanishing at infinity is the difference of its positive and negative parts, both nonnegative and vanishing at infinity. Hence every continuous datum vanishing at infinity is uniformly approximated by differences R_mu g₁ - R_mu g₂ of resolvents of nonnegative such data (exists_nonneg_c0_resolvent_approx).

The two together are what a consumer instantiates: a bounded measurable function uniformly approximated by differences of harmonic parts inherits their exit mean-value property.

theorem DivergenceFormProcess.StoppedDirichlet.hasExitMeanValueOn_sub {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} (hU : IsOpen U) {h k : alpha → ℝ} (hh : Measurable h) (hk : Measurable k) {M N : ℝ} (hM : ∀ (z : alpha), ‖h z‖ ≤ M) (hN : ∀ (z : alpha), ‖k z‖ ≤ N) (hharm : HasExitMeanValueOn P hP U h) (hkharm : HasExitMeanValueOn P hP U k) : HasExitMeanValueOn P hP U fun (z : alpha) => h z - k z

The exit mean-value property is preserved by differences. Both functions are integrable against the exit distribution because they are bounded and measurable.

The positive part of a continuous datum vanishing at infinity

def DivergenceFormProcess.Form.c0PosPart {d : ℕ} (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ

The positive part of a continuous datum vanishing at infinity.

Equations

• DivergenceFormProcess.Form.c0PosPart g = { toFun := fun (x : HCPolySupport.Vec d) => max (g x) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

@[simp]

theorem DivergenceFormProcess.Form.c0PosPart_apply {d : ℕ} (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (x : HCPolySupport.Vec d) : (c0PosPart g) x = max (g x) 0

theorem DivergenceFormProcess.Form.c0PosPart_nonneg {d : ℕ} (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (x : HCPolySupport.Vec d) : 0 ≤ (c0PosPart g) x

theorem DivergenceFormProcess.Form.c0PosPart_sub_c0PosPart_neg {d : ℕ} (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : c0PosPart g - c0PosPart (-g) = g

A continuous datum vanishing at infinity is the difference of two nonnegative ones.

theorem DivergenceFormProcess.Form.abs_apply_le_norm_zeroAtInfty {d : ℕ} (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (y : HCPolySupport.Vec d) : |g y| ≤ ‖g‖

The absolute value of a continuous datum vanishing at infinity is at most its norm.

Density of the resolvent range at nonnegative data

theorem DivergenceFormProcess.Form.exists_nonneg_c0_resolvent_approx {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (F : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) {eps : ℝ} (heps : 0 < eps) : ∃ (g₁ : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (g₂ : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (∀ (y : HCPolySupport.Vec d), 0 ≤ g₁ y) ∧ (∀ (y : HCPolySupport.Vec d), 0 ≤ g₂ y) ∧ ∀ (y : HCPolySupport.Vec d), |((R.operator mu) g₁) y - ((R.operator mu) g₂) y - F y| ≤ eps

The resolvents of nonnegative data are dense. Every continuous datum vanishing at infinity is uniformly approximated by a difference of resolvents of nonnegative continuous data vanishing at infinity: the resolvent has dense range, and a general datum splits into its positive and negative parts.