OnePointChainPrinted

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

The printed early-exit and displacement tails, on a carrier

The deterministic optimization of the early-exit exponent is arithmetic in the model constants and does not see the process at all. What does see the process is the two measure-theoretic steps around it: the Chernoff conversion of the chained Laplace estimate, and the inclusion of the displacement event in the early-exit event.

Both are restated here for a process of a carrier in which the state space is read by a map with a left inverse. The Chernoff step is an inequality between measures of one and the same event and transfers verbatim. The inclusion is deterministic: if the reading of the path's position at time t has reached the cube radius, the path is no longer in the read cube, since the reading of a point of the cube is retracted back to that point. A path whose position is read outside the cube has left the read cube by that time.

Main results

• measure_exitTime_le_exp_sub_of_canonicalChain_on — the Chernoff step on a carrier.
• measure_norm_ge_le_measure_exitTime_le_retract — the displacement inclusion through a retraction.
• measure_exitTime_le_exp_neg_displacementMinScale_on — the printed form.

References

• ABK26, the early-exit and displacement estimates of Section 5.3.

1. The Chernoff step

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_exp_sub_of_canonicalChain_on {alpha : Type u_1} [PseudoMetricSpace alpha] (Q : MeasureTheory.Measure (MarkovProcess.ContinuousPath alpha)) (U : Set alpha) (t : NNReal) (lam kappa : ℝ) (rho : ENNReal) (N : ℕ) (hexit : Q {eta : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U eta ≤ ↑t} ≤ ENNReal.ofReal (Real.exp (lam * ↑t)) * rho ^ N) (hrho : rho ≤ ENNReal.ofReal (Real.exp (-kappa))) : Q {eta : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U eta ≤ ↑t} ≤ ENNReal.ofReal (Real.exp (lam * ↑t - kappa * ↑N))

The chained estimate in its unconditional Chernoff-exponent form, for an arbitrary law on the continuous paths of the carrier.

2. The displacement inclusion through a retraction

theorem Algsuperdiff.Section5.Provider.measure_norm_ge_le_measure_exitTime_le_retract {d : ℕ} {alpha : Type u_1} [PseudoMetricSpace alpha] (Q : MeasureTheory.Measure (MarkovProcess.ContinuousPath alpha)) (emb : HCPolySupport.Vec d → alpha) (ret : alpha → HCPolySupport.Vec d) (hret : ∀ (z : HCPolySupport.Vec d), ret (emb z) = z) (m : ℤ) (t : NNReal) : Q {eta : MarkovProcess.ContinuousPath alpha | 1 / 2 * 3 ^ m ≤ ‖ret (eta t)‖} ≤ Q {eta : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime (emb '' HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) eta ≤ ↑t}

The displacement inclusion, read through a retraction. If the reading of the path's position at time t has supremum norm at least the radius of □_m, the position is not the reading of a point of □_m, so the path has left the read cube by time t.

3. The printed forms

theorem Algsuperdiff.Section5.Provider.measure_exitTime_le_exp_neg_displacementMinScale_on {d : ℕ} {alpha : Type u_1} [PseudoMetricSpace alpha] (M : Section3.ABKModel d) (Q : MeasureTheory.Measure (MarkovProcess.ContinuousPath alpha)) (U : Set alpha) {C delta kappa : ℝ} {m n : ℤ} (t : NNReal) (rho : ENNReal) (hC : 0 < C) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (ht : 0 < ↑t) (hkappa : 0 < kappa) (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 * kappa) (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)) * rho ^ earlyExitChainLength d (m - n).toNat) (hrho : rho ≤ ENNReal.ofReal (Real.exp (-kappa))) : Q {eta : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U eta ≤ ↑t} ≤ ENNReal.ofReal (Real.exp (-earlyExitDecayConstant d M.gamma delta kappa * Support.displacementMinScale M.nu (Section3.Disorder.cstar M) M.gamma (↑t) m))

Printed early-exit probability on a carrier. The canonical-chain estimate and the full auxiliary-scale straddle give the paper's exponential minimum for an arbitrary law on the continuous paths of the carrier.