ExitTimeCutoffLimitTailData #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The exit-time analytic data of a cell #
The per-cell exit-time joint of the full stream field asks each cell for six objects: the solution of the exit-time datum problem for the full field with its continuous representative, the solutions of the same problem for the truncated fields at every truncation scale with their representatives, and the constant-coefficient comparator solution with its representative.
All six are produced here, for every model, every sample, every centre and every cube scale. Solvability is unconditional for each of the three coefficient fields, and each of the three has a positive scalar symmetric part with a continuous skew part, which is exactly what the interior estimate needs to turn a solution into a function continuous on the open cube. Neither the good cube event nor a bound on the solution enters.
The consequence is that the per-cell analytic data need not be carried as a hypothesis by the statements that consume them: what they carried is a theorem about the model.
Main results #
hasCubeStreamExitTimeData— every cell carries the exit-time analytic data of the full stream field.
References #
- ABK26, the localized exit-time problem of Section 5.2, the one-step Laplace estimate and the displacement tail of Section 5.3.
1. Every cell carries the exit-time analytic data #
The exit-time analytic data of a cell exist. The exit-time datum problem is solvable on
y + □_n for the full stream field, for the truncated field at every truncation scale and for
the constant comparator; and each of those three coefficient fields has the structure that
produces a representative continuous on the open cube. No event, no smallness and no bound on a
solution is used, so the datum holds at every centre, every cube scale and every sample.