ExitTimePDEIdentificationCube

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

The exit-time function of a translated triadic cube

The limit of the Dirichlet resolvents of the constant datum on y + □_n as the shift decreases to zero is identified here with any bounded continuous representative of the zero-trace solution of -div (a grad w) = 1 in y + □_n, w = 0 on the boundary,

at every point of the cube. The identification on the centred exhaustion cubes is the same argument at the special centre and scale; nothing here refers to that case, and the solution is supplied rather than constructed, so no existence or sup-norm estimate is repeated.

The argument is the shift-uniform sandwich. A zero-trace solution of the constant forcing solves the shifted problem with datum 1 + lam w, so it is the shifted resolvent of that datum, and by linearity the difference between it and the shifted resolvent of the constant datum is lam times the shifted resolvent of itself. Positivity of the shifted resolvent applied at a small shift gives that the solution is nonnegative; applied again it gives that the shifted resolvent of the constant datum stays below the solution; and order preservation against the uniform bound gives that the gap is at most the shift times the square of that bound. Both sides of the sandwich are continuous on the open cube, so the almost-everywhere statement is pointwise there, and the supremum along the shifts 1 / (k + 1) is squeezed to the value of the representative.

Main definitions

• cubeSetAtOneL2 — the L² class of the constant datum of y + □_n.

Main results

• toScalarL2_eq_alphaShiftedResolvent_add_smul — the resolvent identity w = R_lam (1 + lam w) for a zero-trace solution of the constant forcing.
• alphaShiftedResolvent_le_of_isScalarForcedWeakSolution, sub_alphaShiftedResolvent_le_of_isScalarForcedWeakSolution — the two halves of the shift-uniform sandwich, on an arbitrary open bounded convex domain.
• cubeSetAtExitFunction_coe_eq_of_isScalarForcedWeakSolution — the exit-time function of y + □_n is the continuous representative of the solution at every point of the cube.

References

• ABK26, the localized exit-time problem of Section 5.2.

1. The shift-uniform sandwich on an open bounded convex domain

theorem DivergenceFormProcess.Form.toScalarL2_eq_alphaShiftedResolvent_add_smul {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu Lam : ℝ} (hnu : 0 < nu) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (w : HCPolySupport.H10Function U) (hw : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function) (one : ↥(HCPolySupport.ScalarL2 U)) (hone : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑one x = 1) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : w.toScalarL2 = (alphaShiftedResolvent a ⋯ hnu hEll) (one + ↑lam • w.toScalarL2)

A zero-trace solution of the constant forcing is the shifted resolvent of the shifted datum. This is the identity w = R_lam (1 + lam w).

theorem DivergenceFormProcess.Form.toScalarL2_sub_alphaShiftedResolvent {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu Lam : ℝ} (hnu : 0 < nu) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (w : HCPolySupport.H10Function U) (hw : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function) (one : ↥(HCPolySupport.ScalarL2 U)) (hone : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑one x = 1) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : w.toScalarL2 - (alphaShiftedResolvent a ⋯ hnu hEll) one = ↑lam • (alphaShiftedResolvent a ⋯ hnu hEll) w.toScalarL2

The gap between the solution and the shifted resolvent of the constant datum is the shift times the shifted resolvent of the solution.

theorem DivergenceFormProcess.Form.toScalarL2_nonneg_of_isScalarForcedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu Lam : ℝ} (hnu : 0 < nu) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (w : HCPolySupport.H10Function U) {Mb : ℝ} (hw : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function) (one : ↥(HCPolySupport.ScalarL2 U)) (hone : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑one x = 1) (hMb : 0 ≤ Mb) (hwb : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |w.toFun x| ≤ Mb) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑w.toScalarL2 x

A bounded zero-trace solution of the constant forcing is nonnegative. At a shift small enough that 1 + lam w stays nonnegative, the solution is the shifted resolvent of a nonnegative datum.

