ExitTimePDEIdentificationL2

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

The shift-uniform comparison of the Dirichlet resolvents with the torsion function

The Dirichlet resolvent of the constant datum on an exhaustion cube at the positive shift lam is the solution of -div (a grad u) + lam u = 1 in V, u = 0 on the boundary of V,

and the torsion function is the solution of the same problem without the shift. This file compares the two in L^2(V), with an error that is proportional to the shift and otherwise depends only on the uniform bound of the torsion function.

The comparison rests on one identity. The torsion function solves the shifted problem with the datum 1 + lam w, so it is the shifted resolvent of that datum, and by linearity the difference between the torsion function and the Dirichlet resolvent of the constant datum is lam times the shifted resolvent of the torsion function.

The identity is used three times. At a shift small enough that 1 + lam w stays nonnegative — any shift below the reciprocal of the uniform bound — the positivity of the shifted resolvent gives that the torsion function is nonnegative. The positivity applied again then gives that the Dirichlet resolvent of the constant datum is below the torsion function at every positive shift. Finally, the torsion function is below its uniform bound times the constant datum, so the order preservation of the shifted resolvent bounds the shifted resolvent of the torsion function by that bound times the Dirichlet resolvent of the constant datum, which is itself below the bound; the difference is therefore at most the shift times the square of the bound.

The sandwich is then read as a norm estimate: on a cube of finite volume an almost-everywhere bound is an L^2 bound, so the Dirichlet resolvents of the constant datum converge to the torsion function in L^2(V) at a rate proportional to the shift.

Everything here is an almost-everywhere statement about L^2 classes, or a consequence of one. The pointwise reading on the cube is separate.

noncomputable def DivergenceFormProcess.Form.cubeOneL2 (d v : ℕ) : ↥(HCPolySupport.ScalarL2 (wholeSpaceCube d v))

The L² class of the constant datum of an exhaustion cube.

Equations

• DivergenceFormProcess.Form.cubeOneL2 d v = DivergenceFormProcess.Form.boundedMeasurableToScalarL2 ⋯ ⋯ ⋯

theorem DivergenceFormProcess.Form.cubeOneL2_ae (d v : ℕ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), ↑↑(cubeOneL2 d v) x = 1

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionL2 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ↥(HCPolySupport.ScalarL2 (wholeSpaceCube d v))

The L² class of the torsion function of an exhaustion cube.

Equations

• A.cubeTorsionL2 v = (A.cubeTorsionFunction v).toScalarL2

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionL2_eq_alphaShiftedResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : A.cubeTorsionL2 v = (alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeOneL2 d v + ↑lam • A.cubeTorsionL2 v)

The torsion function solves the shifted problem with the shifted datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionL2_sub_alphaShiftedResolvent_cubeOneL2 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : A.cubeTorsionL2 v - (alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeOneL2 d v) = ↑lam • (alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (A.cubeTorsionL2 v)

The torsion function exceeds the Dirichlet resolvent of the constant datum by the shifted resolvent of itself.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionL2_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), 0 ≤ ↑↑(A.cubeTorsionL2 v) x

The torsion function is nonnegative. At a shift small enough that the shifted datum stays nonnegative, the torsion function is the shifted resolvent of a nonnegative datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.alphaShiftedResolvent_cubeOneL2_le_cubeTorsionL2 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeOneL2 d v)) x ≤ ↑↑(A.cubeTorsionL2 v) x

The Dirichlet resolvent of the constant datum is below the torsion function.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionL2_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), ↑↑(A.cubeTorsionL2 v) x ≤ A.cubeTorsionBound v

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.alphaShiftedResolvent_cubeTorsionL2_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (A.cubeTorsionL2 v)) x ≤ A.cubeTorsionBound v * ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeOneL2 d v)) x

The shifted resolvent of the torsion function is bounded by the bound of the torsion function times the shifted resolvent of the constant datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionL2_sub_alphaShiftedResolvent_cubeOneL2_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), ↑↑(A.cubeTorsionL2 v) x - ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeOneL2 d v)) x ≤ ↑lam * (A.cubeTorsionBound v * A.cubeTorsionBound v)

The shift-uniform sandwich. The Dirichlet resolvent of the constant datum at a positive shift is below the torsion function and above it minus the shift times the square of the uniform bound.

The L² rate