ExitTimeJointCarrier

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

Two inputs of the per-cell exit-time reading

The one-step Laplace estimate consumes, at each cell, two Dirichlet solutions, their continuous representatives, and the identification of the expected exit time from the cell with the representative of the rough-field solution. Two ingredients of that reading are recorded here: the rough-field solution of the exit-time datum solves the constant forcing in the zero-trace class, with the H¹₀ witness of the Dirichlet condition; and on the good cube event its continuous representative is bounded uniformly on the cube.

Main results

• exists_isScalarForcedWeakSolution_of_isDirichletSolutionAt — the scalar forced weak solution of the exit-time datum.
• abs_isCubeRepresentative_le_of_mem_qEvent — the uniform bound on the cube supplied by the good cube event.

References

• ABK26, the localized exit-time problem of Section 5.2 and the one-step Laplace estimate of Section 5.3.

2. The compactified reading, discharged from the chain

theorem Algsuperdiff.Section5.Provider.exists_isScalarForcedWeakSolution_of_isDirichletSolutionAt {d : ℕ} {a : HCPolySupport.CoeffField d} {y : HCPolySupport.Vec d} {n : ℤ} {u : HCPolySupport.H1Function (Support.cubeSetAt y n)} {i : Fin d} (hu : Support.IsDirichletSolutionAt a y n u (Support.linearAxisDatum i)) : ∃ (w : HCPolySupport.H10Function (Support.cubeSetAt y n)), (∀ (x : HCPolySupport.Vec d), u.toFun x = w.toFun x) ∧ DivergenceFormProcess.Form.IsScalarForcedWeakSolution a (Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 1) w.toH1Function

The rough-field solution of the exit-time datum solves the constant forcing in the zero-trace class, with the H¹₀ witness of the Dirichlet condition.

4. The uniform bound on the cube, and the family of good sites

theorem Algsuperdiff.Section5.Provider.abs_isCubeRepresentative_le_of_mem_qEvent (d : ℕ) (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) (Creg : ℝ) (hCreg : 0 < Creg) : ∃ (gamma0 : ℝ) (Cev : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 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 → ℝ), 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 → ∀ z ∈ Support.cubeSetAt y n, |uRep z| ≤ C * Support.exitTimeScale M n

A uniform bound for the representative of the rough-field solution on a good cube. On the good cube event the exit-time homogenization estimate supplies one continuous representative bounded by C T(3^n) at every point of the cube; by uniqueness of continuous representatives the same bound holds for any representative of the same solution. This is the bound the identification of the exit-time function consumes.