ExitTimeJointStream #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-cell exit-time joint of the full stream field #
The one-step Laplace estimate consumes, at each cell, the expected exit time of the process from
that cell, identified with the continuous representative of the solution of the exit-time datum
problem -∇·a∇w = 1 on the cell. The coefficient field a of that problem must be the field the
process itself carries. For the process of one realization of the stream field that is the full
field ν I + k, not a truncation of it: the truncated fields and the full field have different
Dirichlet solutions, and only their limit as the truncation scale grows is the full field's
solution.
This file states the per-cell joint for the full field and discharges it on the one-point compactification. The analytic side of the cell is the exit-time datum problem for the full field, together with the truncated solutions and the comparator solution that the good-cube estimates compare it with; the process side is the exit-time identity of the stream crux chain, composed with the identification of the exit-time function with the continuous representative.
Main definitions #
IsCubeStreamExitTimeData— the analytic data of one cell for the full field.HasCubeStreamExitTimeData— its existential form.IsCubeExitTimeSolutionDataStream— the per-cell joint on a general carrier.
Main results #
abs_isCubeRepresentative_stream_le_of_mem_qEvent— the two-sided bound for the full field's exit-time function on a good cube.exit_time_exponential_moment_on_good_cube_stream— the exit-time bounds and the normalized exponential moment, from the joint.isCubeExitTimeSolutionDataStream_onePoint_of_mem_qEvent— the joint on the one-point compactification, from the analytic data and the inputs of the stream crux chain.
References #
- ABK26, the localized exit-time problem of Section 5.2 and the one-step Laplace estimate of Section 5.3.
1. The analytic data of one cell #
The exit-time analytic data of one cell for the full stream field. The solution w of
the exit-time datum problem for the full field ν I + k on y + □_n, its continuous
representative wRep, and the two families the good-cube estimates compare it with: the
solutions of the same problem for the truncated fields at every scale, with their representatives,
and the solution of the constant-coefficient comparator problem with its representative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cell carries exit-time analytic data for the full stream field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2. The per-cell joint #
The solution data of one cell for the full stream field, read on a general carrier. At
the centre y and cube scale n: a solution of the exit-time datum problem for the full field
with its continuous representative and the comparison data, together with the identification of
the expected exit time from U at the reading of a point of the cube with the representative.
The set U is required to be open and to carry no starting point other than the readings of
points of the cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The two-sided bound on a good cube #
The full field's exit-time function is bounded on a good cube. The truncated solutions
obey the two-sided bound |u_L| ≤ C T(3^n) on the cube at every truncation scale above the cube
scale, and both halves survive the L² limit, so the same bound holds for the continuous
representative of the full field's solution.
4. The exit-time bounds and the exponential moment, from the joint #
The exponential moment of the exit time from a good cube, for the full stream field. The
process enters only through the joint: the expected exit time from U at the reading of a point
of the cube is the continuous representative of the full field's exit-time function there. On
the good cube event the expected exit time is then at most C T(3^n) from every starting point,
at least C⁻¹ T(3^n) from every point of the inner cube once the accuracy is below the returned
threshold, and the exponential moment of τ(U)/(C T(3^n)) is at most 2.
5. The joint on the one-point compactification #
The compactified reading of the per-cell joint, from the stream crux chain. The chain's exit-time identity for the process of the stream field's split-skew resolvent equals the exit-time function of the cube, and the exit-time function of the cube is the continuous representative of the full field's exit-time solution wherever that representative is bounded. No small-contrast datum and no compatibility of the field with a truncation are used.
The compactified per-cell joint on a good cube. The uniform bound the identification of the exit-time function needs is the two-sided good-cube bound, so on the good cube event the analytic data of the cell alone produce the joint.