StoppedMomentsCubeMeanValue #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The stopped moments on a triadic cube with the expected exit time carried #
The composed bounds of StoppedMomentsCube.lean discharge the finiteness of the expected exit
time from the cube through the small-contrast route, and therefore carry a global small-contrast
datum in every hypothesis list. The finiteness is the only place that datum is used.
This file restates the same three bounds with the finiteness carried as an explicit binder, at
the one point where it is consumed — the centre of the cube, which is the starting point of the
process. No analytic datum of the coefficient field appears: the statements below assume only
the resolvent carrying the process and its one-point regularity data. Every route that supplies
the finiteness — the small-contrast one of expectedExitTime_cubeSetAt_ne_top and the
coefficient-generic one of expectedExitTime_cubeSetAt_ne_top_stream — instantiates them.
Main results #
abs_integral_eval_exitTimeTrunc_onePointRealExtension_le_cubeSetAt_of_hwfin— the stopped mean.sq_integral_eval_exitTimeTrunc_onePointRealExtension_le_cubeSetAt_of_hwfin— its square.abs_integral_eval_exitTimeTrunc_onePointRealExtension_sub_mul_le_cubeSetAt_of_hwfin— the stopped second moment.
References #
- ABK26, Steps 1 and 3 of the superdiffusive displacement bounds of Section 5.4.
1. The stopped mean #
The stopped mean against the whole-space process on a triadic cube, with the expected exit time carried. A bounded Borel observable vanishing at the centre has stopped mean at most twice its uniform distance to an observable with the exit mean-value property of the cube.
The squared stopped mean on a triadic cube, with the expected exit time carried.
2. The stopped second moment #
The stopped second moment against the whole-space process on a triadic cube, with the expected exit time carried.