ExitTimeCutoffLimit

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

The good-cube exit-time bounds for the full stream field

The exit-time datum problem is -∇·a∇w = 1 on y + □_n with zero boundary values, written here at the linear datum g(x) = x_i e_i, whose divergence is the constant one. The good-cube estimates of the exit-time comparison are proved for the truncated coefficient fields a_L, simultaneously for every L ≥ n on one and the same sample event.

This module lets L → ∞. The truncated solutions converge in L²(y + □_n) to the solution for the full stream field (the coefficient distance is geometric in L and the solution map is Lipschitz in the coefficient), and a bound valid for every large L on the continuous representatives therefore holds at every point of the cube for the continuous representative of the limit. The event, the constants, and the discrete scale exitTimeScale M n are unchanged.

Main results

• exists_isDirichletSolutionAt_linearAxisDatum_streamCoefficient — the exit-time datum problem is solvable for the full field on every cube.
• tendsto_l2_exitTime_cutoff — w_L → w in L²(y + □_n).
• exit_time_bounds_on_good_cube_stream — the two good-cube bounds for the full field's exit-time function, on the same event and with the same constants.

References

• ABK26, the exit-time comparison of Section 5.2, and the passage L → ∞ from the truncated fields a_L to a.

1. Solvability for the full field

theorem Algsuperdiff.Section5.Provider.exists_isDirichletSolutionAt_linearAxisDatum_streamCoefficient {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (i : Fin d) : ∃ (u : HCPolySupport.H1Function (Support.cubeSetAt y n)), Support.IsDirichletSolutionAt (Field.streamCoefficient M.nu omega) y n u (Support.linearAxisDatum i)

The exit-time datum problem for the full stream field. The coefficient field is elliptic on the cube with lower constant ν, and the linear datum is 1/2-Hölder there.

2. The L² limit of the exit-time functions

theorem Algsuperdiff.Section5.Provider.tendsto_l2_exitTime_cutoff {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (i : Fin d) {u : ℤ → HCPolySupport.H1Function (Support.cubeSetAt y n)} {v : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : ∀ (L : ℤ), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField y n (u L) (Support.linearAxisDatum i)) (hv : Support.IsDirichletSolutionAt (Field.streamCoefficient M.nu omega) y n v (Support.linearAxisDatum i)) : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in Support.cubeSetAt y n, ((u L).toFun x - v.toFun x) ^ 2)) Filter.atTop (nhds 0)

w_L → w in L²(y + □_n): the exit-time functions of the truncated fields converge to the exit-time function of the full field.

3. The good-cube bounds for the full field

theorem Algsuperdiff.Section5.Provider.exit_time_bounds_on_good_cube_stream (d : ℕ) (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) (Creg : ℝ) (hCreg : 0 < Creg) : ∃ (gamma0 : ℝ) (Cev : ℝ) (C : ℝ) (c : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 0 < C ∧ 0 < c ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Ioc 0 (1 / 4), ∀ (n : ℤ) (y : HCPolySupport.Vec d) (i : Fin d) (omega : Field.FullSample d M.gamma), ↑omega ∈ Support.qEvent M Creg Cev n y ep → ∀ (u : ℤ → HCPolySupport.H1Function (Support.cubeSetAt y n)) (uRep : ℤ → HCPolySupport.Vec d → ℝ) (v : HCPolySupport.H1Function (Support.cubeSetAt y n)) (vRep : HCPolySupport.Vec d → ℝ) (w : HCPolySupport.H1Function (Support.cubeSetAt y n)) (wRep : HCPolySupport.Vec d → ℝ), (∀ (L : ℤ), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField y n (u L) (Support.linearAxisDatum i)) → (∀ (L : ℤ), Support.IsCubeRepresentative y n (u L) (uRep L)) → Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n v (Support.linearAxisDatum i) → Support.IsCubeRepresentative y n v vRep → Support.IsDirichletSolutionAt (Field.streamCoefficient M.nu omega) y n w (Support.linearAxisDatum i) → Support.IsCubeRepresentative y n w wRep → (∀ x ∈ Support.cubeSetAt y n, wRep x ≤ C * Support.exitTimeScale M n) ∧ (ep ≤ c → ∀ x ∈ Support.cubeSetAt y (n - 1), C⁻¹ * Support.exitTimeScale M n ≤ wRep x)

The good-cube exit-time bounds pass to the full stream field.

On the same event Q(y + □_n, ε) and with the same constants as the truncated statement, the continuous representative of the exit-time function of the full field a = ν I + k is at most C T(3^n) at every point of y + □_n, and at least C⁻¹ T(3^n) at every point of y + □_{n-1} once ε ≤ c. The truncated solutions u_L are required at every scale, and their representatives are the ones the truncated estimate speaks about.