ExitTimeHomogenization

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

Homogenization of the exit-time problem on a good cube

On the intersection of the good cube event and the large-scale event, the injection estimate applied at the linear datum g(x) = x_i e_i compares the rough-field solution of -∇·a_m∇w = 1 on y + □_n with the homogenized profile w of -σ_n Δ w = 1. Inserting the two inputs of the previous modules — the Hölder bound [g]_{C^{0,1/2}(y+□_n)} ≤ 3^{n/2} and the two-sided comparison of w with the time scale T(3^n) = 3^{2n}/σ_n — turns the normalized estimate

  σ_n 3^{-n} ‖w - w‖_{L^∞(y+□_n)} ≤ C ε 3^{n/2} [g]_{C^{0,1/2}(y+□_n)}

into ‖w - w‖_{L^∞(y+□_n)} ≤ C ε T(3^n), and then, once ε is below the threshold c(d,c⋆,C_reg) returned by the injection estimate, into the two-sided comparison ½ w ≤ w ≤ 2 w on the inner cube y + □_{n-1} and the uniform bound ‖w‖_{L^∞(y+□_n)} ≤ C T(3^n).

The L^∞ norm of the difference is the honest essential supremum of the two Sobolev functions. The pointwise statements are read through continuous representatives: the injection estimate's regularity clause bounds the 1/2-Hölder seminorm of a continuous representative of the rough-field solution by a finite quantity at this datum, so such a representative exists, and it is unique at every point of the cube.

Main results

• exit_time_homogenization_on_good_cube.

References

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

theorem Algsuperdiff.Section5.Provider.exit_time_homogenization_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.goodCubeEvent M Creg n y ep ∩ Support.largeScaleEvent M n y (Cev⁻¹ * ep * (√M.gamma)⁻¹), ∀ (m : ℤ), n ≤ m → ∀ (u v : HCPolySupport.H1Function (Support.cubeSetAt y n)) (vRep : HCPolySupport.Vec d → ℝ), 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 v vRep → MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.toFun x - v.toFun x) ⊤ (MeasureTheory.volume.restrict (Support.cubeSetAt y n)) ≤ ENNReal.ofReal (C * ep * Support.exitTimeScale M n) ∧ ∃ (uRep : HCPolySupport.Vec d → ℝ), Support.IsCubeRepresentative y n u uRep ∧ (∀ x ∈ Support.cubeSetAt y n, |uRep x - vRep x| ≤ C * ep * Support.exitTimeScale M n) ∧ (∀ x ∈ Support.cubeSetAt y n, |uRep x| ≤ C * Support.exitTimeScale M n) ∧ (ep ≤ c → ∀ x ∈ Support.cubeSetAt y (n - 1), 1 / 2 * vRep x ≤ uRep x ∧ uRep x ≤ 2 * vRep x)

Homogenization of the exit-time problem on a good cube. On the event of the injection estimate, the rough-field solution of -∇·a_m∇w = 1 on y + □_n is within C ε T(3^n) of the homogenized profile in the uniform norm, is bounded by C T(3^n), and, once ε is below the threshold c(d,c⋆,C_reg) returned by the injection estimate, is between half and twice the homogenized profile on the inner cube.