EarlyExitModel

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

The early-exit probability and the diffusivity profile at the confinement scale

The quenched displacement-moment composition reads two of its inputs at the random confinement scale of one sample: the probability that the process leaves the cube □_{m_t} before time t, and the closeness of the running diffusivity to the intrinsic scale. Both are supplied here.

The confinement scale is the least scale n with L (1 + S_n) ≤ 3^n, where the deterministic factor is L = K |log γ|^{1/2} R(t). Two consequences of that inequality are used. The first is purely deterministic: 3^{m_t} is at least K |log γ|^{1/2} R(t), so the two-branch minimum M(t, m_t) of the displacement estimate is at least K² |log γ|, and an exponential of -c M(t, m_t) is therefore at most γ^{cK²}; choosing K with 100 ≤ c K² turns that into γ^{100}. The second is the scale arithmetic of the intrinsic-scale comparison, which the profile bound inherits with one factor of the dimension.

Main results

• sq_le_displacementMinScale_of_isConfinementScale — the deterministic lower bound K² |log γ| ≤ M(t, m_t) at a confinement scale.
• exp_neg_mul_displacementMinScale_le_pow_of_isConfinementScale — the exponential of the displacement minimum at a confinement scale is at most γ^{100}.
• ae_isConfinementScale_confinementScale_fullSample — the chosen confinement scale is almost surely a confinement scale, for the law of the full sample.
• abs_mul_intrinsicScale_sq_sub_mul_le_of_isConfinementScale and abs_mul_intrinsicScale_sq_sub_mul_le_confinementScale — the diffusivity profile comparison at a confinement scale and at the chosen confinement scale.

References

• ABK26, the superdiffusive displacement bounds of Section 5.4.

1. The displacement minimum at a confinement scale

theorem Algsuperdiff.Section5.Provider.sq_le_displacementMinScale_of_isConfinementScale {nu cstar gamma t K L : ℝ} {Stilde : ℤ → ENNReal} {m : ℤ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (hgc : gamma ≤ cstar) (ht : 0 < t) (hK : 1 ≤ K) (hKL : K * √|Real.log gamma| * Support.intrinsicScale nu cstar gamma t ≤ L) (hm : Support.IsConfinementScale Stilde L m) : K ^ 2 * |Real.log gamma| ≤ Support.displacementMinScale nu cstar gamma t m

The displacement minimum is large at a confinement scale. The defining inequality of the confinement scale puts 3^{m_t} above the deterministic factor K |log γ|^{1/2} times the intrinsic scale, and the intrinsic-scale comparison of the two branches of the minimum then reads that ratio squared inside M(t, m_t).

theorem Algsuperdiff.Section5.Provider.exp_neg_mul_displacementMinScale_le_pow_of_isConfinementScale {nu cstar gamma t K L c : ℝ} {Stilde : ℤ → ENNReal} {m : ℤ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (hgc : gamma ≤ cstar) (ht : 0 < t) (hK : 1 ≤ K) (hc : 0 ≤ c) (hcK : 100 ≤ c * K ^ 2) (hKL : K * √|Real.log gamma| * Support.intrinsicScale nu cstar gamma t ≤ L) (hm : Support.IsConfinementScale Stilde L m) : Real.exp (-c * Support.displacementMinScale nu cstar gamma t m) ≤ gamma ^ 100

The exponential of the displacement minimum at a confinement scale. With 100 ≤ c K² the exponential rate c M(t, m_t) is at least 100 |log γ|.

2. The early-exit probability at the confinement scale

theorem Algsuperdiff.Section5.Provider.ae_isConfinementScale_confinementScale_fullSample {d : ℕ} (M : Section3.ABKModel d) {S : ℤ → Section3.Cutoff.CutoffSample d → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) {C p L : ℝ} (hC : 0 ≤ C) (hp : 1 ≤ p) (hL : 0 < L) (hmom : ∀ (k : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S k omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal C ^ p) : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), Support.IsConfinementScale (fun (n : ℤ) => Support.widenedScale (fun (k : ℤ) => S k ↑omega) n) L (Support.confinementScale S L ↑omega)

The confinement scale is almost surely a confinement scale, for the full sample. The law of the full sample pushes forward to the law of the coefficient cutoff sample, so one uniform moment bound on the displacement scales gives the statement there.

3. The diffusivity profile at the confinement scale

theorem Algsuperdiff.Section5.Provider.abs_mul_intrinsicScale_sq_sub_mul_le_of_isConfinementScale (d : ℕ) {nu cstar gamma t K : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (ht : 0 < t) (hK : 1 ≤ K) {Stilde : ℤ → ENNReal} {m : ℤ} (hm : Support.IsConfinementScale Stilde (K * √|Real.log gamma| * Support.intrinsicScale nu cstar gamma t) m) {sigmaBar C : ℝ} (hsigma : 0 < sigmaBar) (hC : 0 ≤ C) (hsmall : C * √gamma * |Real.log gamma| ≤ 1 / 2) (hprofile : |sigmaBar - Support.effectiveDiffusivity nu cstar gamma (3 ^ m)| ≤ C * √gamma * |Real.log gamma| * sigmaBar) : |↑d * Support.intrinsicScale nu cstar gamma t ^ 2 - ↑d * (sigmaBar * t)| ≤ ↑d * (1 + 2 * C) * √gamma * |Real.log gamma| * (3 ^ m) ^ 2

The profile comparison in the dimensional form. The scale arithmetic at the confinement scale, multiplied by the dimension; the constant is d (1 + 2C), where C is the relative error of the renormalized diffusivity.

theorem Algsuperdiff.Section5.Provider.abs_mul_intrinsicScale_sq_sub_mul_le_confinementScale {d : ℕ} (M : Section3.ABKModel d) {cstar t K L C : ℝ} (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (sigmaBar : ℤ → ℝ) (hcstar : 0 < cstar) (ht : 0 < t) (hK : 1 ≤ K) (hL : L = K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) (hsigma : ∀ (n : ℤ), 0 < sigmaBar n) (hC : 0 ≤ C) (hsmall : C * √M.gamma * |Real.log M.gamma| ≤ 1 / 2) (hprofile : ∀ (n : ℤ), |sigmaBar n - Support.effectiveDiffusivity M.nu cstar M.gamma (3 ^ n)| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBar n) (hconf : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), Support.IsConfinementScale (fun (n : ℤ) => Support.widenedScale (fun (k : ℤ) => S k ↑omega) n) L (Support.confinementScale S L ↑omega)) : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), |↑d * Support.intrinsicScale M.nu cstar M.gamma t ^ 2 - ↑d * (sigmaBar (Support.confinementScale S L ↑omega) * t)| ≤ ↑d * (1 + 2 * C) * √M.gamma * |Real.log M.gamma| * (3 ^ Support.confinementScale S L ↑omega) ^ 2

The profile comparison at the chosen confinement scale. The renormalized diffusivities of the scales, read at the confinement scale of the sample.