ExitTimeTailModel

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 from the model alone

The early-exit estimate of the chained layer carries the crossing count of the percolation estimate, and asks each cell of the chain for the analytic data of its exit-time problem. Both premises are discharged here, in the two steps the displacement form uses.

The first step supplies the crossing count. A single measurable scale Y serves almost every sample and every smaller cube scale; transporting the successor percolation estimate to the injection constant of the exit-time joint rescales the accuracy parameter by K = max 1 C_ev, which multiplies the lower endpoint of the accuracy window by K and divides the tail rate of the crossing scale by K².

The second step supplies the analytic data of the cells, which exist for every model, every sample, every centre and every cube scale; shrinks the disorder threshold until the accuracy window

  C_floor γ^{1/2} |log γ|^{7/2} ≤ ep ≤ 1/4 ,     ep ≤ c_small

contains a point, that comparison being carried in the conclusion; and transports the almost sure statement from the coefficient cutoff sample to the full sample, which is the form the quenched moment estimates consume.

Main results

• measure_exitTime_le_exp_neg_displacementMinScale_streamProcess_v2 — the early-exit tail of the stream process with the crossing premise supplied.
• measure_exitTime_le_exp_neg_displacementMinScale_streamProcess_v2_of_model — the same, almost surely for the full-sample law, with a nonempty accuracy window and no premise on the cells.

References

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

1. The crossing count supplied

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_exp_neg_displacementMinScale_streamProcess_v2 (d : ℕ) [NeZero d] (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (Cev : ℝ) (Cfloor : ℝ) (Cchain : ℝ) (ctail : ℝ) (csmall : ℝ) (Creg : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 0 < Cfloor ∧ 0 < Cchain ∧ 0 < ctail ∧ 0 < csmall ∧ 0 < Creg ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Icc (Cfloor * √M.gamma * |Real.log M.gamma|.rpow (7 / 2)) (1 / 4), ep ≤ csmall → ∀ (m : ℤ), ∃ (Y : Section3.Cutoff.CutoffSample d → ℕ), Measurable Y ∧ (∀ (N : ℕ), 1 ≤ N → ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | N ≤ Y omega} ≤ ENNReal.ofReal (Real.exp (-(ctail * ep ^ 2 * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) * 3 ^ N)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m - ↑(Y omega), ∀ (omegaFull : Field.FullSample d M.gamma), ↑omegaFull = omega → ∀ (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) → (∀ (j : Fin (Trace.goodSites ((m - n).toNat + 1) Good).card), HasCubeStreamExitTimeData M n omegaFull 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 ≤ Cchain * earlyExitKappa Cchain.toNNReal Cchain⁻¹.toNNReal → earlyExitBaseScale d ≤ 3 ^ (m - n).toNat → ∀ x ∈ Metric.closedBall 0 (1 / 2 * 3 ^ (m - 1)), ((Field.streamProcess M omegaFull) ↑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 Cchain.toNNReal Cchain⁻¹.toNNReal) * Support.displacementMinScale M.nu (Section3.Disorder.cstar M) M.gamma (↑t) m))

The early-exit tail of the stream process with the crossing premise supplied. A single measurable scale serves almost every sample and every smaller cube scale. The rescaling by K = max 1 C_ev weakens the anchor's accuracy floor by the factor K and its exponential rate by the factor K².

2. The cells and the accuracy window supplied

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_exp_neg_displacementMinScale_streamProcess_v2_of_model (d : ℕ) [NeZero d] (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (Cev : ℝ) (Cfloor : ℝ) (Cchain : ℝ) (ctail : ℝ) (csmall : ℝ) (Creg : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 0 < Cfloor ∧ 0 < Cchain ∧ 0 < ctail ∧ 0 < csmall ∧ 0 < Creg ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → Cfloor * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ min (1 / 4) csmall ∧ ∀ ep ∈ Set.Icc (Cfloor * √M.gamma * |Real.log M.gamma|.rpow (7 / 2)) (1 / 4), ep ≤ csmall → ∀ (m : ℤ), ∃ (Y : Section3.Cutoff.CutoffSample d → ℕ), Measurable Y ∧ (∀ (N : ℕ), 1 ≤ N → ↑(Field.fullSampleLaw M) {omegaFull : Field.FullSample d M.gamma | N ≤ Y ↑omegaFull} ≤ ENNReal.ofReal (Real.exp (-(ctail * ep ^ 2 * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) * 3 ^ N)))) ∧ ∀ᵐ (omegaFull : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ∀ n ≤ m - ↑(Y ↑omegaFull), ∀ (_i : Fin d) (Good : Percolation.Site d → Prop) [DecidablePred Good], (∀ (z : Percolation.Site d), Good z ↔ ↑omegaFull ∈ Support.qEvent M Creg Cev n (Support.rescaledLatticePoint n z) ep) → ∀ (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 ≤ Cchain * earlyExitKappa Cchain.toNNReal Cchain⁻¹.toNNReal → earlyExitBaseScale d ≤ 3 ^ (m - n).toNat → ∀ x ∈ Metric.closedBall 0 (1 / 2 * 3 ^ (m - 1)), ((Field.streamProcess M omegaFull) ↑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 Cchain.toNNReal Cchain⁻¹.toNNReal) * Support.displacementMinScale M.nu (Section3.Disorder.cstar M) M.gamma (↑t) m))

The early-exit tail of the stream process, with no premise beyond the model. The crossing count of the percolation estimate and the analytic data of the cells are both supplied, and the disorder threshold is small enough that the accuracy window

  C_floor γ^{1/2}|log γ|^{7/2} ≤ ep ≤ 1/4 ,     ep ≤ c_small

is nonempty; that comparison is the first conjunct of the conclusion. The estimate itself holds almost surely for the full-sample law.

The accuracy rescaling that produced the successor form costs a factor: with K = max 1 C_ev, the floor C_floor is the floor of the percolation estimate at injection constant 1 multiplied by K, and the tail rate c_tail is that estimate's rate divided by K².

The index i no longer occurs in the conclusion, the premise that used it having been discharged; the statement is the one the successor form has at every index.