ExitTimeHomogenizationJoint

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

The expected exit time from a good cube

For a bounded domain U the expected exit time w(x) = E_x[τ(U)] of the diffusion is the solution of the Dirichlet problem -∇·a∇w = 1 in U, w = 0 on ∂U. On the good cube event that problem was already compared, at the linear datum g(x) = x_i e_i whose divergence is the constant one, with the homogenized profile w of -σ_n Δ w = 1: the rough-field solution is bounded by C T(3^n) on the whole cube and is at least half the homogenized profile on the inner cube y + □_{n-1}, while the homogenized profile itself is at least T(3^n)/C there.

Combining the two gives the two exit-time estimates of the early-exit bound: a uniform upper bound for the expected exit time on the cube and a uniform lower bound on the inner cube, both at the scale T(3^n) = 3^{2n}/σ_n.

The value w of the expected exit time enters through the hypothesis hident, which says that w is the extended-real reading of the continuous representative of the Dirichlet solution at every point of the cube. That is the identification of the expected exit time with the solution of the Dirichlet problem; it is named here rather than assumed silently, and it is supplied for the process of a coefficient field by the whole-space exit-time identity.

Main results

• exit_time_bounds_on_good_cube — the uniform upper bound on the cube and the uniform lower bound on the inner cube.

References

• ABK26, the exit-time comparison of Section 5.2.

theorem Algsuperdiff.Section5.Provider.exit_time_bounds_on_good_cube (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 ∈ Support.qEvent M Creg Cev n y ep, ∀ (m : ℤ), n ≤ m → ∀ (u v : HCPolySupport.H1Function (Support.cubeSetAt y n)) (uRep vRep : HCPolySupport.Vec d → ℝ) (w : HCPolySupport.Vec d → ENNReal), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu m omega).toCoeffField y n u (Support.linearAxisDatum i) → Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n v (Support.linearAxisDatum i) → Support.IsCubeRepresentative y n u uRep → Support.IsCubeRepresentative y n v vRep → (∀ x ∈ Support.cubeSetAt y n, w x = ENNReal.ofReal (uRep x)) → (∀ x ∈ Support.cubeSetAt y n, w x ≤ ENNReal.ofReal (C * Support.exitTimeScale M n)) ∧ (ep ≤ c → ∀ x ∈ Support.cubeSetAt y (n - 1), ENNReal.ofReal (C⁻¹ * Support.exitTimeScale M n) ≤ w x)

The expected exit time from a good cube. Let w be a function on the cube identified, through hident, with the continuous representative of the Dirichlet solution of -∇·a_m∇u = 1 on y + □_n with zero boundary values. On the good cube event Q(y + □_n, ε) at the constant returned here, w is at most C T(3^n) at every point of the cube, and, once ε is below the threshold c, at least C⁻¹ T(3^n) at every point of the inner cube y + □_{n-1}.