theorem DivergenceFormProcess.Form.alphaShiftedResolvent_le_of_isScalarForcedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu Lam : ℝ} (hnu : 0 < nu) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (w : HCPolySupport.H10Function U) {Mb : ℝ} (hw : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function) (one : ↥(HCPolySupport.ScalarL2 U)) (hone : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑one x = 1) (hMb : 0 ≤ Mb) (hwb : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |w.toFun x| ≤ Mb) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑((alphaShiftedResolvent a ⋯ hnu hEll) one) x ≤ ↑↑w.toScalarL2 x

The lower half of the sandwich. The shifted resolvent of the constant datum never exceeds a bounded zero-trace solution of the constant forcing.

theorem DivergenceFormProcess.Form.sub_alphaShiftedResolvent_le_of_isScalarForcedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu Lam : ℝ} (hnu : 0 < nu) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (w : HCPolySupport.H10Function U) {Mb : ℝ} (hw : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function) (one : ↥(HCPolySupport.ScalarL2 U)) (hone : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑one x = 1) (hMb : 0 ≤ Mb) (hwb : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |w.toFun x| ≤ Mb) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑w.toScalarL2 x - ↑↑((alphaShiftedResolvent a ⋯ hnu hEll) one) x ≤ ↑lam * (Mb * Mb)

The upper half of the sandwich. The gap between a bounded zero-trace solution of the constant forcing and the shifted resolvent of the constant datum is at most the shift times the square of the uniform bound.

2. The constant datum of a translated triadic cube as an L² class

noncomputable def DivergenceFormProcess.Form.cubeSetAtOneL2 {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : ↥(HCPolySupport.ScalarL2 (Algsuperdiff.Section5.Support.cubeSetAt y n))

The L² class of the constant datum of y + □_n: the class the barrier data of the exit-time problem on that cube is built from.

Equations

• DivergenceFormProcess.Form.cubeSetAtOneL2 y n = DivergenceFormProcess.Form.partDatumL2 ⋯ ⋯ ⋯

theorem DivergenceFormProcess.Form.cubeSetAtOneL2_ae {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (Algsuperdiff.Section5.Support.cubeSetAt y n), ↑↑(cubeSetAtOneL2 y n) x = 1

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneResolvent_ae_alphaShiftedResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : A.cubeSetAtOneResolvent y n lam =ᵐ[HCPolySupport.volumeMeasureOn (Algsuperdiff.Section5.Support.cubeSetAt y n)] fun (x : HCPolySupport.Vec d) => ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (cubeSetAtOneL2 y n)) x

The continuous zero extension of the Dirichlet resolvent of the constant datum agrees almost everywhere on the cube with the L² shifted resolvent of the constant class.

3. The exit-time function of a translated triadic cube

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtExitFunction_coe {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : A.cubeSetAtExitFunction y n ↑x = ⨆ (k : ℕ), ENNReal.ofReal (A.cubeSetAtOneResolvent y n ⟨(↑k + 1)⁻¹, ⋯⟩ x)

The value of the exit-time function of y + □_n at a point of the live space is the supremum along the shifts 1 / (k + 1) of the Dirichlet resolvents of the constant datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtExitFunction_coe_eq_of_isScalarForcedWeakSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (w : HCPolySupport.H10Function (Algsuperdiff.Section5.Support.cubeSetAt y n)) (hw : IsScalarForcedWeakSolution A.a (Algsuperdiff.Section5.Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function) {wRep : HCPolySupport.Vec d → ℝ} (hae : wRep =ᵐ[HCPolySupport.volumeMeasureOn (Algsuperdiff.Section5.Support.cubeSetAt y n)] w.toFun) (hcont : ContinuousOn wRep (Algsuperdiff.Section5.Support.cubeSetAt y n)) {Mb : ℝ} (hMb : 0 ≤ Mb) (hb : ∀ z ∈ Algsuperdiff.Section5.Support.cubeSetAt y n, |wRep z| ≤ Mb) {x : HCPolySupport.Vec d} (hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : A.cubeSetAtExitFunction y n ↑x = ENNReal.ofReal (wRep x)

The exit-time function of a translated triadic cube is the continuous representative of the solution of the constant forcing. The solution is supplied, together with a representative continuous on the cube and a uniform bound for it there; the identification then holds at every point of the open cube.