ExitTimePDEIdentificationLimit

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

The exit-time function of an exhaustion cube is the torsion function

The limit of the Dirichlet resolvents of the constant datum as the shift decreases to zero is identified here, at every point of the cube and not only almost everywhere, with a representative of the torsion function that is continuous there.

The representative is produced from the torsion function itself. The torsion function is bounded, so truncating it at its bound and adding the constant datum gives a bounded measurable datum whose Dirichlet resolvent at shift one is, as an L² class, the torsion function again; the analytic layer supplies a representative of that resolvent which is continuous on the cube (cubeTorsionRepresentative).

With both families continuous on the cube, the almost-everywhere sandwich of the previous file holds at every point of the cube: the Dirichlet resolvent of the constant datum at the shift lam lies between the continuous representative minus lam times the square of the uniform bound and that representative itself. Letting the shift decrease to zero along 1 / (n + 1) squeezes the supremum, so the limit is exactly the value of the representative.

Two consequences are recorded. The limit is bounded on the whole compactification by the uniform bound of the torsion function, hence finite; and almost everywhere on the cube it is the extended-real image of the chosen torsion function.

def DivergenceFormProcess.Form.unitShift : ↑MarkovProcess.Semigroup.PositiveShift

The shift one.

Equations

• DivergenceFormProcess.Form.unitShift = ⟨1, DivergenceFormProcess.Form.unitShift._proof_1⟩

@[simp]

theorem DivergenceFormProcess.Form.unitShift_coe : ↑unitShift = 1

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

The torsion function truncated at its uniform bound and restricted to the cube.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_cubeTorsionTrunc {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : Measurable (A.cubeTorsionTrunc v)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_cubeTorsionTrunc_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (y : HCPolySupport.Vec d) : |A.cubeTorsionTrunc v y| ≤ A.cubeTorsionBound v

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionTrunc_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), A.cubeTorsionTrunc v y = (A.cubeTorsionFunction v).toFun y

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

The datum of the torsion function read as a shifted problem at shift one.

Equations

• A.cubeTorsionDatum v y = DivergenceFormProcess.Form.cubeOneDatum d v y + A.cubeTorsionTrunc v y

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionDatum_apply {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (y : HCPolySupport.Vec d) : A.cubeTorsionDatum v y = cubeOneDatum d v y + A.cubeTorsionTrunc v y

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_cubeTorsionDatum {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : Measurable (A.cubeTorsionDatum v)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_cubeTorsionDatum_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (y : HCPolySupport.Vec d) : |A.cubeTorsionDatum v y| ≤ 1 + A.cubeTorsionBound v

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

The continuous representative on the cube of the torsion function: the Dirichlet resolvent at shift one of the datum the torsion function solves for at that shift.

Equations

• A.cubeTorsionRepresentative v = A.analyticCubeResolvent DivergenceFormProcess.Form.unitShift (A.cubeTorsionDatum v) ⋯ ⋯ v

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuousOn_cubeTorsionRepresentative {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ContinuousOn (A.cubeTorsionRepresentative v) (wholeSpaceCube d v)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionRepresentative_of_notMem {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) {x : HCPolySupport.Vec d} (hx : x ∉ wholeSpaceCube d v) : A.cubeTorsionRepresentative v x = 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionRepresentative_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : A.cubeTorsionRepresentative v =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d v)] fun (x : HCPolySupport.Vec d) => ↑↑(A.cubeTorsionL2 v) x

The continuous representative agrees almost everywhere on the cube with the L² class of the torsion function.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_cubeOneDatum_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : A.analyticCubeResolvent lam (cubeOneDatum d v) ⋯ ⋯ v =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d v)] fun (x : HCPolySupport.Vec d) => ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeOneL2 d v)) x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_of_notMem {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) {x : HCPolySupport.Vec d} (hx : x ∉ wholeSpaceCube d m) : A.analyticCubeResolvent lam f hf hfD m x = 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_cubeOneDatum_le_cubeTorsionRepresentative {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d v) : A.analyticCubeResolvent lam (cubeOneDatum d v) ⋯ ⋯ v x ≤ A.cubeTorsionRepresentative v x

The Dirichlet resolvent of the constant datum is below the continuous representative of the torsion function at every point of the cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionRepresentative_sub_analyticCubeResolvent_cubeOneDatum_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d v) : A.cubeTorsionRepresentative v x - A.analyticCubeResolvent lam (cubeOneDatum d v) ⋯ ⋯ v x ≤ ↑lam * (A.cubeTorsionBound v * A.cubeTorsionBound v)

The continuous representative of the torsion function exceeds the Dirichlet resolvent of the constant datum by at most the shift times the square of the uniform bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionRepresentative_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (x : HCPolySupport.Vec d) : A.cubeTorsionRepresentative v x ≤ A.cubeTorsionBound v

theorem DivergenceFormProcess.Form.iSup_ofReal_eq_of_squeeze {g : ℕ → ℝ} {c e : ℝ} (hle : ∀ (n : ℕ), g n ≤ c) (hge : ∀ (n : ℕ), c - g n ≤ (↑n + 1)⁻¹ * e) : ⨆ (n : ℕ), ENNReal.ofReal (g n) = ENNReal.ofReal c

A sequence squeezed between a value and that value minus a null sequence has that value as the supremum of its nonnegative extended-real images.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeExitFunction_coe_eq {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (x : HCPolySupport.Vec d) : A.cubeExitFunction v ↑x = ENNReal.ofReal (A.cubeTorsionRepresentative v x)

The limit of the Dirichlet resolvents of the constant datum is the continuous representative of the torsion function at every point.