Atom-free running infima and stable passage laws

The running infimum of the stable process has no atoms. Negative levels are split at a positive rational time: the value at that time has a density and is independent of the centered future. Regularity at zero handles the zero level (J. Bertoin, Lévy Processes, 1996, Chapter VII).

theorem BGW.StableTrees.runningInf_noAtoms {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) (c : ℝ) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | runningInfLoc f t = c} = 0

runningInf_noAtoms: for t > 0 the running infimum I_t = inf_{u ≤ t} X_u has no atoms. For c > 0 this is empty (I_t ≤ X_0 = 0); for c = 0 it follows from regularity of 0; for c < 0, I_t = inf_{[a,t]} X for some rational a > 0 and X_a + inf_u (X_{a+u} - X_a) is a sum with an independent atom-free (density) first term.

theorem BGW.StableTrees.iInf_restrict_stablePath (f : Skorokhod.DLoc) (T : NNReal) : ⨅ (s : ↑(Set.Icc 0 ↑T)), (Skorokhod.DLoc.restrict T f) s = runningInfLoc f T

The running infimum of a local path agrees with the infimum of its compact restriction.

theorem BGW.StableTrees.iInf_noAtoms_stableProcessLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : ℝ} (hT : 0 < T) (c : ℝ) : ↑(stableProcessLaw θ T) {g : Skorokhod.D T ℝ | ⨅ (s : ↑(Set.Icc 0 T)), g s = c} = 0

The fixed-horizon form on D T ℝ, the one consumed with StableDomain.tendsto_stepPathLaw: the law of inf_{s ≤ T} g s under stableProcessLaw θ T has no atoms.

theorem BGW.StableTrees.passageLaw_Iic_eq_runningInf {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {t : NNReal} (ht : 0 < t) : (passageLaw θ x) (Set.Iic ↑t) = ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | runningInfLoc f t ≤ -↑x} ∧ ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | runningInfLoc f t ≤ -↑x} = ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | runningInfLoc f t < -↑x}

CDF of the passage time through the running infimum (strict vs weak resolved by runningInf_noAtoms): for x ≥ 0, t > 0, P(T_x ≤ t) = P(I_t ≤ -x) = P(I_t < -x).