ExitTimePDE

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

The Dirichlet resolvent of the constant datum on an exhaustion cube

The exit-time problem on a bounded domain V is the Dirichlet problem with constant forcing, -div (a grad w) = 1 in V, w = 0 on the boundary of V,

and its shifted approximations are the Dirichlet resolvents R^V_lam 1 at the positive shifts lam. This file assembles those approximations for the exhaustion cubes V = wholeSpaceCube d v and records their behaviour as the shift decreases to zero.

The Dirichlet resolvent of a nonnegative datum is antitone in the shift: a larger shift discounts more, and the resolvent identity of the analytic layer converts this into an inequality between the two values. The transported family cubeExitResolvent therefore increases as the shift decreases, and its supremum along the shifts 1 / (n + 1), namely cubeExitFunction, is the candidate for the exit-time function.

The regularity witness for the values used here is explicit: on its cube the Dirichlet resolvent of the constant datum is continuous, which is what makes the pointwise statements independent of the choice of representative.

Everything in this file is analytic; no process, and no hypothesis about one, appears. The identification of cubeExitFunction with an expected exit time is proved separately.

The constant datum on an exhaustion cube

noncomputable def DivergenceFormProcess.Form.cubeOneDatum (d v : ℕ) : HCPolySupport.Vec d → ℝ

The datum of the exit-time problem on an exhaustion cube: the constant one on the cube, extended by zero.

Equations

• DivergenceFormProcess.Form.cubeOneDatum d v = (DivergenceFormProcess.Form.wholeSpaceCube d v).indicator fun (x : HCPolySupport.Vec d) => 1

theorem DivergenceFormProcess.Form.measurable_cubeOneDatum (d v : ℕ) : Measurable (cubeOneDatum d v)

theorem DivergenceFormProcess.Form.cubeOneDatum_nonneg (d v : ℕ) (x : HCPolySupport.Vec d) : 0 ≤ cubeOneDatum d v x

theorem DivergenceFormProcess.Form.abs_cubeOneDatum_le (d v : ℕ) (x : HCPolySupport.Vec d) : |cubeOneDatum d v x| ≤ 1

theorem DivergenceFormProcess.Form.cubeOneDatum_of_mem {d v : ℕ} {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d v) : cubeOneDatum d v x = 1

theorem DivergenceFormProcess.Form.cubeOneDatum_ae_indicator (d v : ℕ) : cubeOneDatum d v =ᵐ[MeasureTheory.volume] (wholeSpaceCube d v).indicator (cubeOneDatum d v)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeOneBarrierData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : WholeSpaceBarrierData A

The barrier data of the exit-time problem. The part domain is an exhaustion cube and the observable is the constant datum on it; every field is discharged by the axis-cube construction.

Equations

• A.cubeOneBarrierData v lam = DivergenceFormProcess.Form.axisCubeBarrierData A (fun (x : Fin d) => -3 ^ v) ⋯ lam ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeOneBarrierData_V {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : (A.cubeOneBarrierData v lam).V = wholeSpaceCube d v

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeOneBarrierData_f {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : (A.cubeOneBarrierData v lam).f = cubeOneDatum d v

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeOneBarrierData_lam {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : (A.cubeOneBarrierData v lam).lam = lam

The shifted family on the compactification and its limit

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeExitResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ℝ) : OnePoint (HCPolySupport.Vec d) → ENNReal

The Dirichlet resolvent of the constant datum on an exhaustion cube, transported to the one-point compactification by zero extension. Outside the positive shifts the value is zero; the identifications below are stated at positive shifts only.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeExitResolvent_coe {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) {lam : ℝ} (hlam : 0 < lam) (y : HCPolySupport.Vec d) : A.cubeExitResolvent v lam ↑y = ENNReal.ofReal (A.analyticCubeResolvent ⟨lam, hlam⟩ (cubeOneDatum d v) ⋯ ⋯ v y)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeExitFunction {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : OnePoint (HCPolySupport.Vec d) → ENNReal

The limit of the Dirichlet resolvents of the constant datum as the shift decreases to zero, taken as the supremum along the shifts 1 / (n + 1). This is the shape in which the expected exit time consumes the limit.

Equations

• A.cubeExitFunction v z = ⨆ (n : ℕ), A.cubeExitResolvent v (↑n + 1)⁻¹ z

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeExitFunction_coe {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (y : HCPolySupport.Vec d) : A.cubeExitFunction v ↑y = ⨆ (n : ℕ), ENNReal.ofReal (A.analyticCubeResolvent ⟨(↑n + 1)⁻¹, ⋯⟩ (cubeOneDatum d v) ⋯ ⋯ v y)

The limit read on the live space: the supremum of the values of the Dirichlet resolvents of the constant datum at the shifts 1 / (n + 1).