ExitTimeTailStream

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

The early-exit tail of the stream process

The chaining layer produces two estimates at once. The event it controls is the early exit from the cube □_m, and the displacement of the path at the fixed time t is bounded by it, because a path whose position has left the cube has left the cube. The displacement form is the one carried by the reading of the chain at the process of the stream field; the early-exit form, which is the stronger of the two, is carried here.

Nothing beyond the chained estimate changes. The Chernoff conversion and the deterministic optimization of the exponent are stated for the early-exit event itself, so replacing the final inclusion by the identity gives the early-exit tail with the same constants, the same accuracy window and the same regime as the displacement tail.

Main results

• measure_exitTime_le_exp_neg_displacementMinScale_of_oneStepLaplace_on — the printed early-exit tail on a carrier, with the contraction and the discount rate of the collected one-step Laplace estimate.
• measure_exitTime_le_exp_neg_displacementMinScale_streamProcess — the early-exit tail for the process of one sample of the stream field.

References

• ABK26, the one-step Laplace estimate, the chaining and the early-exit estimate of Section 5.3.

1. The printed early-exit tail on a carrier

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_exp_neg_displacementMinScale_of_oneStepLaplace_on {d : ℕ} {alpha : Type u_1} [PseudoMetricSpace alpha] (M : Section3.ABKModel d) (Q : MeasureTheory.Measure (MarkovProcess.ContinuousPath alpha)) (U : Set alpha) {C delta : ℝ} {m n : ℤ} (t : NNReal) (hC : 0 < C) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (ht : 0 < ↑t) (hnm : n ≤ m) (hnLower : 3 ^ n ≤ Support.auxiliaryScaleBound M.nu (Section3.Disorder.cstar M) M.gamma delta (↑t) m) (hnUpper : Support.auxiliaryScaleBound M.nu (Section3.Disorder.cstar M) M.gamma delta (↑t) m < 3 ^ (n + 1)) (hscale : Support.lengthTimeScale M.nu (Section3.Disorder.cstar M) M.gamma (3 ^ n) ≤ 2 * Support.exitTimeScale M n) (hdeltaSmall : 128 * 3 ^ d * delta * earlyExitProfileCost (Section3.Disorder.cstar M) M.gamma ≤ C * earlyExitKappa C.toNNReal C⁻¹.toNNReal) (hlarge : earlyExitBaseScale d ≤ 3 ^ (m - n).toNat) (hchain : Q {eta : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U eta ≤ ↑t} ≤ ENNReal.ofReal (Real.exp ((C * Support.exitTimeScale M n)⁻¹ * ↑t)) * oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal ^ earlyExitChainLength d (m - n).toNat) : Q {eta : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U eta ≤ ↑t} ≤ ENNReal.ofReal (Real.exp (-earlyExitDecayConstant d M.gamma delta (earlyExitKappa C.toNNReal C⁻¹.toNNReal) * Support.displacementMinScale M.nu (Section3.Disorder.cstar M) M.gamma (↑t) m))

Composer-fit printed early-exit tail on a carrier. The chained estimate carries exactly the contraction and the discount rate returned by the collected one-step Laplace estimate, so no exponential-domination input remains for its caller.

2. The early-exit tail of the stream process

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_exp_neg_displacementMinScale_streamProcess (d : ℕ) [NeZero 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), ep ≤ c → ∀ (n m : ℤ), n ≤ m → ∀ (omega : Field.FullSample d M.gamma) (i : Fin d) (Good : Percolation.Site d → Prop) [inst : DecidablePred Good], (∀ (z : Percolation.Site d), Good z ↔ ↑omega ∈ Support.qEvent M Creg Cev n (Support.rescaledLatticePoint n z) ep) → (∀ (N : ℕ) (y : ℕ → Fin d → ℤ), Section3.Provider.Percolation.IsLatticePath y N → y 0 ∈ Section3.Provider.Percolation.cubeAt (m - n).toNat 0 → y N ∉ Section3.Provider.Percolation.cubeAt ((m - n).toNat + 1) 0 → 3 / 4 * 3 ^ (m - n).toNat ≤ ↑(Support.qSiteCount M Creg Cev n ep (Percolation.pathSites N y) ↑omega)) → (∀ (j : Fin (Trace.goodSites ((m - n).toNat + 1) Good).card), HasCubeStreamExitTimeData M n omega i (Support.rescaledLatticePoint n ((Trace.goodSiteEnum ((m - n).toNat + 1) Good) j))) → ∀ (delta : ℝ), 0 < delta → delta ≤ 1 → ∀ (t : NNReal), 0 < ↑t → 3 ^ n ≤ Support.auxiliaryScaleBound M.nu (Section3.Disorder.cstar M) M.gamma delta (↑t) m → Support.auxiliaryScaleBound M.nu (Section3.Disorder.cstar M) M.gamma delta (↑t) m < 3 ^ (n + 1) → Support.lengthTimeScale M.nu (Section3.Disorder.cstar M) M.gamma (3 ^ n) ≤ 2 * Support.exitTimeScale M n → 128 * 3 ^ d * delta * earlyExitProfileCost (Section3.Disorder.cstar M) M.gamma ≤ C * earlyExitKappa C.toNNReal C⁻¹.toNNReal → earlyExitBaseScale d ≤ 3 ^ (m - n).toNat → ∀ x ∈ Metric.closedBall 0 (1 / 2 * 3 ^ (m - 1)), ((Field.streamProcess M omega) ↑x) {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | MarkovProcess.ContinuousPath.exitTime (OnePoint.some '' HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) eta ≤ ↑t} ≤ ENNReal.ofReal (Real.exp (-earlyExitDecayConstant d M.gamma delta (earlyExitKappa C.toNNReal C⁻¹.toNNReal) * Support.displacementMinScale M.nu (Section3.Disorder.cstar M) M.gamma (↑t) m))

The printed early-exit tail for the stream process. The chained estimate of the canonical chain, the auxiliary-scale straddle and the deterministic exponent optimization give the paper's exponential minimum for the probability that the process of the stream field leaves □_m before time t.

Beside the model data, the accuracy and the scales, the statement carries the percolation crossing count, the exit-time analytic data of the full field at every good cell, and the auxiliary-scale straddle. The counting premise of the canonical chain is not carried: it follows from the base-scale threshold the straddle already assumes.