StreamExitTimeH10

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

The expected exit time from a triadic cube as a zero-trace Sobolev function

The corrected observable of the stopped second-moment bound is the weakly harmonic observable less a multiple of the expected exit time from the cube. To compare it with the homogenized datum through the renormalization estimate, the expected exit time has to be read as an H¹ function of the cube solving -∇ · a ∇w = 1 weakly with zero trace, at every point.

The analytic object is the Green potential of the constant datum on the cube: the zero-shift limit of the Dirichlet resolvents of one, which is bounded, continuous on the cube, vanishes off it, and has an exact zero-trace representative solving the constant forcing. The process object is identified with it through the exit-time identity of the stream chain and the identification of the exit-time function of the cube with any bounded continuous zero-trace solution of the constant forcing.

Main definitions

• streamExitFunction — the Green potential of the constant datum on y + □_n for the stream field.
• streamExitH10 — its exact zero-trace H¹ representative.

Main results

• isScalarForcedWeakSolution_streamExitH10 — the representative solves -∇ · a ∇w = 1.
• toReal_expectedExitTime_cubeSetAt_eq_stream — at every point of the compactified state space, the expected exit time of the stream process from the cube is the exit function, read through the one-point extension.

References

• ABK26, the localized exit-time problem of Section 5.2 and Step 3 of Section 5.4.

1. The exit function of a triadic cube

theorem Algsuperdiff.Section5.Provider.abs_one_datum_le {d : ℕ} (x : HCPolySupport.Vec d) : |(fun (x : HCPolySupport.Vec d) => 1) x| ≤ 1

The constant datum of the exit-time problem is bounded by one.

noncomputable def Algsuperdiff.Section5.Provider.streamExitFunction {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) : HCPolySupport.Vec d → ℝ

The exit function of y + □_n for the stream field: the Green potential of the constant datum, that is, the zero-shift limit of the Dirichlet resolvents of one on the cube.

Equations

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

noncomputable def Algsuperdiff.Section5.Provider.streamExitH10 {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) : HCPolySupport.H10Function (Support.cubeSetAt y n)

The exact zero-trace H¹ representative of the exit function.

Equations

• Algsuperdiff.Section5.Provider.streamExitH10 M omega y n = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).partGreenH10 ⋯ ⋯ ⋯ ⋯

theorem Algsuperdiff.Section5.Provider.streamWholeSpaceAnalyticData_a {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) : (Field.streamWholeSpaceAnalyticData M omega).a = Field.streamCoefficient M.nu omega

The coefficient field of the stream analytic data is the stream coefficient.

theorem Algsuperdiff.Section5.Provider.streamExitH10_toFun {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) : (streamExitH10 M omega y n).toFun = streamExitFunction M omega y n

theorem Algsuperdiff.Section5.Provider.isScalarForcedWeakSolution_streamExitH10 {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) : DivergenceFormProcess.Form.IsScalarForcedWeakSolution (Field.streamWholeSpaceAnalyticData M omega).a (Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 1) (streamExitH10 M omega y n).toH1Function

The representative solves -∇ · a ∇w = 1 weakly on the cube.

theorem Algsuperdiff.Section5.Provider.streamExitFunction_of_notMem {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∉ Support.cubeSetAt y n) : streamExitFunction M omega y n x = 0

theorem Algsuperdiff.Section5.Provider.streamExitFunction_nonneg {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : 0 ≤ streamExitFunction M omega y n x

theorem Algsuperdiff.Section5.Provider.abs_streamExitFunction_le {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : |streamExitFunction M omega y n x| ≤ 1 * (Field.streamWholeSpaceAnalyticData M omega).partTorsionBound ⋯

theorem Algsuperdiff.Section5.Provider.continuousOn_streamExitFunction {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) : ContinuousOn (streamExitFunction M omega y n) (Support.cubeSetAt y n)

2. The identification with the expected exit time of the stream process

theorem Algsuperdiff.Section5.Provider.expectedExitTime_cubeSetAt_eq_streamExitFunction {d : ℕ} [NeZero d] {M : Section3.ABKModel d} {omega : Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ Support.cubeSetAt y n) : DivergenceFormProcess.StoppedDirichlet.expectedExitTime R.onePointKernelSemigroup ⋯ (OnePoint.some '' Support.cubeSetAt y n) ↑x = ENNReal.ofReal (streamExitFunction M omega y n x)

The expected exit time from the cube is the exit function, at every point of the cube.

theorem Algsuperdiff.Section5.Provider.toReal_expectedExitTime_cubeSetAt_eq_stream {d : ℕ} [NeZero d] {M : Section3.ABKModel d} {omega : Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) (z : OnePoint (HCPolySupport.Vec d)) : (DivergenceFormProcess.StoppedDirichlet.expectedExitTime R.onePointKernelSemigroup ⋯ (OnePoint.some '' Support.cubeSetAt y n) z).toReal = DivergenceFormProcess.Form.onePointRealExtension (streamExitFunction M omega y n) z

The expected exit time from the cube, at every point of the compactified state space. At a point of the cube it is the exit function; off the cube, and at infinity, both vanish.