HomogenizedExitTime #

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

The homogenized exit time on a cube #

The comparator problem of Section 5.1 at the linear datum g(x) = x_i e_i is the homogenized exit-time problem

  -σ_n Δ w = 1  in y + □_n ,      w = 0  on ∂(y + □_n) ,

and exitTimeScale is the pre-T_r expression 3^{2n}/σ_n from display (5.7). The conversion using (1 ± C γ^{1/2}|log γ|) to the definition of T_r is deferred. This module proves that w and this scale are comparable, with a dimensional constant:

  C^{-1} ‖w‖_{L^∞(y+□_n)} ≤ T(3^n) ≤ C inf_{x ∈ y+□_{n-1}} w(x) .

The upper bound is the gradient bound of the comparator, which the interior Schauder estimate supplies at the datum g in the form ‖∇w‖_∞ ≤ C σ_n^{-1}3^n, together with the zero boundary values: a zero-trace function with a bounded gradient is bounded by the gradient bound times half the side length. The lower bound includes the coordinate sum and is d · Ksup · 3^n / 2. The lower bound is the comparison with a bump barrier of height T(3^n)/K supported strictly inside the cube and constant on a ball containing the inner cube.

Both bounds are stated for an arbitrary solution of the comparator problem and an arbitrary representative of it continuous on the cube: the solution is unique away from a null set, and its continuous representative is then unique at every point of the cube, so the two sides do not depend on either choice.