EarlyExitConfinementModel

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

The early-exit probability at the confinement scale, from the model alone

The early-exit estimate of the stream field holds at a pair of scales n ≤ m under a list of conditions: an accuracy inside the window of the percolation estimate, the crossing scale Y_m below m - n, the auxiliary-scale straddle at n, the comparison of the two time scales at n, a smallness condition on the separation parameter, and a lower bound on m - n. Every one of them is met here at the random confinement scale m_t, once the displacement scales are taken to be those of the crossing scales.

Two features of the confinement scale do the work. The first is that the defining inequality L (1 + S_{m_t}) ≤ 3^{m_t} bounds the displacement scale at m_t by the two-branch minimum M(t, m_t), which is the hypothesis of the auxiliary-scale comparison; the deterministic factor L = K |log γ|^{1/2} R(t) leaves a margin of K² |log γ| in that comparison, and choosing K with 3^k ≤ K² converts the margin into n ≤ m_t - Y - k, which is the lower bound on m_t - n. The second is that the same margin makes the exponential of -c M(t, m_t) at most γ^{100} once 100 ≤ c K².

The order of the choices is therefore: the constants of the chained estimate first, then the separation parameter δ from the smallness condition, then the exponential rate c = earlyExitDecayConstant d γ δ κ, and only then the constant K of the confinement scale, which has to satisfy both 100 ≤ c K² and 3^k ≤ K².

Main results

• displacementScale_add_le_displacementMinScale_of_isConfinementScale — the displacement scale at a confinement scale, shifted by a triadic factor below K².

exists_ae_confinement_exitTime_bound_of_threshold — the early-exit tail of the stream process at and above the random confinement scale, together with the moment field of the displacement scales, above a prescribed lower bound on the confinement constant.

• measureReal_compl_survivalEvent_confinementScale_le_pow_of_exitTail_at_confinementScale — the early-exit probability at the confinement scale, from that tail.

References

• ABK26, the early-exit estimate of Section 5.3 and the superdiffusive displacement bounds of Section 5.4.

1. The displacement scale at a confinement scale, with a margin

