OnePointChainStreamFull

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

The displacement tail for the process of the stream field, from the full field's cell problems

The chaining layer of OnePointChainTrace and the printed optimization of OnePointChainPrinted are read here at the process the model produces, with the per-cell exit-time joint taken for the full stream field. Every input the chain asks about the process is supplied by the model: the resolvent is the split-skew analytic resolvent, its regularity datum is the shift-dependent exhaustion-tail input, conservativity of the live kernel semigroup and the bounded-measurable identification are the model's own theorems, and the operator identification holds by definition.

Two hypotheses of the earlier reading disappear here. The small-contrast datum of the stream field is gone, because the exit-time identity used is the one proved directly from the localized split-skew barrier. The compatibility of the stream coefficient with a truncated field is gone, because the cell problems are now posed for the stream coefficient itself. In particular one sample of the full field, rather than a sample of the full field together with an unrelated truncation sample, determines both the process and the cells.

Main results

• earlyExitTraceCount_pos_of_earlyExitBaseScale_le — the counting premise of the canonical chain length follows from the base-scale threshold of the printed optimization.
• measure_exitTime_le_canonicalChain_of_percolation_crossing_streamProcess — the chained early-exit estimate for the stream process at the canonical chain length.

References

• ABK26, the one-step Laplace estimate, the chaining and the displacement tail of Section 5.3.

1. The counting premise of the canonical chain

theorem Algsuperdiff.Section5.Provider.earlyExitTraceCount_pos_of_earlyExitBaseScale_le (d k : ℕ) (h : earlyExitBaseScale d ≤ 3 ^ k) : 0 < earlyExitTraceCount d k

The base-scale threshold already forces a usable trace count. At 3^k above 64 (d + 1 + 3^d) the number of trace sites left after discarding the 2 d sites of the two endpoints is positive, which is the premise the canonical chain length needs.

2. The chained early-exit estimate

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_canonicalChain_of_percolation_crossing_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)) → 0 < earlyExitTraceCount d (m - n).toNat → (∀ (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))) → ∀ x ∈ Metric.closedBall 0 (1 / 2 * 3 ^ (m - 1)), ∀ (t : NNReal), ((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 ((C * Support.exitTimeScale M n)⁻¹ * ↑t)) * oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal ^ earlyExitChainLength d (m - n).toNat

The chained early-exit estimate for the stream process. At one sample of the full field and one nonnegative cube scale n ≤ m, the crossing count of the annulus at index m - n, the counting premise of the canonical chain length and the exit-time analytic data of the full field at every good cell give the tail bound for the process of the stream field, at the discount rate (C T(3^n))⁻¹ and the one-step contraction factor.

No hypothesis about a resolvent, a small-contrast datum, or a truncated coefficient field appears.