StoppedDirichletHarmonic

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

Stopped identities for functions represented by the exit distribution

Let Q be the continuous-path process of a conservative Feller kernel semigroup and let U be an open set with exit time tau. A function h is represented by the exit distribution of U when h y = E_y[h(X_tau)] for every y of U

(HasExitMeanValueOn). This is the mean-value formulation of harmonicity relative to the process: it says nothing about smoothness, and it is a statement about h and U alone, not about the conclusions proved from it below.

Two identities for the stopped process follow, for every deterministic horizon t.

• A function represented by the exit distribution is also represented by the stopped position (integral_eval_exitTimeTrunc_eq_of_hasExitMeanValueOn): E_x[h(X_{t and tau})] = h x. The proof splits the path space at the survival event {t < tau}. Off it the stopped position is already the exit position. On it the stopped position is X_t, where the representation is available because X_t lies in U; the restricted Markov property at the deterministic time t then rewrites the resulting restarted expectation as the expectation of the exit value of the shifted path, and shifting does not move the exit position once the exit time is finite.

• Subtracting a multiple of the expected exit time w y = E_y[tau] produces the second stopped identity (integral_eval_exitTimeTrunc_eq_add_of_hasExitMeanValueOn): if u = h - sigma * w, then E_x[u(X_{t and tau})] = u x + sigma * E_x[t and tau]. The whole content of the second identity beyond the first is the remaining-exit-time identity of StoppedDirichlet.lean, whose proof needs no generator either. The expected stopped time is also written with the horizon exposed, E_x[t and tau] = t - E_x[(t - tau) on {tau <= t}].

Neither identity refers to a generator or to a domain of one. What must be supplied from the analytic side is exactly the hypothesis HasExitMeanValueOn: that the continuous representative of the Dirichlet solution with the given boundary values is reproduced by the exit distribution of the domain.

def DivergenceFormProcess.StoppedDirichlet.HasExitMeanValueOn {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) (h : alpha → ℝ) : Prop

A function is represented by the exit distribution of U when, from every starting point of U, its value is the expectation of its value at the exit position.

Equations

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

theorem DivergenceFormProcess.StoppedDirichlet.integral_eval_exitTimeTrunc_eq_of_hasExitMeanValueOn {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {h : alpha → ℝ} (hh : Measurable h) (C : ℝ) (hC : ∀ (y : alpha), ‖h y‖ ≤ C) (hharm : HasExitMeanValueOn P hP U h) (t : NNReal) {x : alpha} (hx : x ∈ U) (hwfin : expectedExitTime P hP U x ≠ ⊤) : ∫ (omega : MarkovProcess.ContinuousPath alpha), h (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x = h x

A function represented by the exit distribution is represented by the stopped position. For every deterministic horizon, the expectation of the function at the position stopped on leaving U is its value at the starting point.

theorem DivergenceFormProcess.StoppedDirichlet.integral_eval_exitTimeTrunc_eq_add_of_hasExitMeanValueOn {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {h : alpha → ℝ} (hh : Measurable h) (C : ℝ) (hC : ∀ (y : alpha), ‖h y‖ ≤ C) (hharm : HasExitMeanValueOn P hP U h) (sigma : ℝ) {u : alpha → ℝ} (hu : ∀ (y : alpha), u y = h y - sigma * (expectedExitTime P hP U y).toReal) (t : NNReal) {x : alpha} (hx : x ∈ U) (hwfin : expectedExitTime P hP U x ≠ ⊤) : ∫ (omega : MarkovProcess.ContinuousPath alpha), u (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x = u x + sigma * ∫ (omega : MarkovProcess.ContinuousPath alpha), ↑(MarkovProcess.ContinuousPath.exitTimeTrunc U t omega) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x

The stopped identity for a function with a remaining-time correction. If u is the difference of a function represented by the exit distribution and a multiple of the expected exit time, then the expectation of u at the stopped position exceeds its value at the starting point by the same multiple of the expected stopped time.

theorem DivergenceFormProcess.StoppedDirichlet.integral_exitTimeTrunc_eq_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) (t : NNReal) (x : alpha) : ∫ (omega : MarkovProcess.ContinuousPath alpha), ↑(MarkovProcess.ContinuousPath.exitTimeTrunc U t omega) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x = ↑t - ∫ (omega : MarkovProcess.ContinuousPath alpha), (survivalEvent U t)ᶜ.indicator (fun (omega : MarkovProcess.ContinuousPath alpha) => ↑t - (MarkovProcess.ContinuousPath.exitTime U omega).toReal) omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x

The expected stopped time with the horizon exposed: it is the horizon less the expected shortfall on the event that the exit has already occurred.

theorem DivergenceFormProcess.StoppedDirichlet.isOpen_image_coe_of_isOpen {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) : IsOpen (OnePoint.some '' V)

The image of an open subset of the live space is open in the compactification.