theorem Algsuperdiff.Section5.Provider.displacementScale_add_le_displacementMinScale_of_isConfinementScale {nu cstar gamma delta t K : ℝ} {Y : ℤ → ℕ} {m r : ℤ} {j : ℕ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (hgc : gamma ≤ cstar) (hdelta : 0 < delta) (ht : 0 < t) (hK : 1 ≤ K) (hjK : 3 ^ j ≤ K ^ 2) (hm : Support.IsConfinementScale (fun (n : ℤ) => Support.widenedScale (fun (i : ℤ) => Support.displacementScale delta gamma (Y i)) n) (K * √|Real.log gamma| * Support.intrinsicScale nu cstar gamma t) m) (hmr : m ≤ r) : Support.displacementScale delta gamma (Y r + j) ≤ Support.displacementMinScale nu cstar gamma t r

The displacement scale at and above a confinement scale, with a triadic margin. The defining inequality of the confinement scale bounds L S_r 3^{-2(r - m)} by 3^m at every scale r above the confinement scale m, so the ratio between the two-branch minimum M(t, r) and the displacement scale at r is at least K² |log γ| ≥ K². Any triadic factor below K² may therefore be absorbed into the comparison, uniformly in r ≥ m.

2. The rate of the crossing tail

3. The early-exit tail at the confinement scale

theorem Algsuperdiff.Section5.Provider.exists_ae_confinement_exitTime_bound_of_threshold (d : ℕ) [NeZero d] (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (Cscale : ℝ) (CSbar : ℝ) (Kbar : ℝ) (cbar : ℝ), 0 < gamma0 ∧ 1 ≤ Cscale ∧ 1 ≤ CSbar ∧ 1 ≤ Kbar ∧ 0 < cbar ∧ cbar ≤ 1 ∧ gamma0 ≤ cstar ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (t : ℝ), 0 < t → ∀ (Kmin : ℝ), ∃ (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (K : ℝ) (L : ℝ) (c : ℝ) (CS : ℝ) (pS : ℝ), 1 ≤ K ∧ Kmin ≤ K ∧ 0 < c ∧ c ≤ 1 ∧ cbar ≤ c ∧ 100 ≤ c * K ^ 2 ∧ L = K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t ∧ (∃ (delta : ℝ) (Y : ℤ → Section3.Cutoff.CutoffSample d → ℕ), 0 < delta ∧ delta ≤ 1 ∧ (∀ (i : ℤ), Measurable (Y i)) ∧ ∀ (i : ℤ) (omega : Section3.Cutoff.CutoffSample d), S i omega = Support.displacementScale delta M.gamma (Y i omega)) ∧ (∀ (n : ℤ), Measurable (S n)) ∧ (∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ S n omega) ∧ 1 ≤ CS ∧ 1 ≤ pS ∧ CS ≤ CSbar ∧ K ≤ max Kbar Kmin ∧ Cscale⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) ≤ pS ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ pS → (∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (4 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (4 * p)) ∧ ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (8 * 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)) ∧ ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ∀ (k : ℤ), Support.confinementScale S L ↑omega ≤ k → ((Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | MarkovProcess.ContinuousPath.exitTime (OnePoint.some '' Support.cubeSetAt 0 k) eta ≤ ↑t.toNNReal} ≤ ENNReal.ofReal (Real.exp (-c * Support.displacementMinScale M.nu cstar M.gamma t k))

The early-exit tail of the stream process at and above the random confinement scale, with uniform constants. The displacement scales of the crossing scales of the percolation estimate determine a confinement scale, and at every scale above it each condition of the chained early-exit estimate is met: the accuracy lies in the window, which the model form shows nonempty; the crossing-scale condition and the lower bound on the scale gap come from the defining inequality of the confinement scale through the auxiliary-scale comparison; the auxiliary scale is the triadic scale straddling the quantity the estimate names; the comparison of the two time scales is a theorem about the model; and the separation parameter is chosen below the smallness threshold.

The returned exponential rate c and confinement constant K satisfy 100 ≤ c K², which is what turns the tail into the bound γ^{100} at the confinement scale itself. Every requirement on K in the argument is a lower bound, so an arbitrary threshold Kmin may be imposed on it at no cost; the returned K is above it.

The separation parameter is chosen against a bound for the profile cost that holds at every admissible disorder, so it does not depend on the model; this is what makes the four constants below uniform. Three of them are returned before the model and the time:

• Cscale, with Cscale⁻¹ γ^{-1} |log γ|^{-6} ≤ pS, so that a caller whose range of exponents is prescribed in that shape can meet p ≤ pS. The statement does not identify pS; it identifies a lower bound for it, which is all a caller consumes.
• CSbar, with CS ≤ CSbar, and Kbar, with K ≤ max Kbar Kmin. A constant built from CS and K and increasing in both — the component constant of the annealed bound is one — can therefore be fixed before the model.
• cbar, with 0 < cbar ≤ c and cbar ≤ 1: the exponential rate is bounded below by κ δ² / (192 · 3^d), because δ ≤ 1 and the exponent 1/(1-γ) is at most 2. A caller that must fix the rate before the model can use cbar and weaken the tail to it.

The accuracy is taken at the top of its window rather than at the floor, so the rate of the crossing tail is c_tail ep² γ^{-1} |log γ|^{-6} at a value of ep that does not shrink with the disorder. Integrating that tail bounds the moments of the displacement scales of order at most 8 pS by one constant CS ≥ 1, uniformly in the order and in the scale.

4. The early-exit probability at the confinement scale

theorem Algsuperdiff.Section5.Provider.measureReal_compl_survivalEvent_confinementScale_le_pow_of_exitTail_at_confinementScale {d : ℕ} [NeZero d] (M : Section3.ABKModel d) {cstar t K L c : ℝ} (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (hcstar : 0 < cstar) (hgc : M.gamma ≤ cstar) (ht : 0 < t) (hK : 1 ≤ K) (hc : 0 ≤ c) (hcK : 100 ≤ c * K ^ 2) (hKL : K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t ≤ L) (hconf : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), Support.IsConfinementScale (fun (n : ℤ) => Support.widenedScale (fun (i : ℤ) => S i ↑omega) n) L (Support.confinementScale S L ↑omega)) (hexitTail : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ((Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | MarkovProcess.ContinuousPath.exitTime (OnePoint.some '' Support.cubeSetAt 0 (Support.confinementScale S L ↑omega)) eta ≤ ↑t.toNNReal} ≤ ENNReal.ofReal (Real.exp (-c * Support.displacementMinScale M.nu cstar M.gamma t (Support.confinementScale S L ↑omega)))) : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), (((Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) (DivergenceFormProcess.StoppedDirichlet.survivalEvent (OnePoint.some '' Support.cubeSetAt 0 (Support.confinementScale S L ↑omega)) t.toNNReal)ᶜ).toReal ≤ M.gamma ^ 100

The early-exit probability at the confinement scale, from the tail at that scale. The exit-time tail of the stream process read at the random confinement scale, together with the confinement inequality, bounds the probability that the process started at the origin has left □_{m_t} by time t by γ^{100}.

The tail is carried as the named hypothesis hexitTail, in the form the chained estimate produces at the confinement scale: at the exponential rate c and the two-branch displacement minimum, on the cube at the origin. The only requirement on the constant K of the deterministic factor is 100 ≤ c K².